-- 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₁ b₂ : 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])
      (b₁ * b) =
    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])
            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])
            b₁ :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
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])
      (b₂ * b) =
    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])
            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])
            b₂ :
          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])
      ((b₁ + b₂) * b) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (b₁ + 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])
            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])
            (b₁ + b₂) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
simp only [add_mul, add_smul, map_add, e₁, e₂, smul_add, add_add_add_comm]

Premises used: add_mul, map_add, add_smul, add_add_add_comm, smul_add