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_1 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
F : I.Filtration M
hF : F ∈ S
⊢ ∃ (b : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i) b ∧
      (fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1))
          (Subtype.mk (p := fun (x : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) ↦ x ∈ N '' S) F.N ⋯) ≤
        b

Tactic:
exact ⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono 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 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
rw :
  LE.le.{u_2} (α := Submodule R M) (⨆ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
    (⨆ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))
⊢ I • sSup (N '' S) i ≤ sSup (N '' S) (i + 1)

Tactic:
rw [sSup_eq_iSup', iSup_apply, Submodule.smul_iSup, iSup_apply]

Premises used: Submodule.smul_iSup, iSup_apply, sSup_eq_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 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
apply : ∀ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i ≤ (↑i_1 : ℕ → Submodule R M) (i + 1)
⊢ LE.le.{u_2} (α := Submodule R M) (⨆ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
    (⨆ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))

Tactic:
apply iSup_mono _

Premises used: iSup_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_1 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
F : I.Filtration M
hF : F ∈ S
⊢ I • (↑(Subtype.mk (p := fun (x : ℕ → Submodule R M) ↦ x ∈ N '' S) F.N ⋯) : ℕ → Submodule R M) i ≤
    (↑(Subtype.mk (p := fun (x : ℕ → Submodule R M) ↦ x ∈ N '' S) F.N ⋯) : ℕ → Submodule R M) (i + 1)

Tactic:
F.smul_le i

Premises used: Ideal.Filtration.smul_le, Set.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_1 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
F : I.Filtration M
hF : F ∈ S
⊢ I • (↑(Subtype.mk (p := fun (x : ℕ → Submodule R M) ↦ x ∈ N '' S) F.N ⋯) : ℕ → Submodule R M) i ≤
    (↑(Subtype.mk (p := fun (x : ℕ → Submodule R M) ↦ x ∈ N '' S) F.N ⋯) : ℕ → Submodule R M) (i + 1)

Tactic:
exact F.smul_le i

Premises used: Ideal.Filtration.smul_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 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
apply :
  IsCoinitialFor.{u_2} (α := Submodule R M)
    (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i)
    (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1))
⊢ sInf (N '' S) (i + 1) ≤ sInf (N '' S) i

Tactic:
apply sInf_le_sInf_of_isCoinitialFor _

Premises used: sInf_le_sInf_of_isCoinitialFor
-- 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_1 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
F : I.Filtration M
hF : F ∈ S
⊢ ∃ (b : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1)) b ∧
      b ≤
        (fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i)
          (Subtype.mk (p := fun (x : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) ↦ x ∈ N '' S) F.N ⋯)

Tactic:
⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono i⟩

Premises used: Subtype.mk, And.intro, Ideal.Filtration.mono, 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_1 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
F : I.Filtration M
hF : F ∈ S
⊢ ∃ (b : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1)) b ∧
      b ≤
        (fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i)
          (Subtype.mk (p := fun (x : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) ↦ x ∈ N '' S) F.N ⋯)

Tactic:
exact ⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono 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 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ HSMul.hSMul (β := Submodule R M) I (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) i) ≤
    ⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1)

Tactic:
smul_iInf_le.trans ?_

Premises used: Set.Mem, smul_iInf_le, 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
S : Set (I.Filtration M)
i : ℕ
refine :
  LE.le.{u_2} (α := Submodule R M) (⨅ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
    (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))
⊢ HSMul.hSMul (β := Submodule R M) I (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) i) ≤
    ⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1)

Tactic:
refine smul_iInf_le.trans ?_

Premises used: smul_iInf_le, 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
S : Set (I.Filtration M)
i : ℕ
apply : ∀ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i ≤ (↑i_1 : ℕ → Submodule R M) (i + 1)
⊢ LE.le.{u_2} (α := Submodule R M) (⨅ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
    (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))

Tactic:
apply iInf_mono _

