`obtain` without any deconstruction using a tactic block doesn't name hypotheses appropriately

[ericrbg]

import tactic.rcases

example : true :=
begin
  obtain h : true,
  { trivial },
  success_if_fail { exact h },
  assumption,
end

Note that this behaviour does not happen if the term is created using :=:

example : true :=
begin
  obtain h : true := trivial,
  exact h
end

Found whilst making #15735.

[ericrbg]

The bug goes a bit higher; to rcases; rcases h with t will just let the hypothesis remain named h instead of renaming it to t.