(R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          { f //
              (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f =
                IsScalarTower.toAlgHom R S
                  ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸
                    (KaehlerDifferential.ideal R S).cotangentIdeal) } ≃
            { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }