awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
⊢ ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N

Tactic:
rcases h with ⟨-, h⟩
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
specialize : f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) = N
specialize₁ :
  ∀ (h : f n = N ∨ N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ = N),
    b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N

Tactic:
specialize @h (f n) (N + a ^ n • ⊤) ?_
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ N ≤ N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
refine :
  ∀ r ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤),
    ∀ (h1 : r ∈ (↑(f n) : Set M)) (h2 : r ∈ (↑(N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) : Set M)), r ∈ N
⊢ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) = N

Tactic:
refine le_antisymm (fun r ⟨h1, h2⟩ ↦ ?_) (le_inf (fun x ↦ N.smul_mem (a ^ n)) (by simp))

Premises used: le_inf, le_antisymm
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
r : M
h_1 : r ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤)
h1 : r ∈ (↑(f n) : Set M)
h2 : r ∈ (↑(N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) : Set M)
⊢ ∃ y ∈ N, ∃ (z : M), (∃ (b : M), Membership.mem (γ := Submodule R M) ⊤ b ∧ a ^ n • b = z) ∧ y + z = r

Tactic:
simp only [add_eq_sup, SetLike.mem_coe, mem_sup, mem_smul_pointwise_iff_exists] at h2

Premises used: Submodule.mem_smul_pointwise_iff_exists, SetLike.mem_coe, Submodule.mem_sup, Submodule.add_eq_sup
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
r : M
h_1 : r ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤)
h1 : r ∈ (↑(f n) : Set M)
h2 : ∃ y ∈ N, ∃ (z : M), (∃ (b : M), Membership.mem (γ := Submodule R M) ⊤ b ∧ a ^ n • b = z) ∧ y + z = r
obtain :
  ∀ (x : M) (hx : x ∈ N) (y : M),
    x + a ^ n • y ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) →
      ∀ (h1 : x + a ^ n • y ∈ (↑(f n) : Set M)), x + a ^ n • y ∈ N
⊢ r ∈ N

Tactic:
obtain ⟨x, hx, -, ⟨y, -, rfl⟩, rfl⟩ := h2

Premises used: rfl
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
h_1 : x + a ^ n • y ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤)
h1 : x + a ^ n • y ∈ (↑(f n) : Set M)
⊢ (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N)

Tactic:
have h : (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N) := congr_arg (y ∈ ·) (hn (n + n) le_add_self)
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h_1 : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
h_2 : x + a ^ n • y ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤)
h1 : x + a ^ n • y ∈ (↑(f n) : Set M)
h : (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N)
⊢ (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)

Tactic:
rw [pow_add, mul_smul] at h

Premises used: pow_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h_1 : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
h_2 : x + a ^ n • y ∈ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤)
h1 : x + a ^ n • y ∈ (↑(f n) : Set M)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
rwa : a ^ n • y ∈ N
rwa₁ : a ^ n • a ^ n • y ∈ N
rwa₂ : a ^ n • x + a ^ n • a ^ n • y ∈ N
rwa₃ rwa₄ rwa₅ rwa₆ : a ^ n • (x + a ^ n • y) ∈ N
⊢ x + a ^ n • y ∈ N

Tactic:
rwa [N.add_mem_iff_right hx, h, ← N.add_mem_iff_right (N.smul_mem (a ^ n) hx), ← smul_add]

Premises used: HPow.hPow, Submodule.add_mem_iff_right, smul_add, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : f n = N ∨ N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ = N
⊢ f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N

Tactic:
rw [add_eq_sup, sup_eq_left] at h

Premises used: sup_eq_left, Submodule.add_eq_sup
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N

Tactic:
h.imp (fun h ↦ ?_) (fun h ↦ ⟨n, h⟩)

Premises used: Exists.intro, Or.imp
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
refine : ∀ (h : f n = N), b ∈ N
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N

Tactic:
refine h.imp (fun h ↦ ?_) (fun h ↦ ⟨n, h⟩)

Premises used: Or.imp
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
        (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
⊢ f n = f (n + 1)

Tactic:
replace hn : f n = f (n + 1) := hn (n + 1) n.le_succ
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
rw : b ∈ f (n + 1)
⊢ b ∈ N

Tactic:
rw [← h, hn]
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
⊢ a • b ∈ f n

Tactic:
rw [← h] at hab
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
hab₁ : a • b ∈ f n
⊢ f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N

Tactic:
rw [← h] at hab
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
hab₁ : a • b ∈ f n
h₁ : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
⊢ f n = N

Tactic:
rw [← h] at hab
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
hab₁ : a • b ∈ f n
h₁ : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h₂ : f n = N
⊢ f n = f (n + 1)

Tactic:
rw [← h] at hab
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
a : R
b : M
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hab : a • b ∈ f n
h_1 : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
⊢ b ∈ f (n + 1)

Tactic:
simpa [f, pow_succ, mul_smul] using hab

Premises used: pow_succ, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
⊢ IsLasker R M

Tactic:
fun I ↦
  (exists_infIrred_decomposition I).imp fun _ h ↦ h.imp_right fun h' _ ht ↦ (h' ht).isPrimary

Premises used: Exists.imp, exists_infIrred_decomposition, IsLasker
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
f : V⸨X⸩
⊢ BddBelow (α := ℤ)
    (Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)))

Tactic:
⟨f.order - k, fun x h ↦ ?_⟩

