-- 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
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 y : M
h :
  ∀ (x_1 : ↥(eqLocus f g)),
    Eq (α := M ⊗[R] N)
      (↑(({
                toFun := fun (a : ↥(eqLocus f g)) ↦
                  Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                    Membership.mem (γ := Submodule S (M ⊗[R] N))
                      (eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                            f :
                          M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                            g :
                          M ⊗[R] N →ₗ[S] M ⊗[R] P))
                      x)
                    ((x + y) ⊗ₜ[R] (↑a : N)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : ↥(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_1) :
        M ⊗[R] N)
      (↑((HAdd.hAdd (α :=
                ↥(eqLocus f g) →ₗ[R]
                  ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          f :
                        M ⊗[R] N →ₗ[S] M ⊗[R] P)
                      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          g :
                        M ⊗[R] N →ₗ[S] M ⊗[R] P)))
                {
                  toFun := fun (a : ↥(eqLocus f g)) ↦
                    Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                      Membership.mem (γ := Submodule S (M ⊗[R] N))
                        (eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                              f :
                            M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                              g :
                            M ⊗[R] N →ₗ[S] M ⊗[R] P))
                        x)
                      (x ⊗ₜ[R] (↑a : N)) ⋯,
                  map_add' := ⋯, map_smul' := ⋯ :
                  ↥(eqLocus f g) →ₗ[R]
                    ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                            f :
                          M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                            g :
                          M ⊗[R] N →ₗ[S] M ⊗[R] P)) }
                {
                  toFun := fun (a : ↥(eqLocus f g)) ↦
                    Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                      Membership.mem (γ := Submodule S (M ⊗[R] N))
                        (eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                              f :
                            M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                              g :
                            M ⊗[R] N →ₗ[S] M ⊗[R] P))
                        x)
                      (y ⊗ₜ[R] (↑a : N)) ⋯,
                  map_add' := ⋯, map_smul' := ⋯ :
                  ↥(eqLocus f g) →ₗ[R]
                    ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                            f :
                          M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                            g :
                          M ⊗[R] N →ₗ[S] M ⊗[R] P)) } :
              (a : ↥(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_1) :
        M ⊗[R] N)
⊢ {
      toFun := fun (a : ↥(eqLocus f g)) ↦
        Subtype.mk (p := fun (x : M ⊗[R] N) ↦
          Membership.mem (γ := Submodule S (M ⊗[R] N))
            (eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
              (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                    (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                  f :
                M ⊗[R] N →ₗ[S] M ⊗[R] P)
              (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                    (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                  g :
                M ⊗[R] N →ₗ[S] M ⊗[R] P))
            x)
          ((x + y) ⊗ₜ[R] (↑a : N)) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α :=
      ↥(eqLocus f g) →ₗ[R]
        ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
            (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                  (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                f :
              M ⊗[R] N →ₗ[S] M ⊗[R] P)
            (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                  (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                g :
              M ⊗[R] N →ₗ[S] M ⊗[R] P)))
      {
        toFun := fun (a : ↥(eqLocus f g)) ↦
          Subtype.mk (p := fun (x : M ⊗[R] N) ↦
            Membership.mem (γ := Submodule S (M ⊗[R] N))
              (eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                      (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                    f :
                  M ⊗[R] N →ₗ[S] M ⊗[R] P)
                (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                      (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                    g :
                  M ⊗[R] N →ₗ[S] M ⊗[R] P))
              x)
            (x ⊗ₜ[R] (↑a : N)) ⋯,
        map_add' := ⋯, map_smul' := ⋯ :
        ↥(eqLocus f g) →ₗ[R]
          ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
              (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                    (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                  f :
                M ⊗[R] N →ₗ[S] M ⊗[R] P)
              (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                    (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                  g :
                M ⊗[R] N →ₗ[S] M ⊗[R] P)) }
      {
        toFun := fun (a : ↥(eqLocus f g)) ↦
          Subtype.mk (p := fun (x : M ⊗[R] N) ↦
            Membership.mem (γ := Submodule S (M ⊗[R] N))
              (eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
                (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                      (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                    f :
                  M ⊗[R] N →ₗ[S] M ⊗[R] P)
                (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                      (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                    g :
                  M ⊗[R] N →ₗ[S] M ⊗[R] P))
              x)
            (y ⊗ₜ[R] (↑a : N)) ⋯,
        map_add' := ⋯, map_smul' := ⋯ :
        ↥(eqLocus f g) →ₗ[R]
          ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
              (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                    (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                  f :
                M ⊗[R] N →ₗ[S] M ⊗[R] P)
              (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                    (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                  g :
                M ⊗[R] N →ₗ[S] M ⊗[R] P)) }

Tactic:
ext