no goals
α : Type u_2
β : Type u_1
γ : Type ?u.2241
e : Option α ≃ Option β
x : α
h : ∃ x', ↑e (some x) = some x'
⊢ some (removeNone_aux e x) = ↑e (some x)
simp [removeNone_aux, Option.isSome_iff_exists.mpr h]