-- 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
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)
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)
⊢ 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)

Tactic:
induction x with
  | zero => rfl
  | tmul => rfl
  | add x y hx hy => simp [hx, hy]

Premises used: TensorProduct.tmul