∀ {R : Type u_3} {P : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S],
  KaehlerDifferential.kerCotangentToTensor R P S =
      ↑(LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)) ∘ₗ
        ↑P (KaehlerDifferential.kerToTensor R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S) ∘ₗ
          ↑((RingHom.ker (algebraMap P S)).cotangentEquivIdeal.trans
              (LinearEquiv.restrictScalars P
                (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
                  (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯))) →
    ∀
      (l :
        TensorProduct (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S
            Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
          ↥(RingHom.ker (algebraMap (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S))),
      l ∘ₗ KaehlerDifferential.kerToTensor R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S = LinearMap.id →
        (↑((RingHom.ker (algebraMap P S)).cotangentEquivIdeal.trans
                    (LinearEquiv.restrictScalars P
                      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
                        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯))).symm ∘ₗ
              ↑P l ∘ₗ ↑(LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)).symm) ∘ₗ
            KaehlerDifferential.kerCotangentToTensor R P S =
          LinearMap.id