-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_add_of_commute_of_mem_ball [CharZero 𝕂] {x y : 𝔸} (hxy : Commute x y)
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius)
    (hy : y ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (x_1 : ℕ), ∑ x_2 ∈ Finset.antidiagonal x_1, (↑x_1 !)⁻¹ • x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Tactic:
refine tsum_congr fun n => Finset.sum_congr rfl fun kl hkl => ?_

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ (↑n !)⁻¹ • n.choose kl.1 • (x ^ kl.1 * y ^ kl.2) = (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Proof state:
case e_a
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ (↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!)) = (↑kl.1!)⁻¹ * (↑kl.2!)⁻¹

Tactic:
have : (n ! : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr n.factorial_ne_zero

Result:
case e_a
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
this : ↑n ! ≠ 0
⊢ (↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!)) = (↑kl.1!)⁻¹ * (↑kl.2!)⁻¹

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x + y) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Tactic:
dsimp only

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y

Tactic:
rw [exp_eq_tsum,
  tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
    (norm_expSeries_summable_of_mem_ball' x hx) (norm_expSeries_summable_of_mem_ball' y hy)]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x + y) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ (↑n !)⁻¹ • n.choose kl.1 • (x ^ kl.1 * y ^ kl.2) = (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Tactic:
rw [← Nat.cast_smul_eq_nsmul 𝕂, smul_smul, smul_mul_smul_comm, ← Finset.mem_antidiagonal.mp hkl,
  Nat.cast_add_choose, Finset.mem_antidiagonal.mp hkl]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)

Proof state:
case e_a
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
this : ↑n ! ≠ 0
⊢ (↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!)) = (↑kl.1!)⁻¹ * (↑kl.2!)⁻¹

Tactic:
field_simp [this]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)

Tactic:
congr 1

Result:
case e_a
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ (↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!)) = (↑kl.1!)⁻¹ * (↑kl.2!)⁻¹

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Tactic:
conv_lhs =>
  congr
  ext
  rw [hxy.add_pow' _, Finset.smul_sum]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (x_1 : ℕ), ∑ x_2 ∈ Finset.antidiagonal x_1, (↑x_1 !)⁻¹ • x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2