awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ (↑M' : Set M)
⊢ IsLocalizedModule.mk' (S := p) f m 1 = (f : (a : M) → N) m

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ (↑M' : Set M)
⊢ Membership.mem (α := N) (↑(localized' S p f M') : Set N) ((f : (a : M) → N) m : N)

Tactic:
exact ⟨m, hm, 1, by simp⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
refine : LE.le (α := Submodule S N) (localized' S p f M') (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))
⊢ Eq (α := Submodule S N) (localized' S p f M') (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))

Tactic:
refine le_antisymm ?_ (span_le.mpr <| by rintro _ ⟨m, hm, rfl⟩; exact ⟨m, hm, 1, by simp⟩)

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
rw :
  Membership.mem (γ := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))
    (IsLocalization.mk' S 1 s • IsLocalizedModule.mk' (S := p) f m 1)
⊢ Membership.mem (γ := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑M' : Set M))) (IsLocalizedModule.mk' f m s)

Tactic:
rw [← one_smul R m, ← mul_one s, ← IsLocalizedModule.mk'_smul_mk' S]

Premises used: one_smul, IsLocalizedModule.mk'_smul_mk', mul_one
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
⊢ (f : (a : M) → N) m = IsLocalizedModule.mk' (S := p) f m 1

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
⊢ Membership.mem (γ := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))
    (IsLocalization.mk' S 1 s • IsLocalizedModule.mk' (S := p) f m 1)

Tactic:
exact smul_mem _ _ (subset_span ⟨m, hm, by simp⟩)
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ (↑M' : Set M)
⊢ ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = (f : (a : M) → N) x

Tactic:
⟨x, hx, 1, IsLocalizedModule.mk'_one p f x⟩

Premises used: IsLocalizedModule.mk'_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ (↑M' : Set M)
⊢ ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = (f : (a : M) → N) x

Tactic:
exact ⟨x, hx, 1, IsLocalizedModule.mk'_one p f x⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M'_1 M'' M' : Submodule R M
N' : Submodule S N
h : localized' S p f M' ≤ N'
m : M
hm : m ∈ M'
⊢ IsLocalizedModule.mk' (S := p) f m 1 = (f : (a : M) → N) m

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M'_1 M'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun (x : Submodule S N) ↦ comap f (restrictScalars R x)) N'
rw : (⇑f : (a : M) → N) '' (↑M' : Set M) ⊆ (↑N' : Set N)
⊢ localized' S p f M' ≤ N'

Tactic:
rw [localized'_eq_span, span_le]

Premises used: Submodule.localized'_eq_span, Submodule.span_le
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M'_1 M'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun (x : Submodule S N) ↦ comap f (restrictScalars R x)) N'
⊢ (⇑f : (a : M) → N) '' (↑M' : Set M) ⊆ (↑N' : Set N)

Tactic:
apply map_le_iff_le_comap.mpr h

