∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2),
  (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) ↔
    (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S