awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
have 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
Tactic: specialize @h (f n) (N + a ^ n • ⊤) ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) = N
have 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
Tactic: refine le_antisymm (fun r ⟨h1, h2⟩ ↦ ?_) (le_inf (fun x ↦ N.smul_mem (a ^ n)) (by simp))
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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)
⊢ r ∈ N
have h2₁ : ∃ 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
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ r ∈ N
have 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
Tactic: obtain ⟨x, hx, -, ⟨y, -, rfl⟩, rfl⟩ := h2
Cleared hypotheses: r, h_1, h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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)
⊢ x + a ^ n • y ∈ N
have h₁ : (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)
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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)
⊢ x + a ^ n • y ∈ N
have h₁ : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
Tactic: rw [pow_add, mul_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
⊢ x + a ^ n • y ∈ N
have rwa : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ x + a ^ n • y ∈ N
have rwa₁ : a ^ n • 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]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ x + a ^ n • y ∈ N
have rwa₂ : a ^ n • x + a ^ n • 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]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ x + a ^ n • y ∈ N
have rwa₃ : a ^ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
have h₁ : f n = N ∨ HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
Tactic: rw [add_eq_sup, sup_eq_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
have refine : ∀ (h : f n = N), b ∈ N
Tactic: refine h.imp (fun h ↦ ?_) (fun h ↦ ⟨n, h⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
⊢ b ∈ N
have hn₁ : f n = f (n + 1)
Tactic: replace hn : f n = f (n + 1) := hn (n + 1) n.le_succ
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
⊢ b ∈ N
have rw : b ∈ f (n + 1)
Tactic: rw [← h, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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)
⊢ b ∈ f (n + 1)
have hab₁ : a • b ∈ f n
Tactic: rw [← h] at hab
Cleared hypotheses: hab, h_1, h, hn
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)))
have 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
Tactic: refine ⟨f.order - k, fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ order f - (↑k : ℤ) ≤ x
have 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 : ℤ))
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ x ∉ Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))
have rw : Ring.choose (x + (↑k : ℤ)) k • f.coeff (x + (↑k : ℤ)) = 0
Tactic: rw [Function.notMem_support, coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ x ∉ Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))
have rw₁ : HSMul.hSMul (β := V) (Ring.choose (x + (↑k : ℤ)) k) 0 = 0
Tactic: rw [Function.notMem_support, coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ x ∉ Function.support.{0, u_3} (M := V) fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))
have rw₂ : Eq.{u_3 + 1} (α := V) 0 0
Tactic: rw [Function.notMem_support, coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⸩
⊢ 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 : ℤ))) ⋯
have coeff : ∀ (x : ℤ),
  (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (f + g).coeff (n + (↑k : ℤ))) sorry).coeff x =
    (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))) sorry +
          ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • g.coeff (n + (↑k : ℤ))) sorry).coeff
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⸩
⊢ 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 : ℤ))) ⋯)
have coeff : ∀ (x : ℤ),
  (ofSuppBddBelow (fun (n : ℤ) ↦ Ring.choose (n + (↑k : ℤ)) k • (r • f).coeff (n + (↑k : ℤ))) sorry).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 : ℤ))) sorry)).coeff
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Eq.{u_2 + 1} (α := V⸨X⸩ →ₗ[R] V⸨X⸩) (hasseDeriv R 0) LinearMap.id
have 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)
Tactic: ext f n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 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⟦ℤ⟧)
have 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)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ
⊢ 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)
have 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
Tactic: dsimp only [hasseDeriv_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ
⊢ 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
have 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
Tactic: by_cases h : m = n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 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
have 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
Tactic: by_cases h : m = n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single n : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
    ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose n k • x) : V⟦ℤ⟧)
have rw : Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single (n - (↑k : ℤ) + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
  ((single (n - (↑k : ℤ) + (↑k : ℤ) - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) : V⟦ℤ⟧)
Tactic: rw [← Int.sub_add_cancel n k, hasseDeriv_single_add, Int.sub_add_cancel n k]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
rw :
  Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single (n - (↑k : ℤ) + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
    ((single (n - (↑k : ℤ) + (↑k : ℤ) - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) :
      V⟦ℤ⟧)
⊢ Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single n : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
    ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose n k • x) : V⟦ℤ⟧)
have rw₁ : Eq (α := V⸨X⸩) ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) : V⟦ℤ⟧)
  ((single (n - (↑k : ℤ) + (↑k : ℤ) - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) : V⟦ℤ⟧)
Tactic: rw [← Int.sub_add_cancel n k, hasseDeriv_single_add, Int.sub_add_cancel n k]