-- Mathlib/RingTheory/Filtration.lean
theorem submodule_closure_single :
    AddSubmonoid.closure (⋃ i, single R i '' (F.N i : Set M)) = F.submodule.toAddSubmonoid

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
h : ¬i = j
⊢ 0 ∈ F.N j

Tactic:
exact (F.N j).zero_mem

Result:
no goals

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ Finsupp.sum f Finsupp.single ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Tactic:
apply AddSubmonoid.sum_mem _ _

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ ∀ c ∈ f.support, Finsupp.single c (f c) ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i)) = F.submodule.toAddSubmonoid

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i)) ≤ F.submodule.toAddSubmonoid

case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ F.submodule.toAddSubmonoid ≤ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i)) ≤ F.submodule.toAddSubmonoid

Tactic:
rw [AddSubmonoid.closure_le, Set.iUnion_subset_iff]

Result:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ ∀ (i : ℕ), ⇑(single R i) '' ↑(F.N i) ⊆ ↑F.submodule.toAddSubmonoid

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ F.submodule.toAddSubmonoid ≤ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Tactic:
intro f hf

Result:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ f ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
h : i = j
⊢ m ∈ F.N j

Tactic:
rwa [← h]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ ∀ c ∈ f.support, Finsupp.single c (f c) ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Tactic:
rintro c -

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
c : ℕ
⊢ Finsupp.single c (f c) ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
c : ℕ
⊢ Finsupp.single c (f c) ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Tactic:
exact AddSubmonoid.subset_closure (Set.subset_iUnion _ c <| Set.mem_image_of_mem _ (hf c))

Result:
no goals

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ f ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Tactic:
rw [← f.sum_single]

Result:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ Finsupp.sum f Finsupp.single ∈ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))

Proof state:
case a.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ ((single R i) m) j ∈ F.N j

Tactic:
rw [single_apply]

Result:
case a.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ (if i = j then m else 0) ∈ F.N j

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ ∀ (i : ℕ), ⇑(single R i) '' ↑(F.N i) ⊆ ↑F.submodule.toAddSubmonoid

Tactic:
rintro i _ ⟨m, hm, rfl⟩ j

Result:
case a.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ ((single R i) m) j ∈ F.N j

Proof state:
case a.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ (if i = j then m else 0) ∈ F.N j

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
h : i = j
⊢ m ∈ F.N j

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
h : ¬i = j
⊢ 0 ∈ F.N j