-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
e :
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                (a : R) → Module.End R (N ⧸ localized' S p f M'))
              (↑x : R) :
            Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
        m :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                (a : R) → Module.End R (N ⧸ localized' S p f M'))
              (↑x : R) :
            Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
        n :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
⊢ m = n
have obtain : ∀ (m n : N)
  (e :
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
      ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                  (a : R) → Module.End R (N ⧸ localized' S p f M'))
                (↑x : R) :
              Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
            (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
          (Submodule.Quotient.mk m) :
        HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
      ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                  (a : R) → Module.End R (N ⧸ localized' S p f M'))
                (↑x : R) :
              Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
            (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
          (Submodule.Quotient.mk n) :
        HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
Cleared hypotheses: m, n, e