∀ (R : Type u_4) (S : Type u_2) (A : Type u_3) (B : Type u_1) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [h : Algebra.IsPushout R S A B] (this : Algebra.IsPushout R A S B) (a : A) (b : S) (y : Ω[A⁄R]) (x : A) (z : S),
  b • z • a • x • (KaehlerDifferential.map R S A B) y =
      ((algebraMap A B) a * (algebraMap S B) b) • z • x • (KaehlerDifferential.map R S A B) y →
    (LinearEquiv.restrictScalars R
              (TensorProduct.AlgebraTensorModule.congr (Algebra.IsPushout.equiv R A S B).symm.toLinearEquiv
                    (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
                  TensorProduct.comm A (TensorProduct R A S) Ω[A⁄R] ≪≫ₗ
                TensorProduct.AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S) ≪≫ₗ
            TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
          LinearEquiv.restrictScalars R (KaehlerDifferential.tensorKaehlerEquivBase R S A B))
        ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) =
      (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) •
        (LinearEquiv.restrictScalars R
                (TensorProduct.AlgebraTensorModule.congr (Algebra.IsPushout.equiv R A S B).symm.toLinearEquiv
                      (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
                    TensorProduct.comm A (TensorProduct R A S) Ω[A⁄R] ≪≫ₗ
                  TensorProduct.AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S) ≪≫ₗ
              TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
            LinearEquiv.restrictScalars R (KaehlerDifferential.tensorKaehlerEquivBase R S A B))
          ((Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y)