Premises used: iInf_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
⊢ (F ⊔ F').N = F.N ⊔ F'.N

Tactic:
rfl

Premises used: 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
S : Set (I.Filtration M)
⊢ (sSup S).N = sSup (N '' S)

Tactic:
rfl

Premises used: 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 F' : I.Filtration M
⊢ (F ⊓ F').N = F.N ⊓ F'.N

Tactic:
rfl

Premises used: 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
S : Set (I.Filtration M)
⊢ (sInf S).N = sInf (N '' S)

Tactic:
rfl

Premises used: 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
⊢ Eq.{u_2 + 1} (α := ℕ → Submodule R M) (N (I := I) ⊤) ⊤

Tactic:
rfl

Premises used: 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
⊢ Eq.{u_2 + 1} (α := ℕ → Submodule R M) (N (I := I) ⊥) ⊥

Tactic:
rfl

Premises used: 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
ι : Sort u_3
f : ι → I.Filtration M
⊢ (iSup f).N = ⨆ (i : ι), (f i).N

Tactic:
congr_arg sSup (Set.range_comp _ _).symm

Premises used: Set.range_comp, iSup, congr_arg, Eq.symm, SupSet.sSup
-- 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
ι : Sort u_3
f : ι → I.Filtration M
⊢ (iInf f).N = ⨅ (i : ι), (f i).N

Tactic:
congr_arg sInf (Set.range_comp _ _).symm

Premises used: Set.range_comp, iInf, congr_arg, Eq.symm, InfSet.sInf
-- 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_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
rw : HPow.hPow (β := ℕ) I 1 • I ^ i • N ≤ I ^ i • N
⊢ I ^ (i + 1) • N ≤ I ^ i • N

Tactic:
rw [add_comm, pow_add, mul_smul]

Premises used: pow_add, add_comm, SemigroupAction.mul_smul
-- 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_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ HPow.hPow (β := ℕ) I 1 • I ^ i • N ≤ I ^ i • N

Tactic:
Submodule.smul_le_right

Premises used: Set.Mem, Submodule.smul_le_right
-- 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_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ HPow.hPow (β := ℕ) I 1 • I ^ i • N ≤ I ^ i • N

Tactic:
exact Submodule.smul_le_right

Premises used: Submodule.smul_le_right
-- 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_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
rw : I • I ^ i • N ≤ I ^ (1 + i) • N
rw₁ : I • I ^ i • N ≤ (HPow.hPow (β := ℕ) I 1 * I ^ i) • N
rw₂ : I • I ^ i • N ≤ HPow.hPow (β := ℕ) I 1 • I ^ i • N
rw₃ rw₄ : I • I ^ i • N ≤ I • I ^ i • N
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N

Tactic:
rw [add_comm, pow_add, mul_smul, pow_one]

Premises used: pow_add, add_comm, pow_one, SemigroupAction.mul_smul
-- 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
N : Submodule R M
h : ∀ n ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
⊢ (I.stableFiltration N).Stable

Tactic:
use 0
-- 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
N : Submodule R M
n : ℕ
h : n ≥ 0 → I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
⊢ n ≥ 0 → I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)

Tactic:
_
-- 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
N : Submodule R M
n : ℕ
h_1 : n ≥ 0
h : I • I ^ n • N = I ^ (1 + n) • N
h₁ : I • I ^ n • N = (HPow.hPow (β := ℕ) I 1 * I ^ n) • N
h₂ : I • I ^ n • N = HPow.hPow (β := ℕ) I 1 • I ^ n • N
h₃ h₄ : I • I ^ n • N = I • I ^ n • N
⊢ I • I ^ n • N = I ^ (n + 1) • N

Tactic:
rw [add_comm, pow_add, mul_smul, pow_one]

Premises used: pow_add, add_comm, pow_one, SemigroupAction.mul_smul
-- 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
h : F.Stable
obtain : ∀ (n₀ : ℕ) (hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)), ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀

Tactic:
obtain ⟨n₀, hn⟩ := 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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
h : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀

Tactic:
use 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
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ F.N (n₀ + 0) = HPow.hPow (β := ℕ) I 0 • F.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 : 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₀
h : n₀ + n ≥ n₀
⊢ F.N (n₀ + (n + 1)) = I ^ (n + 1) • F.N n₀

Tactic:
rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]

Premises used: add_assoc, pow_add, add_comm, pow_one, SemigroupAction.mul_smul
-- 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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
ih : F.N (n₀ + n) = I ^ n • F.N n₀
⊢ n₀ + n ≥ n₀

