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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
have h : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
Tactic: use n₀
-- 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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
ih : F.N (n₀ + n) = I ^ n • F.N n₀
⊢ F.N (n₀ + (n + 1)) = I ^ (n + 1) • F.N n₀
have h : n₀ + n ≥ n₀
Tactic: rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]
-- 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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
k : ℕ
⊢ F.N (n₀ + k) = I ^ k • F.N n₀
have h : F.N (n₀ + 0) = HPow.hPow (β := ℕ) I 0 • F.N n₀
Tactic: induction k with
  | zero => simp
  | succ _ ih => rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]; lia
Cleared hypotheses: k
-- 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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
k : ℕ
h : F.N (n₀ + 0) = HPow.hPow (β := ℕ) I 0 • F.N n₀
⊢ F.N (n₀ + k) = I ^ k • F.N n₀
have h₁ : ∀ (n : ℕ) (ih : F.N (n₀ + n) = I ^ n • F.N n₀), F.N (n₀ + (n + 1)) = I ^ (n + 1) • F.N n₀
Tactic: induction k with
  | zero => simp
  | succ _ ih => rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]; lia
Cleared hypotheses: k
-- 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
h : F.Stable
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
have obtain : ∀ (n₀ : ℕ) (hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀), ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
Tactic: obtain ⟨n₀, hn₀⟩ := h.exists_pow_smul_eq
-- 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
have h₁ : ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
Tactic: use n₀
-- 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ F.N n = I ^ (n - n₀) • F.N n₀
have h₁ : n = n₀ + (n - n₀)
Tactic: convert! hn₀ (n - n₀)
-- 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n₀ + (n - n₀)
have h₁ : n = n - n₀ + n₀
Tactic: rw [add_comm, tsub_add_cancel_of_le 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
h₁ : n = n - n₀ + n₀
⊢ n = n₀ + (n - n₀)
have h₂ : n = n
Tactic: rw [add_comm, tsub_add_cancel_of_le 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
⊢ F.Stable ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
have refine : ∀ (h : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀) (n : ℕ)
  (hn : n ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)), I • F.N n = F.N (n + 1)
Tactic: refine ⟨Stable.exists_pow_smul_eq_of_ge, fun h => ⟨h.choose, fun n 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
h : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)
⊢ I • F.N n = F.N (n + 1)
have rw : I •
    I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
  F.N (n + 1)
Tactic: rw [h.choose_spec n hn, h.choose_spec (n + 1) (by lia), smul_smul, ← pow_succ',
    tsub_add_eq_add_tsub 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
h : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)
rw :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    F.N (n + 1)
⊢ I • F.N n = F.N (n + 1)
have rw₁ : I •
    I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
  I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
Tactic: rw [h.choose_spec n hn, h.choose_spec (n + 1) (by lia), smul_smul, ← pow_succ',
    tsub_add_eq_add_tsub 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
h : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)
rw :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    F.N (n + 1)
rw₁ :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
⊢ I • F.N n = F.N (n + 1)
have rw₂ : (I * I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
  I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
Tactic: rw [h.choose_spec n hn, h.choose_spec (n + 1) (by lia), smul_smul, ← pow_succ',
    tsub_add_eq_add_tsub 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
h : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)
rw :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    F.N (n + 1)
rw₁ :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
rw₂ :
  (I * I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
⊢ I • F.N n = F.N (n + 1)
have rw₃ : I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀) + 1) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
  I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
Tactic: rw [h.choose_spec n hn, h.choose_spec (n + 1) (by lia), smul_smul, ← pow_succ',
    tsub_add_eq_add_tsub 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
h : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)
rw :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    F.N (n + 1)
rw₁ :
  I •
      I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
        F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
rw₂ :
  (I * I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
rw₃ :
  I ^ (n - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀) + 1) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
    I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
      F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
⊢ I • F.N n = F.N (n + 1)
have rw₄ : I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) =
  I ^ (n + 1 - h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)) •
    F.N (h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀))
