-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
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
b : B
x : S
y : B
e :
  (IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
          ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
        (a : B) → S ⊗[R] Ω[A⁄R])
      (y * b) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            y :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul :
  (IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
          ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
        (a : B) → S ⊗[R] Ω[A⁄R])
      (x • (y * b)) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            (x • y) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul₁ :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
      ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
              ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
            (a : B) → S ⊗[R] Ω[A⁄R])
          (y * b) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            (x • y) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul₂ :
  x •
      (HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              b :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            (x • y) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul₃ :
  x •
      (HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              b :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      b •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul₄ :
  x •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              b :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      x •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      b •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul₅ :
  x •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              b :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      b •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      b •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
smul₆ smul₇ :
  x •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              b :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      b •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    x •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) y
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              b :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      b •
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x
          ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                  ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
                (a : B) → S ⊗[R] Ω[A⁄R])
              y :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
⊢ (IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
          ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
        (a : B) → S ⊗[R] Ω[A⁄R])
      (x • y * b) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (x • y)
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            b :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) b
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            (x • y) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
rw [smul_mul_assoc, map_smul, e, map_smul, smul_add,
        smul_comm x b, smul_assoc]

Premises used: smul_assoc, smul_mul_assoc, SMulCommClass.smul_comm, smul_add, map_smul