-- 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
z : A
tmul :
  (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])
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) z : B) (0 : B)) =
    HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
          0) +
      HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0
        ((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])
            ((algebraMap A B : (a : A) → B) z) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
tmul₁ :
  ∀ (m : A),
    (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])
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) z : B)
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) m : B)) =
      HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
              ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) m) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
        HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) m : 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])
              ((algebraMap A B : (a : A) → B) z) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
tmul₂ :
  ∀ (s : S) (n : 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])
          (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) z : B) n) =
        HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
                n :
              TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
          HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) n
            ((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])
                ((algebraMap A B : (a : A) → B) z) :
              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])
        (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) z : B) (s • n)) =
      HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
              (s • n) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (s • n)
          ((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])
              ((algebraMap A B : (a : A) → B) z) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
tmul₃ :
  ∀ (n₁ n₂ : 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])
          (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) z : B) n₁) =
        HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
                n₁ :
              TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
          HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) n₁
            ((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])
                ((algebraMap A B : (a : A) → B) z) :
              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])
          (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) z : B) n₂) =
        HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
                n₂ :
              TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
          HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) n₂
            ((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])
                ((algebraMap A B : (a : A) → B) z) :
              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])
        (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) z : B) (n₁ + n₂)) =
      HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
              (n₁ + n₂) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (n₁ + n₂)
          ((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])
              ((algebraMap A B : (a : A) → B) z) :
            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])
      (HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) z : B) b) =
    HSMul.hSMul (α := B) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap A B : (a : A) → B) z : 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])
            ((algebraMap A B : (a : A) → B) z) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
induction b using h.out.inductionOn with
      | zero => rw [map_zero, zero_smul, smul_zero, zero_add, mul_zero, map_zero]
      | tmul =>
        simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          algebraMap_smul, ← map_mul]
        rw [← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq]
        simp only [LinearMap.coe_comp, Derivation.coeFn_coe, Function.comp_apply,
          Derivation.leibniz, mk_apply, mulActionBaseChange_smul_tmul, TensorProduct.tmul_add]
      | smul _ _ e =>
        rw [mul_comm, smul_mul_assoc, map_smul, mul_comm, e,
            map_smul, smul_add, smul_comm, smul_assoc]
      | add _ _ e₁ e₂ => simp only [mul_add, add_smul, map_add, e₁, e₂, smul_add, add_add_add_comm]

Premises used: smul_assoc, IsScalarTower.coe_toAlgHom', TensorProduct.mk_apply, smul_zero, AlgHom.toLinearMap_apply, map_zero, map_add, smul_mul_assoc, algebraMap_smul, zero_add, MulZeroClass.mul_zero, Derivation.leibniz, Algebra.IsPushout.out, map_mul, Derivation.coeFn_coe, zero_smul, add_smul, LinearMap.coe_comp, mul_comm, TensorProduct.tmul_add, mul_add, Function.comp_apply, add_add_add_comm, TensorProduct.tmul, SMulCommClass.smul_comm, smul_add, IsBaseChange.lift_eq, KaehlerDifferential.mulActionBaseChange_smul_tmul, map_smul, IsScalarTower.toAlgHom_apply