-- 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
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
x : B ⊗[A] Ω[A⁄R]
a : A
b : S
tmul :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) 0) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) 0)
tmul₁ :
  ∀ (x y : B ⊗[A] Ω[A⁄R]),
    (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
          (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) x) =
        HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
          ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S]) →
      (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
            (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) y) =
          HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
            ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) y : Ω[B⁄S]) →
        (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
            (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) (x + y)) =
          HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
            ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) (x + y) : Ω[B⁄S])
tmul₂ :
  ∀ (x : B) (y : Ω[A⁄R]),
    (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
        (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
          ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) (x ⊗ₜ[A] y)) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) (x ⊗ₜ[A] y) : Ω[B⁄S])
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) x) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S])

Tactic:
induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *]
  | tmul x y =>
  obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *, add_tmul]
  | tmul x z =>
  suffices b • z • a • x • KaehlerDifferential.map R S A B y =
      (algebraMap A B a * algebraMap S B b) • z • x • KaehlerDifferential.map R S A B y by
    simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]
  simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
  ring_nf

Premises used: map_add, algebraMap_smul, TensorProduct.add_tmul, TensorProduct.tmul, SemigroupAction.mul_smul, smul_add, rfl