-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
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
x : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
zero :
  Eq (α := T ⊗[R] A)
    (↑((tensorEqualizerAux S T f g :
            (a : T ⊗[R] ↥(equalizer f g)) →
              ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g)))
          0) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
          TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
        (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
      0)
tmul :
  ∀ (x : T) (y : ↥(equalizer f g)),
    Eq (α := T ⊗[R] A)
      ((↑((tensorEqualizerAux S T f g :
                (a : T ⊗[R] ↥(equalizer f g)) →
                  ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                      (Algebra.TensorProduct.map (AlgHom.id S T) g)))
              (x ⊗ₜ[R] y)) :
          T ⊗[R] A) :
        T ⊗[R] A)
      (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
              TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
            (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
          (x ⊗ₜ[R] y) :
        T ⊗[R] A)
⊢ Eq (α := T ⊗[R] A)
    ((↑((tensorEqualizerAux S T f g :
              (a : T ⊗[R] ↥(equalizer f g)) →
                ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                    (Algebra.TensorProduct.map (AlgHom.id S T) g)))
            x) :
        T ⊗[R] A) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
            TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
          (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
        x :
      T ⊗[R] A)
have add : ∀ (x y : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g))
  (hx :
    Eq (α := T ⊗[R] A)
      ((↑((tensorEqualizerAux S T f g :
                (a : T ⊗[R] ↥(equalizer f g)) →
                  ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                      (Algebra.TensorProduct.map (AlgHom.id S T) g)))
              x) :
          T ⊗[R] A) :
        T ⊗[R] A)
      (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
              TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
            (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
          x :
        T ⊗[R] A))
  (hy :
    Eq (α := T ⊗[R] A)
      ((↑((tensorEqualizerAux S T f g :
                (a : T ⊗[R] ↥(equalizer f g)) →
                  ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                      (Algebra.TensorProduct.map (AlgHom.id S T) g)))
              y) :
          T ⊗[R] A) :
        T ⊗[R] A)
      (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
              TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
            (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
          y :
        T ⊗[R] A)),
  Eq (α := T ⊗[R] A)
    ((↑((tensorEqualizerAux S T f g :
              (a : T ⊗[R] ↥(equalizer f g)) →
                ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                    (Algebra.TensorProduct.map (AlgHom.id S T) g)))
            (x + y)) :
        T ⊗[R] A) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
            TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
          (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
        (x + y) :
      T ⊗[R] A)
Tactic: induction x with
  | zero => rfl
  | tmul => rfl
  | add x y hx hy => simp [hx, hy]
Cleared hypotheses: x