-- 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)) :
      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)
have 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) =
  (↑(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: rw [AlgHom.coe_tensorEqualizerAux]