Premises used: Iff.mpr, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
n : N
hn : n ∈ N'
obtain :
  ∀ (m : M) (s : ↥p) (hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'),
    Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N')))
      (Function.uncurry (IsLocalizedModule.mk' f) (m, s))
⊢ Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N'))) n

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

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N')))
    (Function.uncurry (IsLocalizedModule.mk' f) (m, s))

Tactic:
⟨m, ?_, s, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
refine : m ∈ comap f (restrictScalars R N')
⊢ Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N')))
    (Function.uncurry (IsLocalizedModule.mk' f) (m, s))

Tactic:
refine ⟨m, ?_, s, rfl⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) (IsLocalizedModule.mk' f m s) ∈ N'
⊢ m ∈ comap f (restrictScalars R N')

Tactic:
rw [mem_comap, restrictScalars_mem, ← IsLocalizedModule.mk'_cancel' _ _ s,
      Submonoid.smul_def, ← algebraMap_smul S]

Premises used: Submodule.mem_comap, algebraMap_smul, IsLocalizedModule.mk'_cancel', Submonoid.smul_def, Submodule.restrictScalars_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) (IsLocalizedModule.mk' f m s) ∈ N'

Tactic:
smul_mem _ _ hn

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) (IsLocalizedModule.mk' f m s) ∈ N'

Tactic:
exact smul_mem _ _ hn

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
rw : localized₀ p f ⊥ ≤ ⊥
⊢ localized₀ p f ⊥ = ⊥

Tactic:
rw [← le_bot_iff]

Premises used: le_bot_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
s : ↥p
⊢ Membership.mem (γ := Submodule R N) ⊥ (IsLocalizedModule.mk' f 0 s)

Tactic:
simp only [IsLocalizedModule.mk'_zero, mem_bot]

Premises used: Submodule.mem_bot, IsLocalizedModule.mk'_zero
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
⊢ (↑(localized' S p f ⊥) : Set N) = (↑⊥ : Set N)

Tactic:
apply SetLike.ext'_iff.mp <| Submodule.localized₀_bot p f

Premises used: Submodule.localized₀_bot, Iff.mp, SetLike.ext'_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
rw : ⊤ ≤ localized₀ p f ⊤
⊢ localized₀ p f ⊤ = ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
x : N
h : Membership.mem (γ := Submodule R N) ⊤ x
obtain :
  ∀ (x : M) (s : ↥p),
    Membership.mem (γ := Submodule R N) ⊤ (Function.uncurry (IsLocalizedModule.mk' f) (x, s)) →
      Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ localized₀ p f ⊤
⊢ x ∈ localized₀ p f ⊤

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

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
x : M
s : ↥p
h : Membership.mem (γ := Submodule R N) ⊤ (Function.uncurry (IsLocalizedModule.mk' f) (x, s))
⊢ Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ localized₀ p f ⊤

Tactic:
⟨x, trivial, s, rfl⟩

Premises used: trivial, Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
x : M
s : ↥p
h : Membership.mem (γ := Submodule R N) ⊤ (Function.uncurry (IsLocalizedModule.mk' f) (x, s))
⊢ Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ localized₀ p f ⊤

Tactic:
exact ⟨x, trivial, s, rfl⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
⊢ (↑(localized' S p f ⊤) : Set N) = (↑⊤ : Set N)

Tactic:
apply SetLike.ext'_iff.mp <| Submodule.localized₀_top p f

Premises used: Submodule.localized₀_top, Iff.mp, SetLike.ext'_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
simp :
  ∀ (x : N),
    (∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ↔
      (∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
⊢ localized₀ p f (M' ⊓ M'') = localized₀ p f M' ⊓ localized₀ p f M''

Tactic:
simp only [Submodule.ext_iff, Submodule.mem_inf, mem_localized₀]

Premises used: Submodule.ext_iff, Submodule.mem_inf, Submodule.mem_localized₀
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
⊢ (∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) →
    (∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
grind
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
refine :
  ∀ (x : N),
    ((∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) →
      ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
⊢ ∀ (x : N),
    (∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ↔
      (∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
refine fun x ↦ ⟨by grind, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
⊢ IsLocalizedModule.mk' f j t = IsLocalizedModule.mk' f i s

Tactic:
have h := ht.trans hs.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
h : IsLocalizedModule.mk' f j t = IsLocalizedModule.mk' f i s
⊢ ∃ (s_1 : ↥p), s_1 • t • i = s_1 • s • j

Tactic:
rw [IsLocalizedModule.mk'_eq_mk'_iff] at h

Premises used: IsLocalizedModule.mk'_eq_mk'_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
h : ∃ (s_1 : ↥p), s_1 • t • i = s_1 • s • j
obtain :
  ∀ (k : ↥p) (hk : k • t • i = k • s • j), ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
obtain ⟨k, hk⟩ := h
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
⟨(k * t) • i, ⟨M'.smul_of_tower_mem (k * t) hi, ?_⟩, k * s * t, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro, HSMul.hSMul, Submodule.smul_of_tower_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
refine_1 : (k * t) • i ∈ M''
refine_2 : IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
refine ⟨(k * t) • i, ⟨M'.smul_of_tower_mem (k * t) hi, ?_⟩, k * s * t, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
refine_1 : (k * s) • j ∈ M''
⊢ (k * t) • i ∈ M''

Tactic:
rw [mul_smul, hk, smul_smul]

Premises used: smul_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ (k * s) • j ∈ M''

Tactic:
M''.smul_of_tower_mem (k * s) hj

Premises used: HMul.hMul, Set.Mem, Submodule.smul_of_tower_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ (k * s) • j ∈ M''

Tactic:
exact M''.smul_of_tower_mem (k * s) hj

Premises used: HMul.hMul, Submodule.smul_of_tower_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
refine_2 : IsLocalizedModule.mk' f (k • t • i) (k * s * t) = x
refine_2₁ : IsLocalizedModule.mk' f (k • s • j) (k * s * t) = x
refine_2₂ : IsLocalizedModule.mk' f ((k * s) • j) (k * s * t) = x
refine_2₃ refine_2₄ refine_2₅ refine_2₆ : IsLocalizedModule.mk' f j t = x
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x

Tactic:
rwa [mul_smul, hk, smul_smul, IsLocalizedModule.mk'_cancel_left]

Premises used: smul_smul, SemigroupAction.mul_smul, IsLocalizedModule.mk'_cancel_left