-- Module: Mathlib.RingTheory.Flat.Equalizer
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
f g : A →ₐ[R] B
inst_11 : Module.Flat R T
h₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 : A ⊗[R] S ≃ₐ[R] S ⊗[R] A := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] TensorProduct.{u_1, u_4, u_2} R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  LinearEquiv.restrictScalars R (S := R)
    (LinearMap.kerLTensorEquivOfSurjective.{u_1, u_2, u_3, u_4} (R := R) (N := S) (P := T)
      (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S T)) h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (LinearEquiv.symm
              (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A) :
            TensorProduct.{u_1, u_2, u_4} R (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A ≃ₗ[S]
              ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A)) ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (F := S →+* T) (algebraMap S T)))
            (↑ePp.symm : S ⊗[R] A ≃ₗ[S] A ⊗[R] S) :
          ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A) ≃ₗ[S]
            ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (A ⊗[R] S)) ≪≫ₗ
    LinearEquiv.restrictScalars R
      (_root_.TensorProduct.comm S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) (A ⊗[R] S))
r' x : A ⊗[R] S
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
tmul :
  (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
      (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' (0 ⊗ₜ[S] y)) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (0 ⊗ₜ[S] y) :
        ↥(RingHom.ker φ))
tmul₁ :
  ∀ (x y_1 : A ⊗[R] S),
    (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
          (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' (x ⊗ₜ[S] y)) =
        HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
          ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[S] y) :
            ↥(RingHom.ker φ)) →
      (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
            (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' (y_1 ⊗ₜ[S] y)) =
          HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
            ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (y_1 ⊗ₜ[S] y) :
              ↥(RingHom.ker φ)) →
        (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
            (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' ((x + y_1) ⊗ₜ[S] y)) =
          HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
            ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) ((x + y_1) ⊗ₜ[S] y) :
              ↥(RingHom.ker φ))
tmul₂ :
  ∀ (x : A) (z : S),
    (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
        (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' (x ⊗ₜ[R] z ⊗ₜ[S] y)) =
      HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
        ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[R] z ⊗ₜ[S] y) :
          ↥(RingHom.ker φ))
⊢ (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
      (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' (x ⊗ₜ[S] y)) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[S] y) :
        ↥(RingHom.ker φ))

Tactic:
induction x with
        | zero => simp only [zero_tmul, smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, add_tmul, LinearEquiv.map_add, *]
        | tmul x z =>
        induction r' with
        | zero => simp only [zero_smul, LinearEquiv.map_zero]
        | add x y _ _ => simp only [add_smul, LinearEquiv.map_add, *]
        | tmul r s =>
        rw [smul_tmul']
        ext1
        dsimp [e₄', ePp, φ]
        change ((r * x) ⊗ₜ[R] ((s * z) * y.1)) = (r ⊗ₜ[R] s) * (x ⊗ₜ[R] (z * y.1))
        rw [Algebra.TensorProduct.tmul_mul_tmul, mul_assoc]

Premises used: LinearEquiv.map_zero, mul_assoc, smul_zero, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.zero_tmul, LinearEquiv.map_add, zero_smul, TensorProduct.smul_tmul', add_smul, TensorProduct.add_tmul, TensorProduct.tmul, smul_add