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 F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
h₃ : ∀ (n : ℕ), F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n
⊢ ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Tactic:
use max n₁ n₂

Premises used: Max.max
-- 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
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n

Tactic:
⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩

Premises used: Ideal.Filtration.antitone, And.intro, 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 F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
h₃ : n + n₁ ≤ n + max n₁ n₂
h₄ : n + n₂ ≤ n + max n₁ n₂
⊢ F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n

Tactic:
refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩
-- 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
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ n + n₁ ≤ n + max n₁ n₂

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
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ n + n₂ ≤ n + max n₁ n₂

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
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf :
  Membership.mem (γ := Set (PolynomialModule R M))
    {f : PolynomialModule R M | ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)} f
i : ℕ
rw :
  ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
      HSMul.hSMul (β := M) ((↑r : R[X]).coeff x.1) ((f : (a : ℕ) → M) x.2 : M) ∈
    F.N i
⊢ Membership.mem (α := M) (F.N i) ((r • f : (a : ℕ) → M) i : M)

Tactic:
rw [Subalgebra.smul_def, PolynomialModule.smul_apply]

Premises used: PolynomialModule.smul_apply, Subalgebra.smul_def
-- 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
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf :
  Membership.mem (γ := Set (PolynomialModule R M))
    {f : PolynomialModule R M | ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)} f
i : ℕ
a :
  ∀ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
    HSMul.hSMul (β := M) ((↑r : R[X]).coeff c.1) ((f : (a : ℕ) → M) c.2 : M) ∈ F.N i
⊢ ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
      HSMul.hSMul (β := M) ((↑r : R[X]).coeff x.1) ((f : (a : ℕ) → M) x.2 : M) ∈
    F.N i

Tactic:
apply Submodule.sum_mem

Premises used: Submodule.sum_mem
-- 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
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf :
  Membership.mem (γ := Set (PolynomialModule R M))
    {f : PolynomialModule R M | ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)} f
i j k : ℕ
e : (j, k) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ (j, k).1 + (j, k).2 = i

Tactic:
rw [Finset.mem_antidiagonal] at e

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf :
  Membership.mem (γ := Set (PolynomialModule R M))
    {f : PolynomialModule R M | ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)} f
i j k : ℕ
e : (j, k).1 + (j, k).2 = i
a : HSMul.hSMul (β := M) ((↑r : R[X]).coeff (j, k).1) ((f : (a : ℕ) → M) (j, k).2 : M) ∈ F.N ((j, k).1 + (j, k).2)
⊢ HSMul.hSMul (β := M) ((↑r : R[X]).coeff (j, k).1) ((f : (a : ℕ) → M) (j, k).2 : M) ∈ F.N i

Tactic:
subst e
-- 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
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf :
  Membership.mem (γ := Set (PolynomialModule R M))
    {f : PolynomialModule R M | ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)} f
j k : ℕ
⊢ HSMul.hSMul (β := M) ((↑r : R[X]).coeff (j, k).1) ((f : (a : ℕ) → M) (j, k).2 : M) ∈ F.N ((j, k).1 + (j, k).2)

Tactic:
F.pow_smul_le j k (Submodule.smul_mem_smul (r.2 j) (hf k))

Premises used: Set.Mem, Ideal.Filtration.pow_smul_le, Submodule.smul_mem_smul, Subtype.property
-- 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
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf :
  Membership.mem (γ := Set (PolynomialModule R M))
    {f : PolynomialModule R M | ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)} f
j k : ℕ
⊢ HSMul.hSMul (β := M) ((↑r : R[X]).coeff (j, k).1) ((f : (a : ℕ) → M) (j, k).2 : M) ∈ F.N ((j, k).1 + (j, k).2)

Tactic:
exact F.pow_smul_le j k (Submodule.smul_mem_smul (r.2 j) (hf k))

