awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
    (↑((fun (n₀ : ℕ) ↦
            (Submodule.span (↥(reesAlgebra I))
                (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
              Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)))
          m) :
      Set (PolynomialModule R M))

Tactic:
Set.Subset.trans ?_ Submodule.subset_span

Premises used: Set.Subset.trans, Submodule.subset_span
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
mp :
  Subset (α := Set (PolynomialModule R M)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ m), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
⊢ (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
    (↑((fun (n₀ : ℕ) ↦
            (Submodule.span (↥(reesAlgebra I))
                (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
              Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)))
          m) :
      Set (PolynomialModule R M))

Tactic:
refine Set.Subset.trans ?_ Submodule.subset_span

Premises used: Set.Subset.trans, Submodule.subset_span
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ Subset (α := Set (PolynomialModule R M)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ m), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))

Tactic:
@Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
mp : i ≤ m
⊢ Subset (α := Set (PolynomialModule R M)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ m), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))

Tactic:
refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m

Tactic:
hi.trans e

Premises used: LE.le.trans
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m

Tactic:
exact hi.trans e

Premises used: LE.le.trans
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
mp :
  Eq.{u_2 + 1} (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ),
        ⋃ (i_1 : ℕ), ⋃ (_ : i_1 ≤ i), (⇑(single R i_1) : (a : M) → PolynomialModule R M) '' (↑(F.N i_1) : Set M)))
    (Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
⊢ ⨆ (n₀ : ℕ),
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule

Tactic:
rw [← Submodule.span_iUnion, ← submodule_span_single]

Premises used: Ideal.Filtration.submodule_span_single, Submodule.span_iUnion
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ Eq.{u_2 + 1} (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ),
        ⋃ (i_1 : ℕ), ⋃ (_ : i_1 ≤ i), (⇑(single R i_1) : (a : M) → PolynomialModule R M) '' (↑(F.N i_1) : Set M)))
    (Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))

Tactic:
simp [Set.biUnion_le_eq_iUnion]

Premises used: Set.biUnion_le_eq_iUnion
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
mpr :
  Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
    (Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
⊢ F.submodule.FG

Tactic:
rw [hn]
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
mpr :
  Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
    (⨆ (x : Subtype (Membership.mem (Finset.range n.succ))),
      Submodule.span (↥(reesAlgebra I))
        ((⇑(single R (↑x : ℕ)) : (a : M) → PolynomialModule R M) '' (↑(F.N (↑x : ℕ)) : Set M)))
⊢ Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
    (Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))

Tactic:
simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']

Premises used: iSup_subtype', Finset.mem_range_succ_iff, Submodule.span_iUnion₂
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
mpr :
  ∀ (i : Subtype (Membership.mem (Finset.range n.succ))),
    Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
      (Submodule.span (↥(reesAlgebra I))
        ((⇑(single R (↑i : ℕ)) : (a : M) → PolynomialModule R M) '' (↑(F.N (↑i : ℕ)) : Set M)))
⊢ Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
    (⨆ (x : Subtype (Membership.mem (Finset.range n.succ))),
      Submodule.span (↥(reesAlgebra I))
        ((⇑(single R (↑x : ℕ)) : (a : M) → PolynomialModule R M) '' (↑(F.N (↑x : ℕ)) : Set M)))

Tactic:
apply Submodule.fg_iSup

Premises used: Submodule.fg_iSup
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
mpr :
  ∀ (s : Finset M) (hs : Submodule.span R (↑s : Set M) = F.N i),
    Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
      (Submodule.span (↥(reesAlgebra I))
        ((⇑(single R (↑(Subtype.mk (p := Membership.mem (Finset.range n.succ)) i hi) : ℕ)) :
            (a : M) → PolynomialModule R M) ''
          (↑(F.N (↑(Subtype.mk (p := Membership.mem (Finset.range n.succ)) i hi) : ℕ)) : Set M)))
⊢ Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
    (Submodule.span (↥(reesAlgebra I))
      ((⇑(single R (↑(Subtype.mk (p := Membership.mem (Finset.range n.succ)) i hi) : ℕ)) :
          (a : M) → PolynomialModule R M) ''
        (↑(F.N (↑(Subtype.mk (p := Membership.mem (Finset.range n.succ)) i hi) : ℕ)) : Set M)))

Tactic:
obtain ⟨s, hs⟩ := hF' i
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R (↑s : Set M) = F.N i
rw :
  Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I) (↑(Submodule.map (lsingle R i) (F.N i)) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
⊢ Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))

Tactic:
rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]

Premises used: Submodule.span_span_of_tower, Finset.coe_image, Submodule.map_span
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R (↑s : Set M) = F.N i
⊢ Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I) (↑(Submodule.map (lsingle R i) (F.N i)) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R (↑s : Set M) = F.N i
⊢ Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))

Tactic:
have : Submodule.span (reesAlgebra I) (s.image (lsingle R i) : Set (PolynomialModule R M)) =
        Submodule.span _ (single R i '' (F.N i : Set M)) := by
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]; rfl
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R (↑s : Set M) = F.N i
this :
  Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
mpr :
  Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))
⊢ Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I)) (M := PolynomialModule R M)
    (Submodule.span (↥(reesAlgebra I))
      ((⇑(single R (↑(Subtype.mk (p := Membership.mem (Finset.range n.succ)) i hi) : ℕ)) :
          (a : M) → PolynomialModule R M) ''
        (↑(F.N (↑(Subtype.mk (p := Membership.mem (Finset.range n.succ)) i hi) : ℕ)) : Set M)))

Tactic:
rw [Subtype.coe_mk, ← this]

