-- 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
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
x : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)
zero :
  Eq (α := M ⊗[R] N)
    (↑((tensorEqLocus S M f g :
            (a : M ⊗[R] ↥(eqLocus f g)) →
              ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                  ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
          0) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) 0)
tmul :
  ∀ (x : M) (y : ↥(eqLocus f g)),
    Eq (α := M ⊗[R] N)
      ((↑((tensorEqLocus S M f g :
                (a : M ⊗[R] ↥(eqLocus f g)) →
                  ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                      ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
              (x ⊗ₜ[R] y)) :
          M ⊗[R] N) :
        M ⊗[R] N)
      ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    ((↑((tensorEqLocus S M f g :
              (a : M ⊗[R] ↥(eqLocus f g)) →
                ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                    ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
            x) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) x : M ⊗[R] N)
have add : ∀ (x y : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)),
  Eq (α := M ⊗[R] N)
      ((↑((tensorEqLocus S M f g :
                (a : M ⊗[R] ↥(eqLocus f g)) →
                  ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                      ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
              x) :
          M ⊗[R] N) :
        M ⊗[R] N)
      ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) x : M ⊗[R] N) →
    Eq (α := M ⊗[R] N)
        ((↑((tensorEqLocus S M f g :
                  (a : M ⊗[R] ↥(eqLocus f g)) →
                    ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                        ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
                y) :
            M ⊗[R] N) :
          M ⊗[R] N)
        ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) y : M ⊗[R] N) →
      Eq (α := M ⊗[R] N)
        ((↑((tensorEqLocus S M f g :
                  (a : M ⊗[R] ↥(eqLocus f g)) →
                    ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                        ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
                (x + y)) :
            M ⊗[R] N) :
          M ⊗[R] N)
        ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) (x + y) : M ⊗[R] N)
Tactic: induction x
Cleared hypotheses: x