Theorem: Function.left_id_left_inverse (FOL/FunctionUpdateITE.lean)

State before:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
⊢ LeftInverse g f
Tactic:
simp only [Function.LeftInverse]
State after:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
⊢ ∀ (x : α), g (f x) = x

State before:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
⊢ ∀ (x : α), g (f x) = x
Tactic:
intro x
State after:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
x : α
⊢ g (f x) = x

State before:
α β : Type
f : α → β
g : β → α
h1 : g ∘ f = id
x : α
⊢ g (f x) = x
Tactic:
exact congrFun h1 x
State after:
no goals