awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
⊢ z ∣ HPow.hPow (β := ℕ) z 2

Tactic:
dvd_pow_self _ two_ne_zero

Premises used: dvd_pow_self, two_ne_zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
⊢ z ∣ HPow.hPow (β := ℕ) z 2

Tactic:
exact dvd_pow_self _ two_ne_zero

Premises used: dvd_pow_self, two_ne_zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
rw : Eq.{u_1 + 1} (α := R) (∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, k.choose m.1 • (x ^ m.1 * y ^ m.2)) 0
⊢ (x + y) ^ k = 0

Tactic:
rw [h_comm.add_pow']

Premises used: Commute.add_pow'
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
h₁ : ∀ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, k.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, k.choose m.1 • (x ^ m.1 * y ^ m.2)) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
this : x ^ i * y ^ j = 0
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0

Tactic:
simp only [this, nsmul_eq_mul, mul_zero]

Premises used: MulZeroClass.mul_zero, nsmul_eq_mul
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
h₁ : x ^ i * y ^ j = 0
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0

Tactic:
suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero]
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
neg : ∀ (hi : ¬m ≤ i), x ^ i * y ^ j = 0
⊢ x ^ i * y ^ j = 0

Tactic:
by_cases hi : m ≤ i
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x ^ i * y ^ j = 0

Tactic:
rw [pow_eq_zero_of_le hi hx, zero_mul]

Premises used: pow_eq_zero_of_le, MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
rw : n ≤ j
⊢ x ^ i * y ^ j = 0

Tactic:
rw [pow_eq_zero_of_le ?_ hy, mul_zero]

Premises used: pow_eq_zero_of_le, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
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
⊢ n ≤ j

Tactic:
linarith [Finset.mem_antidiagonal.mp hij]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.RingTheory.Nilpotent.Basic
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
rw rw₁ : m + n - 1 ≤ m + n - 1
⊢ m + n ≤ m + n - 1 + 1

Tactic:
rw [← Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
obtain : ∀ (n : ℕ) (hn : x ^ n = 0), IsNilpotent (x + y)
⊢ IsNilpotent (x + y)

Tactic:
obtain ⟨n, hn⟩ := hx
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
obtain : ∀ (m : ℕ) (hm : y ^ m = 0), IsNilpotent (x + y)
⊢ IsNilpotent (x + y)

Tactic:
obtain ⟨m, hm⟩ := hy
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)

Tactic:
⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩

Premises used: Commute.add_pow_add_eq_zero_of_pow_eq_zero, Exists.intro, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)

Tactic:
exact ⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hnp : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsNilpotent (f i)
h_comm : ∀ (i j : ι), Membership.mem (γ := Finset ι) ∅ i → Membership.mem (γ := Finset ι) ∅ j → Commute (f i) (f j)
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ ∅, f i)

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ insert j s, f i)

Tactic:
?_
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
s : Finset ι
f : ι → R
hnp : ∀ i ∈ s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)
insert :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ Insert.insert j s, f i)
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih => ?_

Premises used: Insert.insert
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)
insert : IsNilpotent (f j + ∑ x ∈ s, f x)
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ Insert.insert j s, f i)

Tactic:
rw [Finset.sum_insert hj]

Premises used: Finset.sum_insert
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)
insert : Commute (f j) (∑ x ∈ s, f x)
insert₁ : IsNilpotent (f j)
insert₂ : IsNilpotent.{u_1} (R := R) (∑ x ∈ s, f x)
⊢ IsNilpotent (f j + ∑ x ∈ s, f x)

Tactic:
apply Commute.isNilpotent_add

Premises used: Commute.isNilpotent_add
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ j ∈ insert j s

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ i ∈ insert j s

Tactic:
simp [hi]
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ Commute (f j) (∑ x ∈ s, f x)

Tactic:
exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))

Premises used: Commute.sum_right
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)
insert : j ∈ Insert.insert j s
⊢ IsNilpotent (f j)

Tactic:
apply hnp
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ j ∈ insert j s

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j_1 : ι
s : Finset ι
hj_1 : j_1 ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j_1 s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j_1 s → j ∈ insert j_1 s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i ∈ insert j_1 s

Tactic:
simp [hi]
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j_1 : ι
s : Finset ι
hj_1 : j_1 ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j_1 s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j_1 s → j ∈ insert j_1 s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ j ∈ insert j_1 s

Tactic:
simp [hj]
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih :
  ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent.{u_1} (R := R) (∑ x ∈ s, f x)

