-- 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
inst_11 : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
b : A ⊗[R] S
zero :
  (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
add :
  ∀ (x y : A ⊗[R] S),
    (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
          ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x : B)
          ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S]) →
      (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
            ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
          HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y : B)
            ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S]) →
        (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
            ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
          HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) : B)
            ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
tmul :
  ∀ (a' : A) (s : S),
    (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) : B)
        ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
⊢ (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) b ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) b : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
induction b with
  | zero => simp
  | add x y _ _ => simp only [map_add, *, add_tmul, add_smul]
  | tmul a' s =>
  trans s • a' • D S B (algebraMap A B a)
  · simp [tensorKaehlerEquiv]
  · simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]

Premises used: Algebra.algebraMap, KaehlerDifferential.tensorKaehlerEquiv, map_add, KaehlerDifferential.D, Algebra.IsPushout.equiv_tmul, add_smul, TensorProduct.add_tmul, TensorProduct.tmul, SMulCommClass.smul_comm, DFunLike.coe, SemigroupAction.mul_smul