Tactic: rw [h.choose_spec n hn, h.choose_spec (n + 1) (by lia), smul_smul, ← pow_succ',
    tsub_add_eq_add_tsub 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 F' : I.Filtration M
h : F.Stable
e : F.N 0 ≤ F'.N 0
⊢ ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
have obtain : ∀ (n₀ : ℕ) (hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)), ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
Tactic: obtain ⟨n₀, hF⟩ := h
Cleared hypotheses: h
-- 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
have h : ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
Tactic: use n₀
-- 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ F.N (0 + n₀) ≤ F'.N 0
have h : 0 ≤ 0 + n₀
Tactic: refine (F.antitone ?_).trans e
-- 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ F.N (n + 1 + n₀) ≤ F'.N (n + 1)
have h : I • F.N (n + n₀) ≤ F'.N (n + 1)
Tactic: rw [add_right_comm, ← 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
h : I • F.N (n + n₀) ≤ F'.N (n + 1)
⊢ F.N (n + 1 + n₀) ≤ F'.N (n + 1)
have h₁ : n + n₀ ≥ n₀
Tactic: rw [add_right_comm, ← 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
⊢ F.N (n + n₀) ≤ F'.N n
have h : F.N (0 + n₀) ≤ F'.N 0
Tactic: induction n with
  | zero => refine (F.antitone ?_).trans e; simp
  | succ n hn =>
    rw [add_right_comm, ← hF]
    · exact (smul_mono_right _ hn).trans (F'.smul_le _)
    simp
Cleared hypotheses: n
-- 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
h : F.N (0 + n₀) ≤ F'.N 0
⊢ F.N (n + n₀) ≤ F'.N n
have h₁ : ∀ (n : ℕ) (hn : F.N (n + n₀) ≤ F'.N n), F.N (n + 1 + n₀) ≤ F'.N (n + 1)
Tactic: induction n with
  | zero => refine (F.antitone ?_).trans e; simp
  | succ n hn =>
    rw [add_right_comm, ← hF]
    · exact (smul_mono_right _ hn).trans (F'.smul_le _)
    simp
Cleared hypotheses: n
-- 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 F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
⊢ ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
have obtain : ∀ (n₁ : ℕ) (h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n), ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
Tactic: obtain ⟨n₁, h₁⟩ := h.exists_forall_le (le_of_eq e)
-- 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 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₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
have obtain : ∀ (n₂ : ℕ) (h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n), ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
Tactic: obtain ⟨n₂, h₂⟩ := h'.exists_forall_le (le_of_eq e.symm)
-- 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 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 : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
have h₃ : ∀ (n : ℕ), F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n
Tactic: use max n₁ n₂
-- 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 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
have h₃ : n + n₁ ≤ n + max n₁ n₂
Tactic: refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩
-- 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 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₂
⊢ F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n
have h₄ : n + n₂ ≤ n + max n₁ n₂
Tactic: refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩
-- 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 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 : ℕ
⊢ Membership.mem (α := M) (F.N i) ((r • f : (a : ℕ) → M) i : M)
have 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
Tactic: rw [Subalgebra.smul_def, PolynomialModule.smul_apply]
-- 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 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 : ℕ
⊢ ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
      HSMul.hSMul (β := M) ((↑r : R[X]).coeff x.1) ((f : (a : ℕ) → M) x.2 : M) ∈
    F.N i
have 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
Tactic: apply Submodule.sum_mem
-- 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 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
⊢ HSMul.hSMul (β := M) ((↑r : R[X]).coeff (j, k).1) ((f : (a : ℕ) → M) (j, k).2 : M) ∈ F.N i
have e₁ : (j, k).1 + (j, k).2 = i
Tactic: rw [Finset.mem_antidiagonal] at e
Cleared hypotheses: e
-- 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 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
⊢ HSMul.hSMul (β := M) ((↑r : R[X]).coeff (j, k).1) ((f : (a : ℕ) → M) (j, k).2 : M) ∈ F.N i
have 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)
Tactic: subst e
Cleared hypotheses: i, e
-- 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 F' : I.Filtration M
⊢ (F ⊓ F').submodule = F.submodule ⊓ F'.submodule
have h : ∀ (x : PolynomialModule R M), x ∈ (F ⊓ F').submodule ↔ x ∈ F.submodule ⊓ F'.submodule
Tactic: ext
-- 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
⊢ AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule.toAddSubmonoid
have a : AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ≤
  F.submodule.toAddSubmonoid
Tactic: apply le_antisymm
-- 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
a :
  AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ≤
    F.submodule.toAddSubmonoid
⊢ AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule.toAddSubmonoid
have a₁ : F.submodule.toAddSubmonoid ≤
  AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
Tactic: apply le_antisymm
-- 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
⊢ AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ≤
    F.submodule.toAddSubmonoid
have a : ∀ (i : ℕ),
  (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
    (↑F.submodule.toAddSubmonoid : Set (PolynomialModule R M))
Tactic: rw [AddSubmonoid.closure_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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
⊢ Membership.mem (α := M) (F.N j)
    ((((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) : (a : ℕ) → M) j : M)
have a : (if i = j then m else 0) ∈ F.N j
Tactic: rw [single_apply]
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
⊢ (if i = j then m else 0) ∈ F.N j
have pos : ∀ (h : i = j), m ∈ F.N j
Tactic: split_ifs with h
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
pos : ∀ (h : i = j), m ∈ F.N j
⊢ (if i = j then m else 0) ∈ F.N j
have neg : ∀ (h : ¬i = j), 0 ∈ F.N j
Tactic: split_ifs with h
-- 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
i : ℕ
m : M
hm : m ∈ (↑(F.N i) : Set M)
j : ℕ
h : i = j
⊢ m ∈ F.N j
have pos : m ∈ F.N i
Tactic: rwa [← h]
-- 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
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ Membership.mem (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) f
have 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)
Tactic: rw [← f.sum_single]