-- Module: Mathlib.RingTheory.Nilpotent.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
s : Finset ι
f : ι → R
hnp : ∀ i ∈ s, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)
empty :
  ∀ (hnp : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsNilpotent (f i))
    (h_comm :
      ∀ (i j : ι), Membership.mem (γ := Finset ι) ∅ i → Membership.mem (γ := Finset ι) ∅ j → Commute (f i) (f j)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ ∅, f i)
insert insert₁ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)),
    IsNilpotent.{u_1} (R := R) (∑ i ∈ Insert.insert j s, f i)
insert₂ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)),
    IsNilpotent (f j + ∑ x ∈ s, f x)
insert₃ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)),
    Commute (f j) (∑ x ∈ s, f x)
insert₄ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)), IsNilpotent (f j)
insert₅ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)),
    IsNilpotent.{u_1} (R := R) (∑ x ∈ s, f x)
insert₆ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)), IsNilpotent (f j)
insert₇ insert₈ :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s)
    (ih :
      ∀ (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)),
        IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i))
    (hnp : ∀ i ∈ Insert.insert j s, IsNilpotent (f i))
    (h_comm : ∀ (i j_1 : ι), i ∈ Insert.insert j s → j_1 ∈ Insert.insert j s → Commute (f i) (f j_1)),
    IsNilpotent.{u_1} (R := R) (∑ x ∈ s, f x)
⊢ IsNilpotent.{u_1} (R := R) (∑ i ∈ s, f i)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih => ?_
  rw [Finset.sum_insert hj]
  apply Commute.isNilpotent_add
  · exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
  · apply hnp; simp
  · exact ih (fun i hi ↦ hnp i (by simp [hi]))
      (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))

Premises used: Insert.insert, Commute.sum_right, Commute.isNilpotent_add