awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
apply :
  TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
    (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
    (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
apply₁ :
  ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ x ∈ s,
      HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ n, (fun (n : ι) ↦ f n y) b)
        ((fun (n : Finset ι) (a : 𝕜) ↦ (∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a : F)) n x) x
⊢ HasDerivAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) x

Tactic:
apply hasDerivAt_of_tendstoLocallyUniformlyOn hs _ _ (fun y hy ↦ (hf y hy).hasSum) hx
    (f' := fun n : Finset ι ↦ fun a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)

Premises used: hasDerivAt_of_tendstoLocallyUniformlyOn, Summable.hasSum
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
obtain :
  ∀ (g : 𝕜 → F) (hg : HasSumLocallyUniformlyOn (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) g s),
    TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
      (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
      (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
⊢ TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
    (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
    (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s

Tactic:
obtain ⟨g, hg⟩ := h
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
g : 𝕜 → F
hg : HasSumLocallyUniformlyOn (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) g s
apply : EqOn g (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) s
⊢ TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
    (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
    (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s

Tactic:
apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right

Premises used: hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn, Iff.mp, TendstoLocallyUniformlyOn.congr_right
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
g : 𝕜 → F
hg : HasSumLocallyUniformlyOn (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) g s
⊢ EqOn g (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) s

Tactic:
fun _ hb ↦ (hg.tsum_eqOn hb).symm

Premises used: Set.EqOn, HasSumLocallyUniformlyOn.tsum_eqOn, Eq.symm
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
g : 𝕜 → F
hg : HasSumLocallyUniformlyOn (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) g s
⊢ EqOn g (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) s

Tactic:
exact fun _ hb ↦ (hg.tsum_eqOn hb).symm

Premises used: HasSumLocallyUniformlyOn.tsum_eqOn, Eq.symm
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
t : Finset ι
r : 𝕜
hr : r ∈ s
⊢ HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ t, f b y) (∑ i ∈ t, derivWithin (fun (z : 𝕜) ↦ f i z) s r) r

Tactic:
HasDerivAt.fun_sum
      (fun q hq ↦ ((hf2 q r hr).differentiableWithinAt.hasDerivWithinAt.hasDerivAt)
      (hs.mem_nhds hr))

Premises used: DifferentiableAt.differentiableWithinAt, DifferentiableWithinAt.hasDerivWithinAt, HasDerivAt.fun_sum, IsOpen.mem_nhds, HasDerivWithinAt.hasDerivAt
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
h₁ :
  ∀ (a : Finset ι),
    Membership.mem (γ := Set (Finset ι))
      {x : Finset ι |
        (fun (n : Finset ι) ↦
            ∀ x ∈ s,
              HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ n, (fun (n : ι) ↦ f n y) b)
                ((fun (n : Finset ι) (a : 𝕜) ↦ (∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a : F)) n x) x)
          x}
      a
h₂ h₃ :
  ∀ (t : Finset ι) (r : 𝕜) (hr : r ∈ s),
    HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ t, f b y) (∑ i ∈ t, derivWithin (fun (z : 𝕜) ↦ f i z) s r) r
⊢ ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ x ∈ s,
      HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ n, (fun (n : ι) ↦ f n y) b)
        ((fun (n : Finset ι) (a : 𝕜) ↦ (∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a : F)) n x) x

Tactic:
filter_upwards with t r hr using HasDerivAt.fun_sum
      (fun q hq ↦ ((hf2 q r hr).differentiableWithinAt.hasDerivWithinAt.hasDerivAt)
      (hs.mem_nhds hr))
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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)

Tactic:
simp
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
succ :
  Eq.{u_3 + 1} (α := F) (derivWithin (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s) s x)
    (∑' (n : ι), derivWithin (iteratedDerivWithin m (f n) s) s x)
⊢ 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:
simp_rw [iteratedDerivWithin_succ]

Premises used: iteratedDerivWithin_succ
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
n : ι
r : 𝕜
hr : r ∈ s
⊢ m ≤ m + 1

Tactic:
lia
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
succ :
  Eq.{u_3 + 1} (α := F) (derivWithin (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s) s x)
    (derivWithin (fun (z : 𝕜) ↦ ∑' (n : ι), iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s z) s x)
rw : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s y
rw₁ :
  SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F)
    (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s z) s) s
⊢ Eq.{u_3 + 1} (α := F) (derivWithin (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s) s x)
    (∑' (n : ι), derivWithin (iteratedDerivWithin m (f n) s) s x)

Tactic:
rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by lia) hr)]

Premises used: derivWithin_tsum
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
t : 𝕜
ht : t ∈ s
k : ℕ
hk1 : 1 ≤ k
hkm : k ≤ m
⊢ k ≤ m + 1

Tactic:
lia
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
t : 𝕜
ht : t ∈ s
k : ι
r : ℕ
e : 𝕜
hr : r ≤ m
he : e ∈ s
⊢ r ≤ m + 1

Tactic:
lia
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
k : ℕ
hk1 : 1 ≤ k
hkm : k ≤ m
⊢ k ≤ m + 1

Tactic:
lia
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
k : ι
r : ℕ
e : 𝕜
hr : r ≤ m
he : e ∈ s
⊢ r ≤ m + 1

Tactic:
lia
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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) (derivWithin (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s) s x)
    (derivWithin (fun (z : 𝕜) ↦ ∑' (n : ι), iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s z) s x)

Tactic:
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))

Premises used: derivWithin_congr
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
r : 𝕜
hr : r ∈ s
pos : ∀ (hm2 : m = 0), Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r
neg : ∀ (hm2 : ¬m = 0), Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r
⊢ Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r

Tactic:
by_cases hm2 : m = 0
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n t
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
r : 𝕜
hr : r ∈ s
hm2 : m = 0
⊢ Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r

Tactic:
simp [hm2, hsum r hr]