-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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)
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)
⊢ Eq.{u_3 + 1} (α := F) (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
    (∑' (n : ι), iteratedDerivWithin m (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))

Premises used: SummableLocallyUniformlyOn_congr, HAdd.hAdd, iteratedDerivWithin_succ, derivWithin_tsum, OfNat.ofNat