awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
s : Set ℕ := {k : ℕ | x ^ k = 0}
hx : 0 < sInf s
by_contra : ∀ (contra : ¬s.Nonempty), False
⊢ s.Nonempty

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

Tactic:
simp [not_nonempty_iff_eq_empty.mp contra] at hx

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : Zero R
inst_1 : Pow R ℕ
hx : IsNilpotent x
⊢ x ^ nilpotencyClass x = 0

Tactic:
Nat.sInf_mem hx

Premises used: Set.Mem, setOf, Nat.sInf_mem, nilpotencyClass
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
k : ℕ
s : Set ℕ := {k : ℕ | x ^ k = 0}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s

Tactic:
have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
k : ℕ
s : Set ℕ := {k : ℕ | x ^ k = 0}
this : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Tactic:
simp [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]

Premises used: nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
left : HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0
right : HPow.hPow (α := R) (β := ℕ) 0 0 ≠ 0
⊢ HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0 ∧ HPow.hPow (α := R) (β := ℕ) 0 0 ≠ 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ HPow.hPow (α := R) (β := ℕ) 0 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ 0 < nilpotencyClass x ↔ IsNilpotent x

Tactic:
⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩

Premises used: isNilpotent_of_pos_nilpotencyClass, Nat.pos_of_ne_zero, Iff.intro
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
refine : ∀ (hx : IsNilpotent x) (hx' : nilpotencyClass x = 0), False
⊢ 0 < nilpotencyClass x ↔ IsNilpotent x

Tactic:
refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx : IsNilpotent x
hx' : nilpotencyClass x = 0
⊢ x ^ nilpotencyClass x = 0

Tactic:
replace hx := pow_nilpotencyClass hx
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx' : nilpotencyClass x = 0
hx : x ^ nilpotencyClass x = 0
⊢ Eq.{u_1 + 1} (α := R) 1 0

Tactic:
rw [hx', pow_zero] at hx

Premises used: pow_zero
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx' : nilpotencyClass x = 0
hx : Eq.{u_1 + 1} (α := R) 1 0
⊢ False

Tactic:
one_ne_zero hx

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx' : nilpotencyClass x = 0
hx : Eq.{u_1 + 1} (α := R) 1 0
⊢ False

Tactic:
exact one_ne_zero hx

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx : IsNilpotent x
⊢ x ^ (nilpotencyClass x - 1) ≠ 0

Tactic:
(nilpotencyClass_eq_succ_iff.mp <| Nat.eq_add_of_sub_eq (pos_nilpotencyClass_iff.mpr hx) rfl).2

Premises used: Iff.mpr, pos_nilpotencyClass_iff, Nat.eq_add_of_sub_eq, And.right, Iff.mp, nilpotencyClass_eq_succ_iff, rfl
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
hx : nilpotencyClass x = 1
⊢ IsNilpotent x

Tactic:
have : IsNilpotent x := isNilpotent_of_pos_nilpotencyClass (hx ▸ Nat.one_pos)
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
rw : x = x ^ nilpotencyClass x
rw₁ : x = HPow.hPow (β := ℕ) x 1
rw₂ rw₃ : x = x
⊢ x = 0

Tactic:
rw [← pow_nilpotencyClass this, hx, pow_one]

Premises used: pow_nilpotencyClass, pow_one
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ nilpotencyClass x = 1 ↔ x = 0

Tactic:
⟨eq_zero_of_nilpotencyClass_eq_one, fun hx ↦ hx ▸ nilpotencyClass_zero⟩

Premises used: Eq.rec, eq_zero_of_nilpotencyClass_eq_one, Iff.intro, nilpotencyClass_zero, Eq.symm
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
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)
inst_4 : IsReduced S
eq_zero : ∀ (x : R), IsNilpotent x → x = 0
⊢ IsReduced R

Tactic:
constructor
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
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)
inst_4 : IsReduced S
x : R
hx : IsNilpotent x
eq_zero : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S)
⊢ x = 0

Tactic:
apply hf
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
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)
inst_4 : IsReduced S
x : R
hx : IsNilpotent x
eq_zero : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
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)
inst_4 : IsReduced S
x : R
hx : IsNilpotent x
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)

