awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
z₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
z₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N),
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
restrict :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
⊢ Eq.{u_1 + 1} (α := A)
    (∑ x ∈ RN.sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ RN,
      HMul.hMul (α := ℚ) (↑x.fst (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ (↑x.snd (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ •
        (a ^ x.fst (β := fun (i : ℕ) ↦ ℕ) * b ^ x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_2 : Function.Bijective (β := ℕ × ℕ) fun (x : (_ : ℕ) × ℕ) ↦
  match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) x with
  | ⟨i, j⟩ => (i, j)
Tactic: apply sum_bijective (fun ⟨i, j⟩ ↦ (i, j))
-- 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
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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
z₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
z₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N),
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
restrict :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
calc_2 :
  Function.Bijective (β := ℕ × ℕ) fun (x : (_ : ℕ) × ℕ) ↦
    match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) x with
    | ⟨i, j⟩ => (i, j)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ x ∈ RN.sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ RN,
      HMul.hMul (α := ℚ) (↑x.fst (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ (↑x.snd (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ •
        (a ^ x.fst (β := fun (i : ℕ) ↦ ℕ) * b ^ x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_2₁ : ∀ (i : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) (RN.sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ RN) i ↔
    Membership.mem (α := ℕ × ℕ) (RN ×ˢ RN)
      (match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) i with
        | ⟨i, j⟩ => (i, j) :
        ℕ × ℕ)
Tactic: apply sum_bijective (fun ⟨i, j⟩ ↦ (i, j))
-- 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
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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
z₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
z₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N),
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
restrict :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
x x_1 : (_ : ℕ) × ℕ
i j i' j' : ℕ
h :
  Eq (α := ℕ × ℕ)
    ((fun (x : (_ : ℕ) × ℕ) ↦
        (match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) x with
          | ⟨i, j⟩ => (i, j) :
          ℕ × ℕ))
      (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) i j))
    ((fun (x : (_ : ℕ) × ℕ) ↦
        (match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) x with
          | ⟨i, j⟩ => (i, j) :
          ℕ × ℕ))
      (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) i' j'))
⊢ Eq (α := (_ : ℕ) × ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) i j) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) i' j')
have refl : Eq (α := (_ : ℕ) × ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) i j) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) i j)
Tactic: cases h
Cleared hypotheses: i', j', 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₂
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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
z₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
z₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N),
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
restrict :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
⊢ ∑ 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))
have s₂ : HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i)) =
  ∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2)