Tactic:
exact ih (fun i hi ↦ hnp i (by simp [hi]))
      (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
pos : ∀ (h : HasFiniteSupport f), IsNilpotent (finsum f)
neg : ∀ (h : ¬HasFiniteSupport f), IsNilpotent (finsum f)
⊢ IsNilpotent (finsum f)

Tactic:
by_cases h : HasFiniteSupport f

Premises used: Function.HasFiniteSupport
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
pos : IsNilpotent.{u_1} (R := R) (∑ i ∈ Finite.toFinset (s := support f) h, f i)
⊢ IsNilpotent (finsum f)

Tactic:
rw [finsum_def, dif_pos h]

Premises used: dif_pos, finsum_def
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ Finite.toFinset (s := support f) h, f i)

Tactic:
Commute.isNilpotent_sum (fun b _ ↦ hf b) (fun _ _ _ _ ↦ h_comm _ _)

Premises used: Commute.isNilpotent_sum
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ Finite.toFinset (s := support f) h, f i)

Tactic:
exact Commute.isNilpotent_sum (fun b _ ↦ hf b) (fun _ _ _ _ ↦ h_comm _ _)

Premises used: Commute.isNilpotent_sum
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : ¬HasFiniteSupport f
⊢ IsNilpotent (finsum f)

Tactic:
simp only [finsum_def, dif_neg h, IsNilpotent.zero]

Premises used: dif_neg, finsum_def, IsNilpotent.zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
pos : ∀ (h : HasFiniteSupport f), IsNilpotent (finsum f)
neg neg₁ : ∀ (h : ¬HasFiniteSupport f), IsNilpotent (finsum f)
⊢ IsNilpotent (finsum f)

Tactic:
classical
  by_cases h : HasFiniteSupport f
  · rw [finsum_def, dif_pos h]
    exact Commute.isNilpotent_sum (fun b _ ↦ hf b) (fun _ _ _ _ ↦ h_comm _ _)
  · simp only [finsum_def, dif_neg h, IsNilpotent.zero]

Premises used: Function.HasFiniteSupport, Commute.isNilpotent_sum, finsum_def, IsNilpotent.zero
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) y
⊢ IsNilpotent (x * y) ↔ IsNilpotent x

Tactic:
⟨?_, h_comm.isNilpotent_mul_right⟩

Premises used: Iff.intro, Commute.isNilpotent_mul_right
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) y
refine : IsNilpotent (x * y) → IsNilpotent x
⊢ IsNilpotent (x * y) ↔ IsNilpotent x

Tactic:
refine ⟨?_, h_comm.isNilpotent_mul_right⟩
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) y
k : ℕ
hk : (x * y) ^ k = 0
⊢ x ^ k * y ^ k = 0

Tactic:
rw [mul_pow h_comm] at hk

Premises used: Commute.mul_pow
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) y
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent x

Tactic:
⟨k, (nonZeroDivisorsRight R).pow_mem hy k _ hk⟩

Premises used: nonZeroDivisorsRight, Submonoid.pow_mem, Exists.intro, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) y
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent x

Tactic:
exact ⟨k, (nonZeroDivisorsRight R).pow_mem hy k _ hk⟩
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) x
⊢ IsNilpotent (x * y) ↔ IsNilpotent y

Tactic:
⟨?_, h_comm.isNilpotent_mul_left⟩

Premises used: Commute.isNilpotent_mul_left, Iff.intro
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) x
refine : IsNilpotent (x * y) → IsNilpotent y
⊢ IsNilpotent (x * y) ↔ IsNilpotent y

Tactic:
refine ⟨?_, h_comm.isNilpotent_mul_left⟩
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) x
k : ℕ
hk : (x * y) ^ k = 0
⊢ x ^ k * y ^ k = 0

Tactic:
rw [mul_pow h_comm] at hk

Premises used: Commute.mul_pow
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) x
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent y

Tactic:
⟨k, (nonZeroDivisorsLeft R).pow_mem hx k _ hk⟩

Premises used: Submonoid.pow_mem, Exists.intro, IsNilpotent, nonZeroDivisorsLeft
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) x
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent y

Tactic:
exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hx k _ hk⟩
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ Commute x (-y)

Tactic:
rw [← neg_right_iff] at h_comm

Premises used: Commute.neg_right_iff
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
h_comm₁ : Commute x (-y)
⊢ IsNilpotent x

Tactic:
rw [← neg_right_iff] at h_comm

Premises used: Commute.neg_right_iff
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
h_comm₁ : Commute x (-y)
hx₁ : IsNilpotent x
⊢ IsNilpotent y

Tactic:
rw [← neg_right_iff] at h_comm

Premises used: Commute.neg_right_iff
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (-y)

Tactic:
rw [← isNilpotent_neg_iff] at hy

