-- Mathlib/RingTheory/Nilpotent/Exp.lean
theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a) (h₃ : IsNilpotent b) :
    exp (a + b) = exp a * exp b

Proof state:
case calc_3.i_inj
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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)
⊢ ∀ (a₁ : (_ : ℕ) × ℕ) (ha₁ : a₁ ∈ (range (2 * N + 1)).sigma fun i => range (i + 1)) (a₂ : (_ : ℕ) × ℕ)
    (ha₂ : a₂ ∈ (range (2 * N + 1)).sigma fun i => range (i + 1)),
    ((match a₁, ha₁ with
        | ⟨i, j⟩, x => (j, i - j)) =
        match a₂, ha₂ with
        | ⟨i, j⟩, x => (j, i - j)) →
      a₁ = a₂

Tactic:
simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]

Result:
case calc_3.i_inj
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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)
⊢ ∀ (a₁ : (_ : ℕ) × ℕ),
    a₁.fst < 2 * N + 1 →
      a₁.snd < a₁.fst + 1 →
        ∀ (a₂ : (_ : ℕ) × ℕ),
          a₂.fst < 2 * N + 1 → a₂.snd < a₂.fst + 1 → a₁.snd = a₂.snd → a₁.fst - a₁.snd = a₂.fst - a₂.snd → a₁ = a₂

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ exp (a + b) = exp a * exp b

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

Result:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ ∑ i ∈ range (2 * N + 1), (↑i !)⁻¹ • (a + b) ^ i =
    (∑ i ∈ range (N + 1), (↑i !)⁻¹ • a ^ i) * ∑ i ∈ range (N + 1), (↑i !)⁻¹ • b ^ i

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
⊢ exp (a + b) = exp a * exp b

Tactic:
have h₅ : b ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₂

Result:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ exp (a + b) = exp a * exp b

Proof state:
case calc_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i !)⁻¹ • (a ^ j * b ^ (i - j) * ↑(i.choose j)) = ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))

Tactic:
suffices (i ! : ℚ)⁻¹ * (i.choose j) = ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) by
  rw [← Nat.cast_commute (i.choose j), ← this, ← Algebra.mul_smul_comm, ← nsmul_eq_mul,
    mul_smul, ← smul_assoc, smul_comm, smul_assoc]
  norm_cast

Result:
case calc_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
h₂ : IsNilpotent a
h₃ : IsNilpotent b
⊢ exp (a + b) = exp a * exp b

Tactic:
obtain ⟨n₁, hn₁⟩ := h₂

Result:
case intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
h₃ : IsNilpotent b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
⊢ exp (a + b) = exp a * exp b

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ ij ∈ filter (fun ij => ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i

Tactic:
have split₁ := sum_filter_add_sum_filter_not (R2N ×ˢ R2N)
  (fun ij ↦ ij.1 + ij.2 ≤ 2 * N)
  (fun ij ↦ ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))

Result:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ ij ∈ filter (fun ij => ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) +
      ∑ x ∈ filter (fun x => ¬x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i

Proof state:
case calc_2.hfg
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := 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₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ :
  ∑ ij ∈ filter (fun ij => ¬(ij.1 ≤ N ∧ ij.2 ≤ N)) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ filter (fun x => x.1 ≤ N ∧ x.2 ≤ N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ filter (fun ij => ij.1 ≤ N ∧ ij.2 ≤ N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
⊢ ∀ i ∈ RN.sigma fun i => RN,
    ((↑i.fst !)⁻¹ * (↑i.snd !)⁻¹) • (a ^ i.fst * b ^ i.snd) =
      ((↑(match i with
                  | ⟨i, j⟩ => (i, j)).1!)⁻¹ *
          (↑(match i with
                  | ⟨i, j⟩ => (i, j)).2!)⁻¹) •
        (a ^
            (match i with
              | ⟨i, j⟩ => (i, j)).1 *
          b ^
            (match i with
              | ⟨i, j⟩ => (i, j)).2)

Tactic:
simp only [implies_true]

Result:
no goals