∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  Function.RightInverse (AddEquiv.refl P.Cotangent).invFun (AddEquiv.refl P.Cotangent).toFun