Theorem: inverse_spec (LeanInRome/S4_Sets_and_Functions/S02_Functions.lean)

State before:
α : 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
Tactic:
rw [inverse, dif_pos h]
State after:
α : 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

State before:
α : 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
Tactic:
exact Classical.choose_spec h
State after:
no goals