rw [inverse, dif_pos h]
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (inverse f y) = y
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y