awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (hypothesis)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
k : ℕ
s : Set ℕ := {k : ℕ | x ^ k = 0}
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0
have this : ∀ (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₁
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0 ∧ HPow.hPow (α := R) (β := ℕ) 0 0 ≠ 0
have left : HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
left : HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0
⊢ HPow.hPow (α := R) 0 (HAdd.hAdd (α := ℕ) 0 1) = 0 ∧ HPow.hPow (α := R) (β := ℕ) 0 0 ≠ 0
have right : HPow.hPow (α := R) (β := ℕ) 0 0 ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ 0 < nilpotencyClass x ↔ IsNilpotent x
have refine : ∀ (hx : IsNilpotent x) (hx' : nilpotencyClass x = 0), False
Tactic: refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (hypothesis)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx : IsNilpotent x
hx' : nilpotencyClass x = 0
⊢ False
have hx₁ : x ^ nilpotencyClass x = 0
Tactic: replace hx := pow_nilpotencyClass hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (hypothesis)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
inst_1 : Nontrivial R
hx' : nilpotencyClass x = 0
hx : x ^ nilpotencyClass x = 0
⊢ False
have hx₁ : Eq.{u_1 + 1} (α := R) 1 0
Tactic: rw [hx', pow_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (hypothesis)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
hx : nilpotencyClass x = 1
⊢ x = 0
have this : IsNilpotent x
Tactic: have : IsNilpotent x := isNilpotent_of_pos_nilpotencyClass (hx ▸ Nat.one_pos)
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = 0
have rw : x = x ^ nilpotencyClass x
Tactic: rw [← pow_nilpotencyClass this, hx, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x : R
inst : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
rw : x = x ^ nilpotencyClass x
⊢ x = 0
have rw₁ : x = HPow.hPow (β := ℕ) x 1
Tactic: rw [← pow_nilpotencyClass this, hx, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
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
⊢ x = 0
have rw₂ : x = x
Tactic: rw [← pow_nilpotencyClass this, hx, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
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
⊢ IsReduced R
have eq_zero : ∀ (x : R), IsNilpotent x → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
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
⊢ x = 0
have eq_zero : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
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) ((f : (a : R) → S) 0 : S)
have eq_zero : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
h : IsNilpotent x
⊢ IsNilpotent (x * y)
have obtain : ∀ (n : ℕ) (hn : x ^ n = 0), IsNilpotent (x * y)
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x * y)
have h : (x * y) ^ n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ (x * y) ^ n = 0
have h : x ^ n * y ^ n = 0
Tactic: rw [h_comm.mul_pow, hn, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
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
⊢ (x * y) ^ n = 0
have h₁ : 0 * y ^ n = 0
Tactic: rw [h_comm.mul_pow, hn, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
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
⊢ (x * y) ^ n = 0
have h₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [h_comm.mul_pow, hn, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Defs (goal)
Goal:
R : Type u_1
x y : R
inst : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (x * y)
have rw : IsNilpotent (y * x)
Tactic: rw [h_comm.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
⊢ exp a = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
have 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))
Tactic: rw [h₁, this, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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))
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
have rw₁ : ∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) =
  HAdd.hAdd (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) 0
Tactic: rw [h₁, this, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
have rw₂ : Eq.{u_1 + 1} (α := A) (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
  (∑ i ∈ range (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
Tactic: rw [h₁, this, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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))
⊢ exp a = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)
have suffices : Eq.{u_1 + 1} (α := A) (∑ i ∈ Ico (nilpotencyClass a) k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i)) 0
Tactic: suffices ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) = 0 by
    dsimp [exp]
    rw [h₁, this, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑x ! : ℚ)⁻¹ (a ^ x) = 0
have rw : HSMul.hSMul (α := ℚ) (β := A) (↑x ! : ℚ)⁻¹ 0 = 0
Tactic: rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑x ! : ℚ)⁻¹ (a ^ x) = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
have inl : ∀ (h₀ : nilpotencyClass a ≤ k), exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
Tactic: rcases le_or_gt (nilpotencyClass a) k with h₀ | h₀
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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)
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
have inr : ∀ (h₀ : k < nilpotencyClass a), exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
Tactic: rcases le_or_gt (nilpotencyClass a) k with h₀ | h₀
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
have 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)
Tactic: simp_rw [exp_eq_sum (pow_eq_zero_of_le h₀ (pow_nilpotencyClass hn)), sum_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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)
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
have inl₁ : Eq.{u_2 + 1} (α := M) (∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • 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]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ exp a • m = ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
have 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)
Tactic: rw [exp, sum_smul, ← sum_range_add_sum_Ico _ (Nat.le_of_succ_le h₀)]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ 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)
have simp_rw : HAdd.hAdd (α := M) (∑ k ∈ range k, HSMul.hSMul (α := ℚ) (↑k ! : ℚ)⁻¹ (a ^ k) • m) 0 =
  ∑ i ∈ range k, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i • m)
Tactic: simp_rw [this, add_zero, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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)
⊢ 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)
have 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))
Tactic: simp_rw [this, add_zero, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ 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)
have inr : Eq.{u_2 + 1} (α := M) (∑ i ∈ Ico k (nilpotencyClass a), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i) • m) 0
Tactic: suffices ∑ i ∈ Ico k (nilpotencyClass a), ((i.factorial : ℚ)⁻¹ • (a ^ i)) • m = 0 by
    simp_rw [this, add_zero, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
have inr : ∀ (r : ℕ) (h₂ : r ∈ Ico k (nilpotencyClass a)), HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
Tactic: refine sum_eq_zero fun r h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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)
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
have inr : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
have inr₁ : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ ((a ^ (r - k) * a ^ k) • m) = 0
Tactic: rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
have inr₂ : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ (r - k) • a ^ k • m) = 0
Tactic: rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
have inr₃ : HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (HSMul.hSMul (β := M) (a ^ (r - k)) 0) = 0
Tactic: rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
have inr₄ : HSMul.hSMul (α := ℚ) (β := M) (↑r ! : ℚ)⁻¹ 0 = 0
Tactic: rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ HSMul.hSMul (α := ℚ) (↑r ! : ℚ)⁻¹ (a ^ r) • m = 0
have inr₅ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ exp (a + b) = exp a * exp b
have obtain : ∀ (n₁ : ℕ) (hn₁ : a ^ n₁ = 0), exp (a + b) = exp a * exp b
Tactic: obtain ⟨n₁, hn₁⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
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
⊢ exp (a + b) = exp a * exp b
have obtain : ∀ (n₂ : ℕ) (hn₂ : b ^ n₂ = 0), exp (a + b) = exp a * exp b
Tactic: obtain ⟨n₂, hn₂⟩ := h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
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₂
⊢ exp (a + b) = exp a * exp b
have h₄ : a ^ (N + 1) = 0
Tactic: have h₄ : a ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₁
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
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
⊢ exp (a + b) = exp a * exp b
have h₅ : b ^ (N + 1) = 0
Tactic: have h₅ : b ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₂