-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_sum_of_commute {ι} (s : Finset ι) (f : ι → 𝔸)
    (h : (s : Set ι).Pairwise (Commute on f)) :
    exp 𝕂 (∑ i ∈ s, f i) =
      s.noncommProd (fun i => exp 𝕂 (f i)) fun _ hi _ hj _ => (h.of_refl hi hj).exp 𝕂

Proof state:
case insert
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ Commute (f a) (∑ x ∈ s, f x)

Tactic:
refine Commute.sum_right _ _ _ fun i hi => ?_

Result:
case insert
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
i : ι
hi : i ∈ s
⊢ Commute (f a) (f i)

Proof state:
case insert
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
i : ι
hi : i ∈ s
⊢ Commute (f a) (f i)

Tactic:
exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)

Result:
no goals

Proof state:
case insert
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ exp 𝕂 (∑ i ∈ insert a s, f i) = (insert a s).noncommProd (fun i => exp 𝕂 (f i)) ⋯

Tactic:
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
  ih (h.mono <| Finset.subset_insert _ _)]

Result:
case insert
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ Commute (f a) (∑ x ∈ s, f x)

Proof state:
case empty
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
h : (↑∅).Pairwise (Commute on f)
⊢ exp 𝕂 (∑ i ∈ ∅, f i) = ∅.noncommProd (fun i => exp 𝕂 (f i)) ⋯

Tactic:
simp

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
s : Finset ι
f : ι → 𝔸
h : (↑s).Pairwise (Commute on f)
⊢ exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯

Tactic:
induction' s using Finset.induction_on with a s ha ih

Result:
case empty
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
h : (↑∅).Pairwise (Commute on f)
⊢ exp 𝕂 (∑ i ∈ ∅, f i) = ∅.noncommProd (fun i => exp 𝕂 (f i)) ⋯

case insert
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_4
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ exp 𝕂 (∑ i ∈ insert a s, f i) = (insert a s).noncommProd (fun i => exp 𝕂 (f i)) ⋯