no goals
α : Sort u_1
β : Sort u_2
γ : Sort ?u.12071
f✝ f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂
rw [h₂.comp_eq_id, comp.right_id]
no goals
α : Sort u_1
β : Sort u_2
γ : Sort ?u.12071
f✝ f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂
rw [← comp.assoc, h₁.comp_eq_id, comp.left_id]