∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [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],
  KaehlerDifferential.tensorKaehlerEquiv R S A B =
    {
      toAddHom :=
        (↑(((LinearEquiv.restrictScalars R
                      (((TensorProduct.AlgebraTensorModule.congr (Algebra.IsPushout.equiv R A S B).symm.toLinearEquiv
                                (LinearEquiv.refl A Ω[A⁄R])).trans
                            (TensorProduct.comm A (TensorProduct R A S) Ω[A⁄R])).trans
                        (TensorProduct.AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S))).trans
                  (TensorProduct.comm R Ω[A⁄R] S)).trans
              (LinearEquiv.restrictScalars R (KaehlerDifferential.tensorKaehlerEquivBase R S A B)))).toAddHom,
      map_smul' := ⋯,
      invFun :=
        (((LinearEquiv.restrictScalars R
                    (((TensorProduct.AlgebraTensorModule.congr (Algebra.IsPushout.equiv R A S B).symm.toLinearEquiv
                              (LinearEquiv.refl A Ω[A⁄R])).trans
                          (TensorProduct.comm A (TensorProduct R A S) Ω[A⁄R])).trans
                      (TensorProduct.AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S))).trans
                (TensorProduct.comm R Ω[A⁄R] S)).trans
            (LinearEquiv.restrictScalars R (KaehlerDifferential.tensorKaehlerEquivBase R S A B))).invFun,
      left_inv := ⋯, right_inv := ⋯ }