-- 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 y : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
⊢ (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)))
have 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)
Tactic: apply Subtype.ext