Tactic: have s₂ := by
    calc (∑ i ∈ RN, (i ! : ℚ)⁻¹ • a ^ i) * ∑ i ∈ RN, (i ! : ℚ)⁻¹ • b ^ i
        = ∑ i ∈ RN, ∑ j ∈ RN, ((i ! : ℚ)⁻¹ * (j ! : ℚ)⁻¹) • (a ^ i * b ^ j) := ?_
      _ = ∑ ij ∈ RN ×ˢ RN, ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
    · rw [sum_mul_sum]
      refine sum_congr rfl fun _ _ ↦ sum_congr rfl fun _ _ ↦ ?_
      rw [smul_mul_assoc, mul_smul_comm, smul_smul]
    · rw [sum_sigma']
      apply sum_bijective (fun ⟨i, j⟩ ↦ (i, j))
      · exact ⟨fun ⟨i, j⟩ ⟨i', j'⟩ h ↦ by cases h; rfl, fun ⟨i, j⟩ ↦ ⟨⟨i, j⟩, rfl⟩⟩
      · simp only [mem_sigma, mem_product, implies_true]
      · simp only [implies_true]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
h : IsNilpotent a
⊢ IsUnit (exp a)
have apply : ∃ (b : A), exp a * b = 1 ∧ b * exp a = 1
Tactic: apply isUnit_iff_exists.2
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
h : IsNilpotent a
⊢ ∃ (b : A), exp a * b = 1 ∧ b * exp a = 1
have h₁ : exp a * exp (-a) = 1 ∧ exp (-a) * exp a = 1
Tactic: use exp (-a)
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
B : Type u_2
F : Type u_3
inst_2 : Ring B
inst_3 : FunLike F A B
inst_4 : RingHomClass F A B
inst_5 : Module ℚ B
a : A
ha : IsNilpotent a
f : F
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (exp a) : B) (exp ((f : (a : A) → B) a) : B)
have obtain : ∀ (k : ℕ) (hk : a ^ k = 0), Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (exp a) : B) (exp ((f : (a : A) → B) a) : B)
Tactic: obtain ⟨k, hk⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
B : Type u_2
F : Type u_3
inst_2 : Ring B
inst_3 : FunLike F A B
inst_4 : RingHomClass F A B
inst_5 : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (exp a) : B) (exp ((f : (a : A) → B) a) : B)
have hk' : HPow.hPow (α := B) ((f : (a : A) → B) a : B) k = 0
Tactic: have hk' : (f a) ^ k = 0 := by simp [← map_pow, hk]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
⊢ IsNilpotent (exp a - 1)
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
⊢ IsNilpotent (exp a - 1)
have rw : IsNilpotent
  (∑ k ∈ range (nilpotencyClass a - Nat.succ 0), HSMul.hSMul (α := ℚ) (↑(k + 1)! : ℚ)⁻¹ (a ^ (k + 1)) +
      HSMul.hSMul (α := ℚ) (↑0! : ℚ)⁻¹ (HPow.hPow (β := ℕ) a 0) -
    1)
