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

State before:
α β : Type
f : α → β
g : β → α
h1 : f ∘ g = id
⊢ RightInverse g f
Tactic:
simp only [Function.RightInverse]
State after:
α β : Type
f : α → β
g : β → α
h1 : f ∘ g = id
⊢ LeftInverse f g

State before:
α β : Type
f : α → β
g : β → α
h1 : f ∘ g = id
⊢ LeftInverse f g
Tactic:
exact Function.left_id_left_inverse g f h1
State after:
no goals