Tactic:
(hx.map f).eq_zero

Premises used: IsNilpotent.map, IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
S : Type u_2
inst : MonoidWithZero R
inst_1 : MonoidWithZero S
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)
inst_4 : IsReduced S
x : R
hx : IsNilpotent x
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)

Tactic:
exact (hx.map f).eq_zero

Premises used: IsNilpotent.map, IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
y : R
inst : Monoid R
k : ℕ
hk : 1 < k
⊢ IsRadical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x

Tactic:
⟨(· k), k.pow_imp_self_of_one_lt hk _ fun _ _ h ↦ .inl (dvd_mul_of_dvd_left h _)⟩

Premises used: dvd_mul_of_dvd_left, Iff.intro, Or.inl, Nat.pow_imp_self_of_one_lt
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
h : IsNilpotent x
obtain : ∀ (n : ℕ) (hn : x ^ n = 0), IsNilpotent (x * y)
⊢ IsNilpotent (x * y)

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

Tactic:
use n
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
h : x ^ n * y ^ n = 0
h₁ : 0 * y ^ n = 0
h₂ h₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (x * y) ^ n = 0

Tactic:
rw [h_comm.mul_pow, hn, zero_mul]

Premises used: MulZeroClass.zero_mul, Commute.mul_pow
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
h : IsNilpotent y
rw : IsNilpotent (y * x)
⊢ IsNilpotent (x * y)

Tactic:
rw [h_comm.eq]

Premises used: Commute.eq
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)

Tactic:
h_comm.symm.isNilpotent_mul_right h

Premises used: Commute.symm, Commute.isNilpotent_mul_right
-- Module: Mathlib.RingTheory.Nilpotent.Defs
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)

Tactic:
exact h_comm.symm.isNilpotent_mul_right h

Premises used: Commute.symm, Commute.isNilpotent_mul_right
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
⊢ ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))

Tactic:
have h₁ : ∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) =
      ∑ i ∈ range (nilpotencyClass a), (i.factorial : ℚ)⁻¹ • (a ^ i) +
        ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) :=
    (sum_range_add_sum_Ico _ (csInf_le' h)).symm
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
this : Eq.{u_1 + 1} (α := A) (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) 0
rw :
  ∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
rw₁ :
  ∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) 0
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))

Tactic:
rw [h₁, this, add_zero]

Premises used: add_zero
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
suffices : Eq.{u_1 + 1} (α := A) (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) 0
⊢ exp a = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)

Tactic:
suffices ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) = 0 by
    dsimp [exp]
    rw [h₁, this, add_zero]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
x : ℕ
h₂ : x ∈ Ico (nilpotencyClass a) k
rw : HSMul.hSMul (α := ℚ) (β := A) (↑x ! : ℚ)⁻¹ 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ HSMul.hSMul (α := ℚ) (↑x ! : ℚ)⁻¹ (a ^ x) = 0

Tactic:
rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]

Premises used: pow_eq_zero_of_le, smul_zero, pow_nilpotencyClass, And.left, Exists.intro, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
    HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) 0

Tactic:
exact sum_eq_zero fun _ h₂ => by
    rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
inl : ∀ (h₀ : nilpotencyClass a ≤ k), exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
inr : ∀ (h₀ : k < nilpotencyClass a), exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)

Tactic:
rcases le_or_gt (nilpotencyClass a) k with h₀ | h₀

Premises used: nilpotencyClass, le_or_gt
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : nilpotencyClass a ≤ k
inl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := A) (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) m =
    ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
inl₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • m)
    (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m))
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)

Tactic:
simp_rw [exp_eq_sum (pow_eq_zero_of_le h₀ (pow_nilpotencyClass hn)), sum_smul, smul_assoc]

Premises used: Finset.sum_smul, smul_assoc, pow_eq_zero_of_le, pow_nilpotencyClass, IsNilpotent.exp_eq_sum
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
inr :
  HAdd.hAdd (α := M) (∑ k ∈ range k, HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m)
      (∑ k ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m) =
    ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)

Tactic:
rw [exp, sum_smul, ← sum_range_add_sum_Ico _ (Nat.le_of_succ_le h₀)]