Tactic: rw [exp, ← Nat.sub_add_cancel (pos_nilpotencyClass_iff.2 ha), Finset.sum_range_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
⊢ IsNilpotent
    (∑ k ∈ range (nilpotencyClass a - Nat.succ 0), HSMul.hSMul (α := ℚ) (↑(k + 1)! : ℚ)⁻¹ (a ^ (k + 1)) +
        HSMul.hSMul (α := ℚ) (↑0! : ℚ)⁻¹ (HPow.hPow (β := ℕ) a 0) -
      1)
have simp : IsNilpotent.{u_1} (R := A) (∑ x ∈ range (nilpotencyClass a - 1), HSMul.hSMul (α := ℚ) (↑(x + 1)! : ℚ)⁻¹ (a ^ (x + 1)))
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a : A
ha : IsNilpotent a
h : Nontrivial A
⊢ IsNilpotent.{u_1} (R := A) (∑ x ∈ range (nilpotencyClass a - 1), HSMul.hSMul (α := ℚ) (↑(x + 1)! : ℚ)⁻¹ (a ^ (x + 1)))
have apply : ∀ (i j : ℕ),
  i ∈ range (nilpotencyClass a - 1) →
    j ∈ range (nilpotencyClass a - 1) →
      Commute (HSMul.hSMul (α := ℚ) (↑(i + 1)! : ℚ)⁻¹ (a ^ (i + 1)))
        (HSMul.hSMul (α := ℚ) (↑(j + 1)! : ℚ)⁻¹ (a ^ (j + 1)))
Tactic: apply Commute.isNilpotent_sum fun _ _ ↦ smul (pow_of_pos ha <| by positivity) _
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
hfM : IsNilpotent fM
hfN : IsNilpotent fN
h : fN ∘ₗ g = g ∘ₗ fM
⊢ exp fN ∘ₗ g = g ∘ₗ exp fM
have h₁ : ∀ (m : M), Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
hfM : IsNilpotent fM
hfN : IsNilpotent fN
h : fN ∘ₗ g = g ∘ₗ fM
m : M
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
have h₁ : ∀ (k : ℕ) (hfM : fM ^ k = 0),
  Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
Tactic: obtain ⟨k, hfM⟩ := hfM
Cleared hypotheses: hfM
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
hfN : IsNilpotent fN
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k : ℕ
hfM : fM ^ k = 0
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
have h₁ : ∀ (l : ℕ) (hfN : fN ^ l = 0),
  Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
Tactic: obtain ⟨l, hfN⟩ := hfN
Cleared hypotheses: hfN
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k : ℕ
hfM : fM ^ k = 0
l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
have hfM₁ : fM ^ kl = 0
Tactic: replace hfM : fM ^ kl = 0 := pow_eq_zero_of_le (by omega) hfM
Cleared hypotheses: hfM
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
hfN : fN ^ l = 0
kl : ℕ := max k l
hfM : fM ^ kl = 0
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
have hfN₁ : fN ^ kl = 0
Tactic: replace hfN : fN ^ kl = 0 := pow_eq_zero_of_le (by omega) hfN
Cleared hypotheses: hfN
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module ℚ M
inst_6 : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
⊢ Eq.{u_3 + 1} (α := N) ((exp fN ∘ₗ g : (a : M) → N) m : N) ((g ∘ₗ exp fM : (a : M) → N) m : N)
have this : ∀ (i : ℕ),
  Eq (α := N) ((fN ^ i : (a : N) → N) ((g : (a : M) → N) m : N) : N)
    ((g : (a : M) → N) ((fM ^ i : (a : M) → M) m : M) : N)
Tactic: have (i : ℕ) : (fN ^ i) (g m) = g ((fM ^ i) m) := by
    simpa using LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h i) m
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have h_nilL : IsNilpotent DL
Tactic: have h_nilL : IsNilpotent DL := h_nil.map <| lTensorAlgHom R B B
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have h_nilR : IsNilpotent DR
Tactic: have h_nilR : IsNilpotent DR := h_nil.map <| rTensorAlgHom R B B
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
⊢ Commute DL DR
have a : ∀ (x x_1 : B),
  Eq (α := B ⊗[R] B)
    (((((AlgebraTensorModule.curry (DL * DR) : B →ₗ[R] B →ₗ[R] B ⊗[R] B) : (a : B) → B →ₗ[R] B ⊗[R] B) x :
            B →ₗ[R] B ⊗[R] B) :
          (a : B) → B ⊗[R] B)
        x_1 :
      B ⊗[R] B)
    (((((AlgebraTensorModule.curry (DR * DL) : B →ₗ[R] B →ₗ[R] B ⊗[R] B) : (a : B) → B →ₗ[R] B ⊗[R] B) x :
            B →ₗ[R] B ⊗[R] B) :
          (a : B) → B ⊗[R] B)
        x_1 :
      B ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have h_comm : Commute DL DR
Tactic: have h_comm : Commute DL DR := by ext; simp [DL, DR]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have hm : let m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B;
m = LinearMap.mul' R B
Tactic: set m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B with hm
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
⊢ Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
have suffices : exp D ∘ₗ m = m ∘ₗ exp (DL + DR)
Tactic: suffices exp D ∘ₗ m = m ∘ₗ exp (DL + DR) by simpa using LinearMap.congr_fun this (x ⊗ₜ[R] y)
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
⊢ exp D ∘ₗ m = m ∘ₗ exp (DL + DR)
have apply : D ∘ₗ m = m ∘ₗ (DL + DR)
Tactic: apply commute_exp_left_of_commute (h_comm.isNilpotent_add h_nilL h_nilR) h_nil
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
⊢ D ∘ₗ m = m ∘ₗ (DL + DR)
have a : ∀ (x x_1 : B),
  Eq (α := B)
    (((((AlgebraTensorModule.curry (D ∘ₗ m) : B →ₗ[R] B →ₗ[R] B) : (a : B) → B →ₗ[R] B) x : B →ₗ[R] B) : (a : B) → B)
        x_1 :
      B)
    (((((AlgebraTensorModule.curry (m ∘ₗ (DL + DR)) : B →ₗ[R] B →ₗ[R] B) : (a : B) → B →ₗ[R] B) x : B →ₗ[R] B) :
          (a : B) → B)
        x_1 :
      B)
Tactic: ext