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
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
mpr :
  (∃ (r : ↥I), (↑r : R) • x = x) →
    Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x

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
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
obtain :
  ∀ (k : ℕ)
    (hk :
      ∀ n ≥ k,
        I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n =
          (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)),
    N ≤ I • N
⊢ N ≤ I • N

Tactic:
obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)

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

Tactic:
have := hk k (le_refl _)
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (k + 1)
⊢ I • N = N

Tactic:
rw [hN, hN] at this
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • N = N
⊢ N ≤ I • N

Tactic:
le_of_eq this.symm

Premises used: le_of_eq, Eq.symm
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • N = N
⊢ N ≤ I • N

Tactic:
exact le_of_eq this.symm

Premises used: le_of_eq, Eq.symm
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
mp :
  ∀ (r : R) (hr₁ : r ∈ I) (hr₂ : ∀ n ∈ N, r • n = n),
    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

Tactic:
obtain ⟨r, hr₁, hr₂⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
        obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
        have := hk k (le_refl _)
        rw [hN, hN] at this
        exact le_of_eq this.symm)

Premises used: IsNoetherian.noetherian, Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_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
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
r : R
hr₁ : r ∈ I
hr₂ : ∀ n ∈ N, r • n = n
H : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
⊢ ∃ (r : ↥I), (↑r : R) • x = x

Tactic:
⟨⟨r, hr₁⟩, hr₂ _ H⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : R
hr₁ : r ∈ I
hr₂ : ∀ n ∈ N, r • n = n
H : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
⊢ ∃ (r : ↥I), (↑r : R) • x = x

Tactic:
exact ⟨⟨r, hr₁⟩, hr₂ _ 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
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
r : ↥I
eq : (↑r : R) • x = x
mpr : ∀ (i : ℕ), x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x

Tactic:
rw [Submodule.mem_iInf]

Premises used: Submodule.mem_iInf
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : (↑r : R) • x = x
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (HPow.hPow (β := ℕ) I 0) ⊤

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

Tactic:
rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]

Premises used: pow_add, smul_smul, add_comm, pow_one
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : (↑r : R) • x = x
i : ℕ
hi : x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
⊢ (↑r : R) • x ∈ I • HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤

Tactic:
Submodule.smul_mem_smul r.prop hi

Premises used: Set.Mem, Subtype.prop, Submodule.smul_mem_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
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
r : ↥I
eq : (↑r : R) • x = x
i : ℕ
hi : x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
⊢ (↑r : R) • x ∈ I • HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤

Tactic:
exact Submodule.smul_mem_smul r.prop hi

Premises used: Subtype.prop, Submodule.smul_mem_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
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
r : ↥I
eq : (↑r : R) • x = x
i : ℕ
mpr : x ∈ HSMul.hSMul (β := Submodule R M) (HPow.hPow (β := ℕ) I 0) ⊤
mpr₁ :
  ∀ (i : ℕ) (hi : x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤), x ∈ HSMul.hSMul (β := Submodule R M) (I ^ (i + 1)) ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤

Tactic:
induction i with
    | zero => simp
    | succ i hi =>
      rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
      exact Submodule.smul_mem_smul r.prop hi

Premises used: pow_add, smul_smul, add_comm, pow_one
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
rw : LE.le.{u_2} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
obtain : ∀ (r : ↥I) (hr : (↑r : R) • x = x), Membership.mem (γ := Submodule R M) ⊥ x
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
obtain ⟨r, hr⟩ := (I.mem_iInf_smul_pow_eq_bot_iff x).mp hx

Premises used: Ideal.mem_iInf_smul_pow_eq_bot_iff, Iff.mp
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
r : ↥I
hr : (↑r : R) • x = x
⊢ Membership.mem (γ := Ideal R) (jacobson ⊥) (1 - (↑r : R) - 1)

Tactic:
simpa using h r.2

Premises used: 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
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
r : ↥I
hr : (↑r : R) • x = x
⊢ IsUnit (1 - (↑r : R))

Tactic:
have := isUnit_of_sub_one_mem_jacobson_bot (1 - r.1) (by simpa using h r.2)
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
r : ↥I
hr : (↑r : R) • x = x
this : IsUnit (1 - (↑r : R))
apply : (1 - (↑r : R)) • x = HSMul.hSMul (β := M) (1 - (↑r : R)) 0
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
apply this.smul_left_cancel.mp

Premises used: IsUnit.smul_left_cancel, Iff.mp
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
r : ↥I
hr : (↑r : R) • x = x
this : IsUnit (1 - (↑r : R))
⊢ (1 - (↑r : R)) • x = HSMul.hSMul (β := M) (1 - (↑r : R)) 0

Tactic:
simp [sub_smul, hr]

Premises used: sub_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
inst_3 : IsNoetherianRing R
inst_4 : IsLocalRing R
inst_5 : Module.Finite R M
h : I ≠ ⊤
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥

Tactic:
Ideal.iInf_pow_smul_eq_bot_of_le_jacobson _
    ((le_maximalIdeal h).trans (maximalIdeal_le_jacobson _))

Premises used: Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, IsLocalRing.maximalIdeal_le_jacobson, IsLocalRing.le_maximalIdeal, LE.le.trans
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
⊢ Eq.{u_1 + 1} (α := Submodule R R) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R R) (I ^ i) ⊤) ⊥

