no goals
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g => g ∘ f) (g ∘ surjInv (_ : Surjective f)) = g
simp only [comp.assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp.right_id]