Tactic:
lia
-- 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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
k : ℕ
h : F.N (n₀ + 0) = HPow.hPow (β := ℕ) I 0 • F.N n₀
h₁ : ∀ (n : ℕ) (ih : F.N (n₀ + n) = I ^ n • F.N n₀), F.N (n₀ + (n + 1)) = I ^ (n + 1) • F.N n₀
⊢ F.N (n₀ + k) = I ^ k • 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

Premises used: add_assoc, pow_add, add_comm, pow_one, SemigroupAction.mul_smul
-- 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
h : F.Stable
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₀
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
obtain ⟨n₀, hn₀⟩ := h.exists_pow_smul_eq

Premises used: Ideal.Filtration.Stable.exists_pow_smul_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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
h₁ : ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
use 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ F.N (n₀ + (n - n₀)) = I ^ (n - n₀) • F.N n₀

Tactic:
hn₀ (n - n₀)

Premises used: HSub.hSub
-- 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
h₁ : n = n₀ + (n - n₀)
⊢ F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
convert! hn₀ (n - n₀)

Premises used: HSub.hSub
-- 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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
h₁ : n = n - n₀ + n₀
h₂ h₃ : n = n
⊢ n = n₀ + (n - n₀)

Tactic:
rw [add_comm, tsub_add_cancel_of_le hn]

Premises used: tsub_add_cancel_of_le, add_comm
-- 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.Stable ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
⟨Stable.exists_pow_smul_eq_of_ge, fun h => ⟨h.choose, fun n hn => ?_⟩⟩

Premises used: Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, Iff.intro, Exists.intro, Exists.choose
-- 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
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)
⊢ F.Stable ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
refine ⟨Stable.exists_pow_smul_eq_of_ge, fun h => ⟨h.choose, fun n 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
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₀)
⊢ n + 1 ≥ h.choose (p := fun (n₀ : ℕ) ↦ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀)

Tactic:
lia
-- 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
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₀))
rw₄ 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₀))
⊢ I • 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]

Premises used: Exists.choose_spec, smul_smul, tsub_add_eq_add_tsub, HAdd.hAdd, OfNat.ofNat, pow_succ'
-- 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
e : F.N 0 ≤ F'.N 0
obtain : ∀ (n₀ : ℕ) (hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)), ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
⊢ ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n

Tactic:
obtain ⟨n₀, hF⟩ := 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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
h : ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
⊢ ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n

Tactic:
use 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
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

Tactic:
(F.antitone ?_).trans e

Premises used: Ideal.Filtration.antitone, 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
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
h : 0 ≤ 0 + n₀
⊢ F.N (0 + n₀) ≤ F'.N 0

Tactic:
refine (F.antitone ?_).trans e

Premises used: Ideal.Filtration.antitone, 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
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ 0 ≤ 0 + 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
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)
h₁ : n + n₀ ≥ n₀
⊢ F.N (n + 1 + n₀) ≤ F'.N (n + 1)

Tactic:
rw [add_right_comm, ← hF]

Premises used: add_right_comm
-- 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
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
⊢ I • F.N (n + n₀) ≤ F'.N (n + 1)

Tactic:
(smul_mono_right _ hn).trans (F'.smul_le _)

Premises used: Ideal.Filtration.smul_le, Set.Mem, smul_mono_right, 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
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
⊢ I • F.N (n + n₀) ≤ F'.N (n + 1)

Tactic:
exact (smul_mono_right _ hn).trans (F'.smul_le _)

Premises used: Ideal.Filtration.smul_le, smul_mono_right, 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
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
⊢ n + 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
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
h₁ : ∀ (n : ℕ) (hn : F.N (n + n₀) ≤ F'.N n), F.N (n + 1 + n₀) ≤ F'.N (n + 1)
⊢ F.N (n + n₀) ≤ F'.N n

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

Premises used: add_right_comm, Ideal.Filtration.antitone, 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
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
⊢ ∃ (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)

Premises used: Ideal.Filtration.Stable.exists_forall_le, le_of_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 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
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
⊢ ∃ (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)

Premises used: Ideal.Filtration.Stable.exists_forall_le, le_of_eq, Eq.symm