-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
m : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
h :
  ∀ (k : ℕ),
    1 ≤ k →
      k ≤ m →
        SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F)
          (fun (n : ι) ↦ iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) s
hf2 :
  ∀ (n : ι) (k : ℕ) (r : 𝕜),
    k ≤ m → r ∈ s → DifferentiableAt.{u_2, u_2, u_3} 𝕜 (F := F) (iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) r
zero :
  ∀ {x : 𝕜} (hx : x ∈ s)
    (h :
      ∀ (k : ℕ),
        1 ≤ k →
          k ≤ 0 →
            SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F)
              (fun (n : ι) ↦ iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) s)
    (hf2 :
      ∀ (n : ι) (k : ℕ) (r : 𝕜),
        k ≤ 0 → r ∈ s → DifferentiableAt.{u_2, u_2, u_3} 𝕜 (F := F) (iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) r),
    Eq.{u_3 + 1} (α := F) (iteratedDerivWithin 0 (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
      (∑' (n : ι), iteratedDerivWithin 0 (f n) s x)
⊢ Eq.{u_3 + 1} (α := F) (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
    (∑' (n : ι), iteratedDerivWithin m (f n) s x)
have succ : ∀ (m : ℕ)
  (hm :
    ∀ {x : 𝕜} (hx : x ∈ s)
      (h :
        ∀ (k : ℕ),
          1 ≤ k →
            k ≤ m →
              SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F)
                (fun (n : ι) ↦ iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) s)
      (hf2 :
        ∀ (n : ι) (k : ℕ) (r : 𝕜),
          k ≤ m →
            r ∈ s → DifferentiableAt.{u_2, u_2, u_3} 𝕜 (F := F) (iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) r),
      Eq.{u_3 + 1} (α := F) (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
        (∑' (n : ι), iteratedDerivWithin m (f n) s x))
  {x : 𝕜} (hx : x ∈ s)
  (h :
    ∀ (k : ℕ),
      1 ≤ k →
        k ≤ m + 1 →
          SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F)
            (fun (n : ι) ↦ iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) s)
  (hf2 :
    ∀ (n : ι) (k : ℕ) (r : 𝕜),
      k ≤ m + 1 →
        r ∈ s → DifferentiableAt.{u_2, u_2, u_3} 𝕜 (F := F) (iteratedDerivWithin k (fun (z : 𝕜) ↦ f n z) s) r),
  Eq.{u_3 + 1} (α := F) (iteratedDerivWithin (m + 1) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
    (∑' (n : ι), iteratedDerivWithin (m + 1) (f n) s x)
Tactic: induction m generalizing x with
  | zero => simp
  | succ m hm =>
    simp_rw [iteratedDerivWithin_succ]
    rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by lia) hr)]
    · exact derivWithin_congr (fun t ht ↦ hm ht (fun k hk1 hkm ↦ h k hk1 (by lia))
          (fun k r e hr he ↦ hf2 k r e (by lia) he)) (hm hx (fun k hk1 hkm ↦ h k hk1 (by lia))
          (fun k r e hr he ↦ hf2 k r e (by lia) he))
    · intro r hr
      by_cases hm2 : m = 0
      · simp [hm2, hsum r hr]
      · exact ((h m (by lia) (by lia)).summable hr).congr (fun _ ↦ by simp)
    · exact SummableLocallyUniformlyOn_congr
        (fun _ _ ht ↦ by rw [iteratedDerivWithin_succ]) (h (m + 1) (by lia) (by lia))
Cleared hypotheses: m, x, hx, h, hf2