Theorem: inverse_spec (LeanInRome/S4_Sets_and_Functions/solutions/Solutions_S02_Functions.lean)

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

State before:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (choose h) = y
Tactic:
exact Classical.choose_spec h
State after:
no goals