∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
  {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f}, (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M