awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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
⊢ LE.le.{u_2} (α := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R 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)))
      n)
    ((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)
have mp : ∀ (i : ℕ) (j : 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: rw [Submodule.span_le, Set.iUnion₂_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
have 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))
Tactic: refine Set.Subset.trans ?_ Submodule.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
have mp : i ≤ m
Tactic: refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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₀ : ℕ),
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule
have 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)))
Tactic: rw [← Submodule.span_iUnion, ← submodule_span_single]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
⊢ F.submodule.FG
have 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)))
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
⊢ 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)))
have 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)))
Tactic: simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
⊢ 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)))
have 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)))
Tactic: apply Submodule.fg_iSup
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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
⊢ 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)))
have 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)))
Tactic: obtain ⟨s, hs⟩ := hF' i
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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)))
have 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)))
Tactic: rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
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
⊢ 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)))
have 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)))
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
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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)) (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)))
have 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)))
Tactic: rw [Subtype.coe_mk, ← this]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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
⊢ F.submodule.FG ↔ F.Stable
have delta : F.submodule.FG ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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)
⊢ F.submodule.FG ↔ F.Stable
have 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))
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
⊢ F.submodule.FG ↔ F.Stable
have 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))
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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))
⊢ F.submodule.FG ↔ F.Stable
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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
⊢ F'.Stable
have rw : ∀ (hF : F.submodule.FG) {F' : I.Filtration M} (hf : F' ≤ F), F'.submodule.FG
Tactic: rw [← submodule_fg_iff_stable] at hF ⊢
Cleared hypotheses: hF, F', hf
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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
⊢ F'.Stable
have hF' : ∀ (hF : F.submodule.FG) {F' : I.Filtration M} (hf : F' ≤ F) (i : ℕ), (F'.N i).FG
Tactic: rw [← submodule_fg_iff_stable] at hF ⊢
Cleared hypotheses: hF, F', hf
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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
⊢ F'.Stable
have hF'₁ : ∀ (i : ℕ), (F.N i).FG
Tactic: rw [← submodule_fg_iff_stable] at hF ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
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
⊢ F'.submodule.FG
have this : IsNoetherian.{u_1, u_2} ↥(reesAlgebra I) ↥F.submodule
Tactic: have := isNoetherian_of_fg_of_noetherian _ hF
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
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
⊢ F'.submodule.FG
have this₁ : ∀ s ≤ F.submodule, s.FG
Tactic: rw [isNoetherian_submodule] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
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) ⊤
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
have hN : ∀ (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)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
have mp : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x →
  ∃ (r : ↥I), (↑r : R) • x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
mp :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x →
    ∃ (r : ↥I), (↑r : R) • x = x
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
have mpr : (∃ (r : ↥I), (↑r : R) • x = x) →
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
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) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ N ≤ I • N
have obtain : ∀ (k : ℕ)
  (hk :
    ∀ n ≥ k,
      I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n =
        (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)),
  N ≤ I • N
Tactic: obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)