awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
hx : x ∈ r • P
smul₀ : ∀ (p : M) (hp : p ∈ P), r • p ∈ N
⊢ x ∈ N
have smul₁ : ∀ (r_1 : R), ∀ m ∈ r • P, ∀ (h : m ∈ N), r_1 • m ∈ N
Tactic: induction hx using Submodule.smul_inductionOn_pointwise with
  | smul₀ p hp =>
    rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
    exact hr _ ⟨p, hp, rfl⟩
  | smul₁ _ _ _ h => exact N.smul_mem _ h
  | add _ _ _ _ hx hy => exact N.add_mem hx hy
  | zero => exact N.zero_mem
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
hx : x ∈ r • P
smul₀ : ∀ (p : M) (hp : p ∈ P), r • p ∈ N
smul₁ : ∀ (r_1 : R), ∀ m ∈ r • P, ∀ (h : m ∈ N), r_1 • m ∈ N
⊢ x ∈ N
have add : ∀ (x y : M), x ∈ r • P → y ∈ r • P → ∀ (hx : x ∈ N) (hy : y ∈ N), x + y ∈ N
Tactic: induction hx using Submodule.smul_inductionOn_pointwise with
  | smul₀ p hp =>
    rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
    exact hr _ ⟨p, hp, rfl⟩
  | smul₁ _ _ _ h => exact N.smul_mem _ h
  | add _ _ _ _ hx hy => exact N.add_mem hx hy
  | zero => exact N.zero_mem
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
hx : x ∈ r • P
smul₀ : ∀ (p : M) (hp : p ∈ P), r • p ∈ N
smul₁ : ∀ (r_1 : R), ∀ m ∈ r • P, ∀ (h : m ∈ N), r_1 • m ∈ N
add : ∀ (x y : M), x ∈ r • P → y ∈ r • P → ∀ (hx : x ∈ N) (hy : y ∈ N), x + y ∈ N
⊢ x ∈ N
have zero : 0 ∈ N
Tactic: induction hx using Submodule.smul_inductionOn_pointwise with
  | smul₀ p hp =>
    rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
    exact hr _ ⟨p, hp, rfl⟩
  | smul₁ _ _ _ h => exact N.smul_mem _ h
  | add _ _ _ _ hx hy => exact N.add_mem hx hy
  | zero => exact N.zero_mem
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ N ≤ N'
have apply : N ≤ N' ⊔ I • N
Tactic: apply le_of_le_smul_of_le_jacobson_bot hN hIjac
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ N ≤ N' ⊔ I • N
have apply_fun : ∀ (hmaple : comap (I • N).mkQ (map (I • N).mkQ N) ≤ comap (I • N).mkQ (map (I • N).mkQ N')), N ≤ N' ⊔ I • N
Tactic: apply_fun comap (I • N).mkQ at hmaple
Cleared hypotheses: hmaple
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
apply_fun : ∀ (hmaple : comap (I • N).mkQ (map (I • N).mkQ N) ≤ comap (I • N).mkQ (map (I • N).mkQ N')), N ≤ N' ⊔ I • N
⊢ N ≤ N' ⊔ I • N
have apply_fun₁ : Monotone (comap (I • N).mkQ)
Tactic: apply_fun comap (I • N).mkQ at hmaple
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : comap (I • N).mkQ (map (I • N).mkQ N) ≤ comap (I • N).mkQ (map (I • N).mkQ N')
⊢ N ≤ N' ⊔ I • N
have hmaple₁ : N ≤ I • N ⊔ N'
Tactic: simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at hmaple
Cleared hypotheses: hmaple
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : N ≤ I • N ⊔ N'
grw : N ≤ I • N ⊔ N'
⊢ N ≤ N' ⊔ I • N
have grw₁ : N ≤ N
Tactic: grw [sup_comm, ← hmaple]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N = N'
have a : N ≤ N'
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
a : N ≤ N'
⊢ N = N'
have a₁ : N' ≤ N
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N' ≤ N
have hmaple₁ : comap (I • N).mkQ (map (I • N).mkQ N) = comap (I • N).mkQ (map (I • N).mkQ N')
Tactic: apply_fun comap (I • N).mkQ at hmaple
Cleared hypotheses: hmaple
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : comap (I • N).mkQ (map (I • N).mkQ N) = comap (I • N).mkQ (map (I • N).mkQ N')
⊢ N' ≤ N
have hmaple₁ : N = I • N ⊔ N'
Tactic: simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at hmaple
Cleared hypotheses: hmaple
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ jacobson ⊥
hmaple : N = I • N ⊔ N'
⊢ N' ≤ N
have a : N' ≤ I • N ⊔ N'
Tactic: rw [hmaple]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ ∃ (t : Set M),
    Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) t ∧
      (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' t = s ∧ span R t = N
have h : Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s) ∧
  (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N
Tactic: use Quotient.out '' s
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s) ∧
    (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N
have h : Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s)
Tactic: split_ands
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
h : Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s)
⊢ Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s) ∧
    (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N
have h₁ : (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s
Tactic: split_ands
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
h : Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s)
h₁ : (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s
⊢ Set.InjOn (β := M ⧸ I • N) (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) (Quotient.out '' s) ∧
    (⇑(I • N).mkQ : (a : M) → M ⧸ I • N) '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N
have h₂ : span R (Quotient.out '' s) = N
Tactic: split_ands
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ span R (Quotient.out '' s) = N
have h : N = span R (Quotient.out '' s)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ jacobson ⊥
hsspan : span R s = map (I • N).mkQ N
⊢ N = span R (Quotient.out '' s)
have h : map (I • N).mkQ N = map (I • N).mkQ (span R (Quotient.out '' s))
Tactic: apply eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot hN hIjac
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x : R
inst : Ring R
h : IsNilpotent x
⊢ IsNilpotent (-x)
have obtain : ∀ (n : ℕ) (hn : x ^ n = 0), IsNilpotent (-x)
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x : R
inst : Ring R
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (-x)
have h : (-x) ^ n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x : R
inst : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-x) ^ n = 0
have h : HPow.hPow (α := R) (-1) n * x ^ n = 0
Tactic: rw [neg_pow, hn, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x : R
inst : Ring R
n : ℕ
hn : x ^ n = 0
h : HPow.hPow (α := R) (-1) n * x ^ n = 0
⊢ (-x) ^ n = 0
have h₁ : HPow.hPow (α := R) (-1) n * 0 = 0
Tactic: rw [neg_pow, hn, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x : R
inst : Ring R
n : ℕ
hn : x ^ n = 0
h : HPow.hPow (α := R) (-1) n * x ^ n = 0
h₁ : HPow.hPow (α := R) (-1) n * 0 = 0
⊢ (-x) ^ n = 0
have h₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [neg_pow, hn, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
ha : IsNilpotent a
t : R
⊢ IsNilpotent (t • a)
have obtain : ∀ (k : ℕ) (ha : a ^ k = 0), IsNilpotent (t • a)
Tactic: obtain ⟨k, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ IsNilpotent (t • a)
have h : (t • a) ^ k = 0
Tactic: use k
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ (t • a) ^ k = 0
have h : t ^ k • a ^ k = 0
Tactic: rw [smul_pow, ha, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
h : t ^ k • a ^ k = 0
⊢ (t • a) ^ k = 0
have h₁ : HSMul.hSMul (β := S) (t ^ k) 0 = 0
Tactic: rw [smul_pow, ha, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
inst_2 : MulActionWithZero R S
inst_3 : SMulCommClass R S S
inst_4 : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
h : t ^ k • a ^ k = 0
h₁ : HSMul.hSMul (β := S) (t ^ k) 0 = 0
⊢ (t • a) ^ k = 0
have h₂ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [smul_pow, ha, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)
have obtain : ∀ (n : ℕ) (hn : r ^ n = 0), IsUnit (r - 1)
Tactic: obtain ⟨n, hn⟩ := hnil
Cleared hypotheses: hnil
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (r - 1)
have refine_1 : (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1
Tactic: refine ⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
n : ℕ
hn : r ^ n = 0
refine_1 : (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1
⊢ IsUnit (r - 1)
have refine_2 : (-∑ i ∈ Finset.range n, r ^ i) * (r - 1) = 1
Tactic: refine ⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (1 - r)
have rw : IsUnit (r - 1)
Tactic: rw [← IsUnit.neg_iff, neg_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r + 1)
have rw : IsUnit (-r - 1)
Tactic: rw [← IsUnit.neg_iff, neg_add']
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (u + r)
have rw : IsUnit (1 + r * (↑hu.unit⁻¹ : R))
Tactic: rw [← Units.isUnit_mul_units _ hu.unit⁻¹, add_mul, IsUnit.mul_val_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (1 + r * (↑hu.unit⁻¹ : R))
have h_comm₁ : Commute r (↑hu.unit⁻¹ : R)
Tactic: replace h_comm : Commute r (↑hu.unit⁻¹) := Commute.units_inv_right h_comm
Cleared hypotheses: h_comm
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r (↑hu.unit⁻¹ : R)
⊢ IsUnit (1 + r * (↑hu.unit⁻¹ : R))
have refine : IsNilpotent (r * (↑hu.unit⁻¹ : R))
Tactic: refine IsNilpotent.isUnit_one_add ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
⊢ e = 0
have zero : ∀ (hn : HPow.hPow (β := ℕ) e 0 = 0), e = 0
Tactic: obtain ⟨rfl | n, hn⟩ := nilp
Cleared hypotheses: nilp
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
zero : ∀ (hn : HPow.hPow (β := ℕ) e 0 = 0), e = 0
⊢ e = 0
have succ : ∀ (n : ℕ) (hn : e ^ (n + 1) = 0), e = 0
Tactic: obtain ⟨rfl | n, hn⟩ := nilp
Cleared hypotheses: nilp
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (hypothesis)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : HPow.hPow (β := ℕ) e 0 = 0
⊢ e = 0
have hn₁ : Eq.{u_1 + 1} (α := R) 1 0
Tactic: rw [pow_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : Eq.{u_1 + 1} (α := R) 1 0
⊢ e = 0
have zero : 1 * e = 0
Tactic: rw [← one_mul e, hn, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : Eq.{u_1 + 1} (α := R) 1 0
zero : 1 * e = 0
⊢ e = 0
have zero₁ : 0 * e = 0
Tactic: rw [← one_mul e, hn, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : Eq.{u_1 + 1} (α := R) 1 0
zero : 1 * e = 0
zero₁ : 0 * e = 0
⊢ e = 0
have zero₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← one_mul e, hn, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
⊢ e = 0
have succ : e = e ^ (n + 1)
Tactic: rw [← hn, idem.pow_succ_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
succ : e = e ^ (n + 1)
⊢ e = 0
have succ₁ : e = e
Tactic: rw [← hn, idem.pow_succ_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
⊢ IsRadical.{u_1} (R := R) 0 ↔ IsReduced R
have simp_rw : IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x
Tactic: simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
have simp_rw : IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R), x ^ k = 0 → x = 0
Tactic: simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
k : ℕ
hk : 1 < k
simp_rw : IsRadical.{u_1} (R := R) 0 ↔ ∀ (x : R), x ^ k = 0 → x = 0
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
have simp_rw₁ : (∀ (x : R), 0 ∣ x ^ k → 0 ∣ x) ↔ ∀ (x : R), x ^ k = 0 → x = 0
Tactic: simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y : R
hy : IsRadical y
h0 : y ≠ 0
hxy : x ∣ y
⊢ ∀ (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1
have obtain : ∀ (z : R) (hy : IsRadical (x * z)) (h0 : x * z ≠ 0) (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1
Tactic: obtain ⟨z, rfl⟩ := hxy
Cleared hypotheses: y, hy, h0, hxy
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
⊢ ∀ (x_1 : R), x ∣ HPow.hPow (β := ℕ) x_1 2 → x ∣ x_1
have refine : ∀ (w : R) (dvd : x ∣ HPow.hPow (β := ℕ) w 2), x * z ∣ HPow.hPow (β := ℕ) (w * z) 2
Tactic: refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ HPow.hPow (β := ℕ) w 2
⊢ x * z ∣ HPow.hPow (β := ℕ) (w * z) 2
have rw : x * z ∣ HPow.hPow (β := ℕ) w 2 * HPow.hPow (β := ℕ) z 2
Tactic: rw [mul_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ HPow.hPow (β := ℕ) w 2
⊢ x * z ∣ HPow.hPow (β := ℕ) w 2 * HPow.hPow (β := ℕ) z 2
have a : z ∣ HPow.hPow (β := ℕ) z 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ (x + y) ^ k = 0
have rw : Eq.{u_1 + 1} (α := R) (∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, k.choose m.1 • (x ^ m.1 * y ^ m.2)) 0
Tactic: rw [h_comm.add_pow']
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ Eq.{u_1 + 1} (α := R) (∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, k.choose m.1 • (x ^ m.1 * y ^ m.2)) 0
have h₁ : ∀ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, k.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) = 0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0
have h₁ : x ^ i * y ^ j = 0
Tactic: suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
⊢ x ^ i * y ^ j = 0
have pos : ∀ (hi : m ≤ i), x ^ i * y ^ j = 0
Tactic: by_cases hi : m ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
pos : ∀ (hi : m ≤ i), x ^ i * y ^ j = 0
⊢ x ^ i * y ^ j = 0
have neg : ∀ (hi : ¬m ≤ i), x ^ i * y ^ j = 0
Tactic: by_cases hi : m ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
hi : m ≤ i
⊢ x ^ i * y ^ j = 0
have pos : 0 * y ^ j = 0
Tactic: rw [pow_eq_zero_of_le hi hx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
hi : m ≤ i
pos : 0 * y ^ j = 0
⊢ x ^ i * y ^ j = 0
have pos₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [pow_eq_zero_of_le hi hx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
hi : ¬m ≤ i
⊢ x ^ i * y ^ j = 0
have rw : n ≤ j
Tactic: rw [pow_eq_zero_of_le ?_ hy, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k
hi : ¬m ≤ i
⊢ n ≤ j
have linarith : j < n →
  -1 + (HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) +
          (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 - (↑m : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑j : ℤ) 1 - (↑n : ℤ)) +
      -(HAdd.hAdd (α := ℤ) (↑i : ℤ) (↑j : ℤ) - (↑k : ℤ)) =
    0
Tactic: linarith [Finset.mem_antidiagonal.mp hij]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Basic (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
m n : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
⊢ m + n ≤ m + n - 1 + 1
have rw : m + n - 1 ≤ m + n - 1
Tactic: rw [← Nat.sub_le_iff_le_add]