Premises used: Subtype.coe_mk
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R (↑s : Set M) = F.N i
this :
  Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
⊢ Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))

Tactic:
⟨_, rfl⟩

Premises used: Submodule.FG, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn :
  F.submodule =
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R (↑s : Set M) = F.N i
this :
  Eq (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))
    (Submodule.span (↥(reesAlgebra I)) ((⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
⊢ Submodule.FG.{u_1, u_2} (R := ↥(reesAlgebra I))
    (Submodule.span ↥(reesAlgebra I)
      (↑(Finset.image (⇑(lsingle R i) : (a : M) → PolynomialModule R M) s) : Set (PolynomialModule R M)))

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
delta : F.submodule.FG ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
delta₁ :
  F.submodule.FG ↔
    ∃ (n₀ : ℕ),
      F.submodule =
        Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
mp :
  F.submodule.FG →
    ∃ (n₀ : ℕ),
      F.submodule =
        Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
mpr mpr₁ :
  (∃ (n₀ : ℕ),
      F.submodule =
        Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) →
    F.submodule.FG
⊢ F.submodule.FG ↔ F.Stable

Tactic:
classical
  delta Ideal.Filtration.Stable
  simp_rw [← F.submodule_eq_span_le_iff_stable_ge]
  constructor
  · rintro H
    refine H.stabilizes_of_iSup_eq
        ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_
    · intro n m e
      rw [Submodule.span_le, Set.iUnion₂_subset_iff]
      intro i hi
      refine Set.Subset.trans ?_ Submodule.subset_span
      refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
      exact hi.trans e
    · dsimp
      rw [← Submodule.span_iUnion, ← submodule_span_single]
      simp [Set.biUnion_le_eq_iUnion]
  · rintro ⟨n, hn⟩
    rw [hn]
    simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']
    apply Submodule.fg_iSup
    rintro ⟨i, hi⟩
    obtain ⟨s, hs⟩ := hF' i
    have : Submodule.span (reesAlgebra I) (s.image (lsingle R i) : Set (PolynomialModule R M)) =
        Submodule.span _ (single R i '' (F.N i : Set M)) := by
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]; rfl
    rw [Subtype.coe_mk, ← this]
    exact ⟨_, rfl⟩

Premises used: Subtype.coe_mk, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, Set.Subset.trans, iSup_subtype', Finset.mem_range_succ_iff, Submodule.fg_iSup, Ideal.Filtration.submodule_span_single, Submodule.span_iUnion, Ideal.Filtration.Stable, Submodule.subset_span, Set.biUnion_le_eq_iUnion, Set.iUnion₂_subset_iff, Submodule.span_le, Submodule.span_iUnion₂
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
rw : ∀ (hF : F.submodule.FG) {F' : I.Filtration M} (hf : F' ≤ F), F'.submodule.FG
hF' : ∀ (hF : F.submodule.FG) {F' : I.Filtration M} (hf : F' ≤ F) (i : ℕ), (F'.N i).FG
hF'₁ : ∀ (i : ℕ), (F.N i).FG
⊢ F'.Stable

Tactic:
rw [← submodule_fg_iff_stable] at hF ⊢

Premises used: Ideal.Filtration.submodule_fg_iff_stable
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F'.N i).FG

Tactic:
IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F'.N i).FG

Tactic:
exact IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F.N i).FG

Tactic:
IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F.N i).FG

Tactic:
exact IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ IsNoetherian.{u_1, u_2} ↥(reesAlgebra I) ↥F.submodule

Tactic:
have := isNoetherian_of_fg_of_noetherian _ hF
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : IsNoetherian.{u_1, u_2} ↥(reesAlgebra I) ↥F.submodule
⊢ ∀ s ≤ F.submodule, s.FG

Tactic:
rw [isNoetherian_submodule] at this

Premises used: isNoetherian_submodule
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : ∀ s ≤ F.submodule, s.FG
⊢ F'.submodule.FG

Tactic:
this _ (OrderHomClass.mono (submoduleInfHom M I) hf)

Premises used: Ideal.Filtration.submoduleInfHom, OrderHomClass.mono
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : ∀ s ≤ F.submodule, s.FG
⊢ F'.submodule.FG

Tactic:
exact this _ (OrderHomClass.mono (submoduleInfHom M I) hf)

Premises used: Ideal.Filtration.submoduleInfHom, OrderHomClass.mono
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.Stable
⊢ (F ⊓ F').Stable

Tactic:
hF.of_le inf_le_left

Premises used: Ideal.Filtration.Stable.of_le, inf_le_left
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
hF : F.Stable
⊢ (F' ⊓ F).Stable

Tactic:
hF.of_le inf_le_right

Premises used: inf_le_right, Ideal.Filtration.Stable.of_le
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
N : Submodule R M
⊢ ∃ (k : ℕ),
    ∀ n ≥ k,
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤ ⊓ N = I ^ (n - k) • (HSMul.hSMul (β := Submodule R M) (I ^ k) ⊤ ⊓ N)

Tactic:
((I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)).exists_pow_smul_eq_of_ge

Premises used: Ideal.trivialFiltration, Ideal.stableFiltration_stable, Set.Mem, Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, Ideal.Filtration.Stable.inter_right, Top.top
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
k : ℕ
⊢ HSMul.hSMul (β := Submodule R M) (I ^ k) ⊤ = Filtration.N (I.stableFiltration ⊤) k

Tactic:
simp
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
⊢ ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N

Tactic:
have hN : ∀ k, (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N :=
    fun k => inf_eq_right.mpr ((iInf_le _ k).trans <| le_of_eq <| by simp)