awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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
have apply : EqOn g (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) s
Tactic: apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right
-- 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
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
⊢ ∀ᶠ (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
have 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
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))
-- 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
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
⊢ ∀ᶠ (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
have h₂ : ∀ (a : Finset ι),
  ∀ x ∈ s,
    HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ a, f b y) (∑ i ∈ a, derivWithin (fun (z : 𝕜) ↦ f i z) s 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))
-- 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
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) (iteratedDerivWithin (m + 1) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
    (∑' (n : ι), iteratedDerivWithin (m + 1) (f n) s x)
have 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)
Tactic: simp_rw [iteratedDerivWithin_succ]
-- 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
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)
    (∑' (n : ι), derivWithin (iteratedDerivWithin m (f n) s) s x)
have 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)
Tactic: rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by lia) hr)]
-- 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
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)
⊢ 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)
have rw : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s y
Tactic: rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by lia) hr)]
-- 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
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
⊢ 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)
have 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
Tactic: rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by lia) hr)]
-- 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
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
⊢ Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r
have pos : ∀ (hm2 : m = 0), Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r
Tactic: by_cases hm2 : m = 0
-- 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
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
⊢ Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r
have neg : ∀ (hm2 : ¬m = 0), Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f n z) s r
Tactic: by_cases hm2 : m = 0
-- 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
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
x_1 : ι
x_2 : 𝕜
ht : x_2 ∈ s
⊢ Eq.{u_3 + 1} (α := F) (iteratedDerivWithin (m + 1) (fun (z : 𝕜) ↦ f x_1 z) s x_2)
    (derivWithin (fun (z : 𝕜) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f x_1 z) s z) s x_2)
have rw : Eq.{u_3 + 1} (α := F) (derivWithin (iteratedDerivWithin m (fun (z : 𝕜) ↦ f x_1 z) s) s x_2)
  (derivWithin (fun (z : 𝕜) ↦ iteratedDerivWithin m (fun (z : 𝕜) ↦ f x_1 z) s z) s x_2)
Tactic: rw [iteratedDerivWithin_succ]
-- 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
⊢ Eq.{u_3 + 1} (α := F) (iteratedDerivWithin m (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x)
    (∑' (n : ι), iteratedDerivWithin m (f n) s x)
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
⊢ HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s
have obtain : ∀ (g : β → α) (hg : HasProdUniformlyOn f g s), HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s
Tactic: obtain ⟨g, hg⟩ := h.exists
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
g : β → α
hg hp : HasProdUniformlyOn f g s
⊢ HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s
have rw : ∀ (hg : TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s) (hp : HasProdUniformlyOn f g s),
  TendstoUniformlyOn.{u_2, u_1, u_3} (β := α) (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2)
    (fun (x : β) ↦ ∏' (i : ι), f i x) atTop s
Tactic: rw [hasProdUniformlyOn_iff_tendstoUniformlyOn] at hg ⊢
Cleared hypotheses: hg, hp
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformlyOn f g s
hs : IsCompact s
⊢ HasProdUniformlyOn f g s
have rwa : TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
Tactic: rwa [hasProdUniformlyOn_iff_tendstoUniformlyOn,
    ← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformlyOn f g s
hs : IsCompact s
rwa : TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ HasProdUniformlyOn f g s
have rwa₁ : TendstoLocallyUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
Tactic: rwa [hasProdUniformlyOn_iff_tendstoUniformlyOn,
    ← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
x : β
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
h : HasProdLocallyUniformlyOn f g s
hx : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t
have obtain : ∀ (K : Set β) (hK3 : K ⊆ s) (hK1 : K ∈ 𝓝 x) (hK2 : IsCompact K), ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t
Tactic: obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdUniformlyOn f g s
⊢ HasProdLocallyUniformlyOn f g s
have h₁ : TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
Tactic: simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn, HasProdLocallyUniformlyOn] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
hs : IsOpen[inst_2] s
inst_3 : LocallyCompactSpace β
h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g K
⊢ HasProdLocallyUniformlyOn f g s
have rw : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop K
Tactic: rw [HasProdLocallyUniformlyOn, tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
h2 : MultipliableLocallyUniformlyOn f s
⊢ MultipliableLocallyUniformlyOn f' s
have h₁ : HasProdLocallyUniformlyOn f' (fun (x : β) ↦ ∏' (i : ι), f i x) s
Tactic: apply HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
h2 : MultipliableLocallyUniformlyOn f s
h₁ : HasProdLocallyUniformlyOn f' (fun (x : β) ↦ ∏' (i : ι), f i x) s
⊢ MultipliableLocallyUniformlyOn f' s
have g : β → α
Tactic: apply HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : HasProdLocallyUniformlyOn f g s
⊢ TendstoLocallyUniformlyOn (fun (N : ℕ) (b : β) ↦ ∏ i ∈ Finset.range N, f i b) g atTop s
have h₁ : TendstoLocallyUniformlyOn (fun (x1 : Finset ℕ) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
Tactic: rw [hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn] at h
Cleared hypotheses: h