Premises used: Finset.sum_smul, Finset.sum_range_add_sum_Ico, Nat.le_of_succ_le, IsNilpotent.exp
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
this : Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • m) 0
simp_rw :
  HAdd.hAdd (α := M) (∑ k ∈ range k, HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m) 0 =
    ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
simp_rw₁ :
  Eq.{u_2 + 1} (α := M) (∑ k ∈ range k, HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m)
    (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m))
⊢ HAdd.hAdd (α := M) (∑ k ∈ range k, HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m)
      (∑ k ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m) =
    ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)

Tactic:
simp_rw [this, add_zero, smul_assoc]

Premises used: smul_assoc, add_zero
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
inr : Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • m) 0
⊢ HAdd.hAdd (α := M) (∑ k ∈ range k, HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m)
      (∑ k ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m) =
    ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)

Tactic:
suffices ∑ i ∈ Ico k (nilpotencyClass a), ((i.factorial : ℚ)⁻¹ • (a ^ i)) • m = 0 by
    simp_rw [this, add_zero, smul_assoc]
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • m) 0

Tactic:
sum_eq_zero fun r h₂ ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
inr : ∀ (r : ℕ) (h₂ : r ∈ Ico k (nilpotencyClass a)), HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • m) 0

Tactic:
refine sum_eq_zero fun r h₂ ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module A M
inst_4 : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
r : ℕ
h₂ : r ∈ Ico k (nilpotencyClass a)
inr : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r • m) = 0
inr₁ : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ ((a ^ (r - k) * a ^ k) • m) = 0
inr₂ : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ (r - k) • a ^ k • m) = 0
inr₃ : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (HSMul.hSMul (β := M) (a ^ (r - k)) 0) = 0
inr₄ : HSMul.hSMul (α := ℚ) (β := M) (↑r ! : ℚ)⁻¹ 0 = 0
inr₅ inr₆ : Eq.{u_2 + 1} (α := M) 0 0
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0

Tactic:
rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]

Premises used: smul_assoc, smul_zero, pow_sub_mul_pow, And.left, Iff.mp, SemigroupAction.mul_smul, Finset.mem_Ico
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
h₂ : IsNilpotent a
h₃ : IsNilpotent b
obtain : ∀ (n₁ : ℕ) (hn₁ : a ^ n₁ = 0), exp (a + b) = exp a * exp b
⊢ exp (a + b) = exp a * exp b

Tactic:
obtain ⟨n₁, hn₁⟩ := h₂
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
h₃ : IsNilpotent b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
obtain : ∀ (n₂ : ℕ) (hn₂ : b ^ n₂ = 0), exp (a + b) = exp a * exp b
⊢ exp (a + b) = exp a * exp b

Tactic:
obtain ⟨n₂, hn₂⟩ := h₃
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
⊢ n₁ ≤ N + 1

Tactic:
omega
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
⊢ a ^ (N + 1) = 0

Tactic:
have h₄ : a ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₁
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
⊢ n₂ ≤ N + 1

Tactic:
omega
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
⊢ b ^ (N + 1) = 0

Tactic:
have h₅ : b ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₂
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ N + 1 + (N + 1) ≤ 2 * N + 1 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
rw :
  ∑ i ∈ range (2 * N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
⊢ exp (a + b) = exp a * exp b

Tactic:
rw [exp_eq_sum (k := 2 * N + 1)
    (Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero h₁ h₄ h₅ (by lia)),
    exp_eq_sum h₄, exp_eq_sum h₅]

Premises used: Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero, IsNilpotent.exp_eq_sum
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
set :
  let R2N := range (2 * N + 1);
  ∀ (hR2N : R2N = range (2 * N + 1)),
    ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
      HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
        (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
⊢ ∑ i ∈ range (2 * N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))

Tactic:
set R2N := range (2 * N + 1) with hR2N

Premises used: HMul.hMul, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
set :
  let RN := range (N + 1);
  ∀ (hRN : RN = range (N + 1)),
    ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
      HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
        (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
⊢ ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))

Tactic:
set RN := range (N + 1) with hRN

Premises used: Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ i ∈ R2N,
      HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))

Tactic:
?_