-- 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' : A ⊗[R] S
x : A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
zero :
  (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) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) 0)
add :
  ∀ (x y : A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))),
    (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (r' • x) =
        HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
          ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) x : ↥(RingHom.ker φ)) →
      (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (r' • y) =
          HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
            ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) y : ↥(RingHom.ker φ)) →
        (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (r' • (x + y)) =
          HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
            ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x + y) :
              ↥(RingHom.ker φ))
tmul :
  ∀ (x : A ⊗[R] S) (y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))),
    (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 φ)) (r' • x) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) x : ↥(RingHom.ker φ))

Tactic:
induction x with
        | zero => simp only [smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, LinearEquiv.map_add, *]
        | tmul x y =>
        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