-- 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 y : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
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) =
    (↑(HMul.hMul (α :=
          ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
          (β :=
          ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
          ((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 :
            ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
          ((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 :
            ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))) :
      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) =
    HMul.hMul (α :=
      ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B) (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
          (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
      (β :=
      ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B) (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
          (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
      ((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 :
        ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
            (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
            (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
      ((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 :
        ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
            (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
            (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext