awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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 : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • (m - n))
⊢ Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))

Tactic:
replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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 : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
rwa :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₁ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (((↑x : R) • IsLocalization.mk' S 1 x) • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₂ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S (↑x : R) x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₃ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₄ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (m - n)),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀
    (e :
      Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
        (Submodule.Quotient.mk n)),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)

Tactic:
rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e

Premises used: Submodule.Quotient.eq, smul_assoc, IsLocalization.mk'_self', one_smul, IsLocalization.smul_mk'_one, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
y : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
obtain :
  ∀ (y : N),
    ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
      HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2
          (Submodule.Quotient.mk y) =
        ((Submodule.toLocalizedQuotient' S p f M' :
              LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
                (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
            (a : M ⧸ M') → N ⧸ localized' S p f M')
          x.1
⊢ ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    x.2 • y =
      ((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        x.1

Tactic:
obtain ⟨y, rfl⟩ := mk_surjective _ y

Premises used: Submodule.Quotient.mk_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
y : N
obtain :
  ∀ (y : M) (s : ↥p),
    ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
      HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2
          (Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s))) =
        ((Submodule.toLocalizedQuotient' S p f M' :
              LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
                (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
            (a : M ⧸ M') → N ⧸ localized' S p f M')
          x.1
⊢ ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2 (Submodule.Quotient.mk y) =
      ((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        x.1

Tactic:
obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
y : M
s : ↥p
⊢ HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk y, s).2
      (Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s))) =
    ((Submodule.toLocalizedQuotient' S p f M' :
          LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
            (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : M ⧸ M') → N ⧸ localized' S p f M')
      (Submodule.Quotient.mk y, s).1

Tactic:
simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']

Premises used: Submodule.Quotient.mk_smul, IsLocalizedModule.mk'_cancel', Submodule.toLocalizedQuotient'_mk, Function.uncurry_apply_pair
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
y : M
s : ↥p
⊢ ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2
        (Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s))) =
      ((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        x.1

Tactic:
exact ⟨⟨Submodule.Quotient.mk y, s⟩,
      by simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
m n : M ⧸ M'
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        m :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        n :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
obtain :
  ∀ (m n : M)
    (e :
      Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
        (((Submodule.toLocalizedQuotient' S p f M' :
                LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
                  (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : M ⧸ M') → N ⧸ localized' S p f M')
            (Submodule.Quotient.mk m) :
          HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
        (((Submodule.toLocalizedQuotient' S p f M' :
                LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
                  (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : M ⧸ M') → N ⧸ localized' S p f M')
            (Submodule.Quotient.mk n) :
          HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))),
    ∃ (c : ↥p),
      HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
⊢ ∃ (c : ↥p), c • m = c • n

Tactic:
obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)

Premises used: PProd.mk, Submodule.Quotient.mk_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
m n : M
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
⊢ Membership.mem (α := N) (γ := Submodule S N) (localized' S p f M') ((f : (a : M) → N) (m - n) : N)

Tactic:
simpa [Submodule.Quotient.eq] using e

Premises used: Submodule.Quotient.eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
m n : M
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
obtain :
  ∀ (x : M) (hx : x ∈ M') (s : ↥p) (hs : mk' f x s = (f : (a : M) → N) (m - n)),
    ∃ (c : ↥p),
      HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
⊢ ∃ (c : ↥p),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)

Tactic:
obtain ⟨x, hx, s, hs⟩ : f (m - n) ∈ _ := by simpa [Submodule.Quotient.eq] using e

Premises used: HSub.hSub, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
m n : M
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
x : M
hx : x ∈ M'
s : ↥p
hs : mk' f x s = (f : (a : M) → N) (m - n)
⊢ Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) (s • (m - n)) : N) ((f : (a : M) → N) x : N)

Tactic:
simp [-map_sub, ← hs]

Premises used: map_sub
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
m n : M
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
x : M
hx : x ∈ M'
s : ↥p
hs : mk' f x s = (f : (a : M) → N) (m - n)
obtain :
  ∀ (c : ↥p) (hc : c • s • (m - n) = c • x),
    ∃ (c : ↥p),
      HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
⊢ ∃ (c : ↥p),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)

Tactic:
obtain ⟨c, hc⟩ := exists_of_eq (S := p) (show f (s • (m - n)) = f x by simp [-map_sub, ← hs])

Premises used: IsLocalizedModule.exists_of_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
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
m n : M
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
x : M
hx : x ∈ M'
s : ↥p
hs : mk' f x s = (f : (a : M) → N) (m - n)
c : ↥p
hc : c • s • (m - n) = c • x
⊢ HSMul.hSMul (β := M ⧸ M') (c * s) (Submodule.Quotient.mk m) =
    HSMul.hSMul (β := M ⧸ M') (c * s) (Submodule.Quotient.mk n)

Tactic:
simpa only [← Quotient.mk_smul, Submodule.Quotient.eq,
      ← smul_sub, mul_smul, hc] using M'.smul_mem c hx

Premises used: Submodule.Quotient.eq, Submodule.Quotient.mk_smul, smul_sub, Subtype.val, SemigroupAction.mul_smul, Submodule.smul_mem