Premises used: Ideal.Filtration.pow_smul_le, Submodule.smul_mem_smul, Subtype.property
-- 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
f : PolynomialModule R M
⊢ f ∈ F.submodule ↔ ∀ (i : ℕ), Membership.mem (α := M) (F.N i) ((f : (a : ℕ) → M) i : M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
h : ∀ (x : PolynomialModule R M), x ∈ (F ⊓ F').submodule ↔ x ∈ F.submodule ⊓ F'.submodule
⊢ (F ⊓ F').submodule = F.submodule ⊓ F'.submodule

Tactic:
ext
-- 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
x : PolynomialModule R M
⊢ x ∈ (F ⊓ F').submodule ↔ x ∈ F.submodule ⊓ F'.submodule

Tactic:
forall_and

Premises used: Set.Mem, setOf, Set.inter, forall_and
-- 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
x : PolynomialModule R M
⊢ x ∈ (F ⊓ F').submodule ↔ x ∈ F.submodule ⊓ F'.submodule

Tactic:
exact forall_and

Premises used: forall_and
-- 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
a :
  AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ≤
    F.submodule.toAddSubmonoid
a₁ :
  F.submodule.toAddSubmonoid ≤
    AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
⊢ AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule.toAddSubmonoid

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
a :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑F.submodule.toAddSubmonoid : Set (PolynomialModule R M))
⊢ AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ≤
    F.submodule.toAddSubmonoid

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

Premises used: Set.iUnion_subset_iff, AddSubmonoid.closure_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
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
a : (if i = j then m else 0) ∈ F.N j
⊢ Membership.mem (α := M) (F.N j)
    ((((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) : (a : ℕ) → M) j : M)

Tactic:
rw [single_apply]

Premises used: PolynomialModule.single_apply
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
pos : ∀ (h : i = j), m ∈ F.N j
neg : ∀ (h : ¬i = j), 0 ∈ F.N j
⊢ (if i = j then m else 0) ∈ F.N j

Tactic:
split_ifs with h
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
h : i = j
pos pos₁ pos₂ pos₃ : m ∈ F.N i
⊢ m ∈ F.N j

Tactic:
rwa [← h]
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
h : ¬i = j
⊢ 0 ∈ F.N j

Tactic:
(F.N j).zero_mem

Premises used: Set.Mem, Submodule.zero_mem, Ideal.Filtration.N
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
h : ¬i = j
⊢ 0 ∈ F.N j

Tactic:
exact (F.N j).zero_mem

Premises used: Submodule.zero_mem, Ideal.Filtration.N
-- 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
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
a :
  Membership.mem (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
    (Finsupp.sum f Finsupp.single)
⊢ Membership.mem (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) f

Tactic:
rw [← f.sum_single]

Premises used: Finsupp.sum_single
-- 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
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
apply :
  ∀ c ∈ f.support,
    Membership.mem (α := PolynomialModule R M) (γ := AddSubmonoid (PolynomialModule R M))
      (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
      (Finsupp.single c ((f : (a : ℕ) → M) c) : ℕ →₀ M)
⊢ Membership.mem (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
    (Finsupp.sum f Finsupp.single)

Tactic:
apply AddSubmonoid.sum_mem _ _

Premises used: AddSubmonoid.sum_mem
-- 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
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
c : ℕ
⊢ Membership.mem (α := PolynomialModule R M) (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
    (Finsupp.single c ((f : (a : ℕ) → M) c) : ℕ →₀ M)

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

Premises used: Set.Mem, AddSubmonoid.subset_closure, Set.subset_iUnion, Set.mem_image_of_mem
-- 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
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
c : ℕ
⊢ Membership.mem (α := PolynomialModule R M) (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
    (Finsupp.single c ((f : (a : ℕ) → M) c) : ℕ →₀ M)

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

Premises used: AddSubmonoid.subset_closure, 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
rw : Submodule.span ↥(reesAlgebra I) (↑F.submodule : Set (PolynomialModule R M)) = F.submodule
⊢ Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule

Tactic:
rw [← Submodule.span_closure, submodule_closure_single, Submodule.coe_toAddSubmonoid]

Premises used: Ideal.Filtration.submodule_closure_single, Submodule.coe_toAddSubmonoid, Submodule.span_closure
-- 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
⊢ Submodule.span ↥(reesAlgebra I) (↑F.submodule : Set (PolynomialModule R M)) = F.submodule

Tactic:
Submodule.span_eq (Filtration.submodule F)

Premises used: Ideal.Filtration.submodule, Submodule.span_eq
-- 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
⊢ Submodule.span ↥(reesAlgebra I) (↑F.submodule : Set (PolynomialModule R M)) = F.submodule

Tactic:
exact Submodule.span_eq (Filtration.submodule F)

Premises used: Ideal.Filtration.submodule, Submodule.span_eq
-- 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
n₀ : ℕ
rw :
  (∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
rw [← submodule_span_single,
    ← (Submodule.span_mono (Set.iUnion₂_subset_iUnion _ _)).ge_iff_eq',
    Submodule.span_le, Set.iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff, Ideal.Filtration.submodule_span_single, LE.le.ge_iff_eq', Set.iUnion₂_subset_iUnion, Submodule.span_mono, Submodule.span_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
F : I.Filtration M
n₀ : ℕ
mp :
  (∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))) →
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
mpr :
  (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))
⊢ (∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
constructor
-- 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
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
⊢ I • F.N n = F.N (n + 1)

Tactic:
(F.smul_le n).antisymm ?_

Premises used: Ideal.Filtration.smul_le, LE.le.antisymm
-- 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
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
mp : F.N (n + 1) ≤ I • F.N n
⊢ I • F.N n = F.N (n + 1)

Tactic:
refine (F.smul_le n).antisymm ?_

Premises used: Ideal.Filtration.smul_le, LE.le.antisymm
-- 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
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
mp :
  ∀
    (l :
      Finsupp.{u_2, u_1}
        (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
          Type u_2)
        ↥(reesAlgebra I))
    (hl :
      Eq.{u_2 + 1} (α := PolynomialModule R M)
        ((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M)
        ((single R (n + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M)),
    x ∈ I • F.N n
⊢ x ∈ I • F.N n

Tactic:
obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp (H _ ⟨x, hx, rfl⟩)

Premises used: Finsupp.mem_span_iff_linearCombination, And.intro, Exists.intro, Iff.mp, 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
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  Eq.{u_2 + 1} (α := PolynomialModule R M)
    ((Finsupp.linearCombination (↥(reesAlgebra I))
            (Subtype.val (p := fun (x : PolynomialModule R M) ↦
              Membership.mem (γ := Set (PolynomialModule R M))
                (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                x)) :
          (a :
              (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                  Type u_2) →₀
                ↥(reesAlgebra I)) →
            PolynomialModule R M)
        l :
      PolynomialModule R M)
    ((single R (n + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M)
⊢ Eq.{u_2 + 1} (α := M)
    ((fun (f : ℕ →₀ M) ↦ ((f : (a : ℕ) → M) (n + 1) : M))
      ((Finsupp.linearCombination (↥(reesAlgebra I))
            (Subtype.val (p := fun (x : PolynomialModule R M) ↦
              Membership.mem (γ := Set (PolynomialModule R M))
                (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                x)) :
          (a :
              (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                  Type u_2) →₀
                ↥(reesAlgebra I)) →
            PolynomialModule R M)
        l))
    ((fun (f : ℕ →₀ M) ↦ ((f : (a : ℕ) → M) (n + 1) : M)) ((single R (n + 1) : (a : M) → PolynomialModule R M) x))

Tactic:
replace hl := congr_arg (fun f : ℕ →₀ M => f (n + 1)) hl
-- 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
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  Eq (α := M)
    ((((Finsupp.linearCombination (↥(reesAlgebra I))
                  (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                    Membership.mem (γ := Set (PolynomialModule R M))
                      (⋃ (i : ℕ),
                        ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                      x)) :
                (a :
                    (↑(⋃ (i : ℕ),
                            ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                        Type u_2) →₀
                      ↥(reesAlgebra I)) →
                  PolynomialModule R M)
              l :
            PolynomialModule R M) :
          (a : ℕ) → M)
        (n + 1) :
      M)
    ((((single R (n + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M) : (a : ℕ) → M) (n + 1) : M)
⊢ (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x

Tactic:
rw [PolynomialModule.single_apply, if_pos rfl] at hl

Premises used: PolynomialModule.single_apply, if_pos, rfl