Tactic:
I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h

Premises used: Ideal.iInf_pow_smul_eq_bot_of_isLocalRing
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
h₁ : ∀ (x : ℕ), I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : ℕ), I ^ i) ⊥

Tactic:
convert! I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h

Premises used: Ideal.iInf_pow_smul_eq_bot_of_isLocalRing
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
x : ℕ
h₁ : ∀ (i : R), i ∈ I ^ x ↔ i ∈ HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
⊢ I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤

Tactic:
ext i
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
x : ℕ
i : R
h₁ : i ∈ I ^ x ↔ i ∈ I ^ x * ⊤
h₂ : i ∈ I ^ x ↔ i ∈ I ^ x * 1
h₃ h₄ : i ∈ I ^ x ↔ i ∈ I ^ x
⊢ i ∈ I ^ x ↔ i ∈ HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤

Tactic:
rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]

Premises used: Ideal.one_eq_top, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
mp : IsIdempotentElem I → I = ⊥ ∨ I = ⊤
mpr : I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
pos : I = ⊤ → I = ⊥ ∨ I = ⊤
neg : ¬I = ⊤ → I = ⊥ ∨ I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
by_cases I = ⊤
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
Or.inr ‹_›

Premises used: Or.inr
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
exact Or.inr ‹_›

Premises used: Or.inr
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
Or.inl (eq_bot_iff.mpr ?_)

Premises used: Iff.mpr, Or.inl, eq_bot_iff
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
neg : I ≤ ⊥
⊢ I = ⊥ ∨ I = ⊤

Tactic:
refine Or.inl (eq_bot_iff.mpr ?_)

Premises used: Iff.mpr, Or.inl, eq_bot_iff
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
neg : I ≤ ⨅ (i : ℕ), I ^ i
⊢ I ≤ ⊥

Tactic:
rw [← Ideal.iInf_pow_eq_bot_of_isLocalRing I ‹_›]

Premises used: Ideal.iInf_pow_eq_bot_of_isLocalRing
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
neg : ∀ (i : ℕ), I ≤ I ^ i
⊢ I ≤ ⨅ (i : ℕ), I ^ i

Tactic:
apply le_iInf

Premises used: le_iInf
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
⊢ I ≤ HPow.hPow (β := ℕ) I 0

Tactic:
simp [H.pow_succ_eq]

Premises used: IsIdempotentElem.pow_succ_eq
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
n : ℕ
⊢ I ≤ I ^ (n + 1)

Tactic:
simp [H.pow_succ_eq]

Premises used: IsIdempotentElem.pow_succ_eq
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ IsIdempotentElem.{u_3} (M := Ideal R) ⊥

Tactic:
simp [IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ IsIdempotentElem.{u_3} (M := Ideal R) ⊤

Tactic:
simp [IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
rw : LE.le.{u_2} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
by_contra : ∀ (hx' : x ∉ ⊥), False
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
by_contra hx'
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x

Tactic:
have := Ideal.mem_iInf_smul_pow_eq_bot_iff I x
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
this :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
obtain : ∀ (r : ↥I) (hr : (↑r : R) • x = x), False
⊢ False

Tactic:
obtain ⟨r, hr⟩ := this.mp hx

Premises used: Iff.mp
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
this :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
r : ↥I
hr : (↑r : R) • x = x
⊢ (↑r : R) = 1

Tactic:
have := smul_left_injective _ hx' (hr.trans (one_smul _ x).symm)
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
this_1 :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
r : ↥I
hr : (↑r : R) • x = x
this : (↑r : R) = 1
⊢ False

Tactic:
I.eq_top_iff_one.not.mp h (this ▸ r.prop)

Premises used: Eq.rec, Iff.not, Ideal.eq_top_iff_one, Subtype.prop, Iff.mp
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
this_1 :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
r : ↥I
hr : (↑r : R) • x = x
this : (↑r : R) = 1
⊢ False

Tactic:
exact I.eq_top_iff_one.not.mp h (this ▸ r.prop)

Premises used: Eq.rec, Iff.not, Ideal.eq_top_iff_one, Subtype.prop, Iff.mp
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsDomain R
h : I ≠ ⊤
⊢ Eq.{u_1 + 1} (α := Submodule R R) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R R) (I ^ i) ⊤) ⊥

Tactic:
I.iInf_pow_smul_eq_bot_of_isTorsionFree (M := R) h

Premises used: Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsDomain R
h : I ≠ ⊤
h₁ : ∀ (x : ℕ), I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : ℕ), I ^ i) ⊥

Tactic:
convert! I.iInf_pow_smul_eq_bot_of_isTorsionFree (M := R) h

Premises used: Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsDomain R
h : I ≠ ⊤
x : ℕ
⊢ I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M_1 : Type u_2
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
inst_5 : Subsingleton M_1
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M_1 ≃ₗ[R] N
⊢ Subsingleton N

Tactic:
have := e.symm.toEquiv.subsingleton
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M_1 : Type u_2
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
inst_5 : Subsingleton M_1
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M_1 ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N

Tactic:
.of_subsingleton

Premises used: IsFiniteLength.of_subsingleton