∀ {R : Type u_4} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {P : Algebra.Extension R S}
  {Q : Algebra.Extension R T} (f : P.Hom Q) (this : IsScalarTower R P.Ring Q.Ring) (this_1 : IsScalarTower P.Ring S T)
  (this_2 : IsScalarTower P.Ring Q.Ring T) (this_3 : Algebra.FormallyEtale P.Ring Q.Ring)
  (x : TensorProduct S T P.CotangentSpace),
  (LinearMap.liftBaseChange T
        (LinearMap.liftBaseChange Q.Ring
            (↑P.Ring ((TensorProduct.mk S T P.CotangentSpace) 1) ∘ₗ
              ↑P.Ring ((TensorProduct.mk P.Ring S Ω[P.Ring⁄R]) 1)) ∘ₗ
          ↑(KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm))
      ((LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map f)).toFun x) =
    x