Theorem: inverse_spec (LeanTeaching/TD/TD06_sol.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]
State after:
α : Type u_1
β : Type u_2
inst✝ : Inhabited α
P : α → Prop
h✝ : ∃ x, P x
f : α → β
y : β
h : ∃ x, f x = y
⊢ f (if h : ∃ x, f x = y then choose h else default) = 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 (if h : ∃ x, f x = y then choose h else default) = y
Tactic:
rw [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