Premises used: HahnSeries.order, HSub.hSub, Nat.cast, Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
f : V⸨X⸩
refine :
  ∀ (x : ℤ)
    (h :
      Membership.mem (γ := Set ℤ)
        (Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) x),
    order f - (↑k : ℤ) ≤ x
⊢ BddBelow (α := ℤ)
    (Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)))

Tactic:
refine ⟨f.order - k, fun x h ↦ ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h :
  Membership.mem (γ := Set ℤ)
    (Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) x
contrapose! :
  ∀ (h : x < order f - (↑k : ℤ)),
    x ∉ Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))
⊢ order f - (↑k : ℤ) ≤ x

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h : x < order f - (↑k : ℤ)
rw : Ring.choose (x + (↑k : ℤ)) k • f.coeff (x + (↑k : ℤ)) = 0
rw₁ : HSMul.hSMul (β := V) (Ring.choose (x + (↑k : ℤ)) k) 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := V) 0 0
⊢ x ∉ Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))

Tactic:
rw [Function.notMem_support, coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h, smul_zero]

Premises used: smul_zero, Function.notMem_support, Iff.mp, lt_sub_iff_add_lt, HahnSeries.coeff_eq_zero_of_lt_order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
f g : V⸨X⸩
coeff :
  ∀ (x : ℤ),
    (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (f + g).coeff (n + (↑k : ℤ))) ⋯).coeff x =
      (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) ⋯ +
            ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • g.coeff (n + (↑k : ℤ))) ⋯).coeff
        x
⊢ ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (f + g).coeff (n + (↑k : ℤ))) ⋯ =
    ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) ⋯ +
      ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • g.coeff (n + (↑k : ℤ))) ⋯

Tactic:
ext
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
f g : V⸨X⸩
x : ℤ
⊢ (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (f + g).coeff (n + (↑k : ℤ))) ⋯).coeff x =
    (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) ⋯ +
          ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • g.coeff (n + (↑k : ℤ))) ⋯).coeff
      x

Tactic:
simp only [ofSuppBddBelow, coeff_add', Pi.add_apply, smul_add]

Premises used: Pi.add_apply, HahnSeries.ofSuppBddBelow, HahnSeries.coeff_add', smul_add
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
r : R
f : V⸨X⸩
coeff :
  ∀ (x : ℤ),
    (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (r • f).coeff (n + (↑k : ℤ))) ⋯).coeff x =
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
            (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) ⋯)).coeff
        x
⊢ ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (r • f).coeff (n + (↑k : ℤ))) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R_1 : Type u_1
R : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : Semiring R
inst_2 : Module R V
k : ℕ
r : R
f : V⸨X⸩
x : ℤ
⊢ (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (r • f).coeff (n + (↑k : ℤ))) ⋯).coeff x =
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
          (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) ⋯)).coeff
      x

Tactic:
simp only [ofSuppBddBelow, HahnSeries.coeff_smul, RingHom.id_apply, smul_comm r]

Premises used: RingHom.id_apply, HahnSeries.coeff_smul, HahnSeries.ofSuppBddBelow, SMulCommClass.smul_comm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f) n = Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
h :
  ∀ (f : V⸨X⸩) (n : ℤ),
    Eq.{u_2 + 1} (α := V) (HahnSeries.coeff ((hasseDeriv R 0 : (a : V⸨X⸩) → V⸨X⸩) f) n)
      (HahnSeries.coeff ((LinearMap.id : (a : V⸨X⸩) → V⸨X⸩) f) n)
⊢ Eq.{u_2 + 1} (α := V⸨X⸩ →ₗ[R] V⸨X⸩) (hasseDeriv R 0) LinearMap.id

Tactic:
ext f n
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
f : V⸨X⸩
n : ℤ
⊢ Eq.{u_2 + 1} (α := V) (HahnSeries.coeff ((hasseDeriv R 0 : (a : V⸨X⸩) → V⸨X⸩) f) n)
    (HahnSeries.coeff ((LinearMap.id : (a : V⸨X⸩) → V⸨X⸩) f) n)

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k : ℕ
n : ℤ
x : V
coeff :
  ∀ (m : ℤ),
    Eq.{u_2 + 1} (α := V)
      (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x)) m)
      (HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m)
⊢ Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
    ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x) : V⟦ℤ⟧)

Tactic:
ext m
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
coeff :
  HSMul.hSMul (β := V) (Ring.choose (m + (↑k : ℤ)) k)
      (HahnSeries.coeff ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) (m + (↑k : ℤ))) =
    HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m
⊢ Eq.{u_2 + 1} (α := V)
    (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x)) m)
    (HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m)

Tactic:
dsimp only [hasseDeriv_coeff]

Premises used: LaurentSeries.hasseDeriv_coeff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
pos :
  ∀ (h : m = n),
    HSMul.hSMul (β := V) (Ring.choose (m + (↑k : ℤ)) k)
        (HahnSeries.coeff ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) (m + (↑k : ℤ))) =
      HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m
neg :
  ∀ (h : ¬m = n),
    HSMul.hSMul (β := V) (Ring.choose (m + (↑k : ℤ)) k)
        (HahnSeries.coeff ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) (m + (↑k : ℤ))) =
      HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m
⊢ HSMul.hSMul (β := V) (Ring.choose (m + (↑k : ℤ)) k)
      (HahnSeries.coeff ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) (m + (↑k : ℤ))) =
    HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m

Tactic:
by_cases h : m = n