exists.some is eq to itself

Stream: new members

[Marcus Rossel]

I'm stuck on this:

import data.finmap

example (f : finmap (λ _ : ℕ, ℕ)) (n : ℕ) (h : ∃ m, f.lookup n = some m) :
f.lookup n = some h.some :=
begin
  obtain ⟨m, hm⟩ := h,
  simp only [hm],

end

Since m is obtained from ∃ m, f.lookup n = some m, there must be some way to prove that m = (∃ m, f.lookup n = some m).some. But I can't figure out how.

[Eric Wieser]

apply classical.some_spec

[Eric Wieser]

generalize_proofs h2, makes it a bit easier to understand the goal state