Premises used: isNilpotent_neg_iff
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
rw : IsNilpotent (x + -y)
⊢ IsNilpotent (x - y)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)

Tactic:
h_comm.isNilpotent_add hx hy

Premises used: Commute.isNilpotent_add
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
x y : R
inst : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)

Tactic:
exact h_comm.isNilpotent_add hx hy

Premises used: Commute.isNilpotent_add
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → R
hnp : ∀ i ∈ s, IsNilpotent (f i)
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)

Tactic:
Commute.isNilpotent_sum hnp fun _ _ _ _ ↦ Commute.all _ _

Premises used: Commute.isNilpotent_sum, Commute.all
-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
⊢ IsNilpotent (finsum f)

Tactic:
Commute.isNilpotent_finsum hf fun _ _ ↦ Commute.all _ _

Premises used: Commute.isNilpotent_finsum, Commute.all
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
r : R
F : Type u_3
inst_2 : FunLike F R S
inst_3 : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
h : HPow.hPow (α := S) ((f : (a : R) → S) r : S) (Exists.choose (p := fun (n : ℕ) ↦ r ^ n = 0) hr) = 0
⊢ IsNilpotent.{u_2} (R := S) ((f : (a : R) → S) r : S)

Tactic:
use hr.choose

Premises used: Exists.choose
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
r : R
F : Type u_3
inst_2 : FunLike F R S
inst_3 : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
h : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (r ^ Exists.choose (p := fun (n : ℕ) ↦ r ^ n = 0) hr) : S) (0 : S)
h₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
h₂ h₃ : Eq.{u_2 + 1} (α := S) 0 0
⊢ HPow.hPow (α := S) ((f : (a : R) → S) r : S) (Exists.choose (p := fun (n : ℕ) ↦ r ^ n = 0) hr) = 0

Tactic:
rw [← map_pow, hr.choose_spec, map_zero]

Premises used: Exists.choose_spec, map_zero, map_pow
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
r : R
F : Type u_3
inst_2 : FunLike F R S
inst_3 : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsNilpotent.{u_2} (R := S) ((f : (a : R) → S) r : S)
k : ℕ
hk rwa rwa₁ rwa₂ rwa₃ : HPow.hPow (α := S) ((f : (a : R) → S) r : S) k = 0
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (r ^ k) : S) (0 : S)

Tactic:
rwa [map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
r u : R
hu : IsUnit u
h_comm : Commute r u
n : ℕ
rw : r ^ n * u ^ n = 0 ↔ r ^ n = 0
rw₁ rw₂ : r ^ n = 0 ↔ r ^ n = 0
⊢ (r * u) ^ n = 0 ↔ r ^ n = 0

Tactic:
rw [h_comm.mul_pow, (hu.pow n).mul_left_eq_zero]

Premises used: IsUnit.mul_left_eq_zero, IsUnit.pow, Commute.mul_pow
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
r u : R
hu : IsUnit u
h_comm : Commute r u
⊢ IsNilpotent (u * r) ↔ IsNilpotent r

Tactic:
h_comm ▸ hu.isNilpotent_mul_unit_of_commute_iff h_comm

Premises used: Eq.rec, IsUnit.isNilpotent_mul_unit_of_commute_iff
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : Subsingleton R
s : Set ℕ := {k : ℕ | x ^ k = 0}
this : Eq (α := Set ℕ) {k : ℕ | x ^ k = 0} univ
⊢ Eq (α := ℕ) (sInf {k : ℕ | x ^ k = 0}) 0

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : Subsingleton R
s : Set ℕ := {k : ℕ | x ^ k = 0}
suffices : s = univ
⊢ nilpotencyClass x = 0

Tactic:
suffices s = univ by change sInf _ = 0; simp [s] at this; simp [this]
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : Subsingleton R
s : Set ℕ := {k : ℕ | x ^ k = 0}
⊢ s = univ

Tactic:
eq_univ_iff_forall.mpr fun k ↦ Subsingleton.elim _ _

Premises used: Iff.mpr, Set.eq_univ_iff_forall, HPow.hPow, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
inst_2 : Subsingleton R
s : Set ℕ := {k : ℕ | x ^ k = 0}
⊢ s = univ

Tactic:
exact eq_univ_iff_forall.mpr fun k ↦ Subsingleton.elim _ _

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Subsingleton.elim
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k : ℕ | x ^ k = 0}
change : s.Nonempty
⊢ IsNilpotent x

Tactic:
change s.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k : ℕ | x ^ k = 0}
⊢ 0 < sInf s

Tactic:
change 0 < sInf s at hx

Premises used: InfSet.sInf