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
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
⊢ 1 ≤ m

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
r : 𝕜
hr : r ∈ s
hm2 : ¬m = 0
⊢ 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
r : 𝕜
hr : r ∈ s
hm2 : ¬m = 0
x_1 : ι
⊢ Eq.{u_3 + 1} (α := F) (iteratedDerivWithin m (fun (z : 𝕜) ↦ f x_1 z) s r)
    (iteratedDerivWithin m (fun (z : 𝕜) ↦ f x_1 z) s r)

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
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:
exact ((h m (by lia) (by lia)).summable hr).congr (fun _ ↦ by simp)

Premises used: SummableLocallyUniformlyOn.summable, Summable.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
x_1 : ι
x_2 : 𝕜
ht : x_2 ∈ s
rw 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)
⊢ 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)

Tactic:
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
⊢ 1 ≤ 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
⊢ m + 1 ≤ 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
⊢ 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:
exact SummableLocallyUniformlyOn_congr
        (fun _ _ ht ↦ by rw [iteratedDerivWithin_succ]) (h (m + 1) (by lia) (by lia))

Premises used: SummableLocallyUniformlyOn_congr, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
⊢ ∃ (g : β → α), HasProdUniformlyOn f g s

Tactic:
h

Premises used: Multipliable, UniformOnFun, HasProdUniformlyOn, MultipliableUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
h : HasProdUniformlyOn f g s
⊢ MultipliableUniformlyOn f s

Tactic:
⟨g, h⟩

Premises used: Multipliable, Exists.intro, MultipliableUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
⊢ HasProdUniformlyOn f g s ↔ TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
simpa [HasProdUniformlyOn, HasProd, ← UniformOnFun.ofFun_prod, Finset.prod_fn] using
    UniformOnFun.tendsto_iff_tendstoUniformlyOn (𝔖 := {s})

Premises used: UniformOnFun.tendsto_iff_tendstoUniformlyOn, HasProd, UniformOnFun.ofFun_prod, HasProdUniformlyOn, Finset.prod_fn, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
f' : ι → β → α
h : HasProdUniformlyOn f g s
hff' :
  ∀ᶠ (n : Finset ι) in atTop,
    Set.EqOn.{u_2, u_1} (β := α) (fun (x : β) ↦ ∏ i ∈ n, f i x) (fun (x : β) ↦ ∏ i ∈ n, f' i x) s
⊢ HasProdUniformlyOn f' g s

Tactic:
hasProdUniformlyOn_iff_tendstoUniformlyOn.mpr (h.tendstoUniformlyOn.congr hff')

Premises used: Iff.mpr, TendstoUniformlyOn.congr, hasProdUniformlyOn_iff_tendstoUniformlyOn, HasProdUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
g' : β → α
h : HasProdUniformlyOn f g s
hgg' : Set.EqOn g g' s
⊢ HasProdUniformlyOn f g' s

Tactic:
hasProdUniformlyOn_iff_tendstoUniformlyOn.mpr (h.tendstoUniformlyOn.congr_right hgg')

Premises used: Iff.mpr, TendstoUniformlyOn.congr_right, hasProdUniformlyOn_iff_tendstoUniformlyOn, HasProdUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
f : ℕ → β → α
h : HasProdUniformlyOn f g s
⊢ TendstoUniformlyOn (fun (x1 : ℕ) (x2 : β) ↦ ∏ i ∈ Finset.range x1, f i x2) g atTop s

Tactic:
(tendsto_finset_range.eventually <| h.tendstoUniformlyOn · ·)

Premises used: Set.Mem, TendstoUniformlyOn, Filter.tendsto_finset_range, Filter.Tendsto.eventually, HasProdUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
x : β
s : Set β
inst_1 : UniformSpace α
h : HasProdUniformlyOn f g s
hx : x ∈ s
⊢ HasProd (fun (x_1 : ι) ↦ f x_1 x) (g x)

Tactic:
h.tendstoUniformlyOn.tendsto_at hx

Premises used: iInf, HasProd, TendstoUniformlyOn.tendsto_at, Filter.atTop, HasProdUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : T2Space α
h : HasProdUniformlyOn f g s
⊢ Set.EqOn (fun (x : β) ↦ ∏' (b : ι), f b x) g s

Tactic:
fun _ hx ↦ (h.hasProd hx).tprod_eq

Premises used: Set.EqOn, HasProd.tprod_eq, HasProdUniformlyOn.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
x : β
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
hx : x ∈ s
⊢ Multipliable.{u_1, u_3} (α := α) fun (x_1 : ι) ↦ f x_1 x

Tactic:
(h.exists.choose_spec.hasProd hx).multipliable

Premises used: Exists.choose_spec, MultipliableUniformlyOn.exists, HasProd.multipliable, HasProdUniformlyOn.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
obtain : ∀ (g : β → α) (hg : HasProdUniformlyOn f g s), HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s
⊢ HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s

Tactic:
obtain ⟨g, hg⟩ := h.exists

Premises used: MultipliableUniformlyOn.exists
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
g : β → α
hg : HasProdUniformlyOn f g s
⊢ HasProdUniformlyOn f g s

Tactic:
have hp := hg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
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
⊢ HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s

Tactic:
rw [hasProdUniformlyOn_iff_tendstoUniformlyOn] at hg ⊢

Premises used: hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
g : β → α
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:
hg.congr_inseparable_right fun x hx =>
    tendsto_nhds_unique_inseparable (hp.hasProd hx) (hp.hasProd hx).multipliable.hasProd

Premises used: tendsto_nhds_unique_inseparable, Multipliable.hasProd, HasProd.multipliable, TendstoUniformlyOn.congr_inseparable_right, HasProdUniformlyOn.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformlyOn f s
g : β → α
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:
exact hg.congr_inseparable_right fun x hx =>
    tendsto_nhds_unique_inseparable (hp.hasProd hx) (hp.hasProd hx).multipliable.hasProd

Premises used: tendsto_nhds_unique_inseparable, Multipliable.hasProd, HasProd.multipliable, TendstoUniformlyOn.congr_inseparable_right, HasProdUniformlyOn.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
⊢ MultipliableUniformlyOn f s ↔ HasProdUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s

Tactic:
⟨MultipliableUniformlyOn.hasProdUniformlyOn, HasProdUniformlyOn.multipliableUniformlyOn⟩

Premises used: MultipliableUniformlyOn.hasProdUniformlyOn, Iff.intro, HasProdUniformlyOn.multipliableUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
t : Set β
h : HasProdUniformlyOn f g t
hst : s ⊆ t
⊢ HasProdUniformlyOn f g s

Tactic:
hasProdUniformlyOn_iff_tendstoUniformlyOn.mpr <| h.tendstoUniformlyOn.mono hst

Premises used: Iff.mpr, TendstoUniformlyOn.mono, hasProdUniformlyOn_iff_tendstoUniformlyOn, HasProdUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
t : Set β
h : MultipliableUniformlyOn f t
hst : s ⊆ t
⊢ MultipliableUniformlyOn f s

Tactic:
(h.exists.choose_spec.mono hst).multipliableUniformlyOn

Premises used: Exists.choose_spec, MultipliableUniformlyOn.exists, HasProdUniformlyOn.mono, HasProdUniformlyOn.multipliableUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
⊢ HasProdLocallyUniformlyOn f g s ↔
    TendstoLocallyUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
Iff.rfl

Premises used: Iff.rfl, HasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop t

Tactic:
simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h

Premises used: hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
rwa₁ rwa₂ rwa₃ rwa₄ : TendstoLocallyUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ HasProdUniformlyOn f g s

Tactic:
rwa [hasProdUniformlyOn_iff_tendstoUniformlyOn,
    ← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hs]

Premises used: tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact, hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
obtain : ∀ (K : Set β) (hK3 : K ⊆ s) (hK1 : K ∈ 𝓝 x) (hK2 : IsCompact K), ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t
⊢ ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp hx

Premises used: Filter.HasBasis.mem_iff, compact_basis_nhds, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
K : Set β
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t

Tactic:
⟨K, nhdsWithin_le_nhds hK1,
    HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact (h.mono hK3) hK2⟩

Premises used: nhdsWithin_le_nhds, And.intro, TendstoLocallyUniformlyOn.mono, Exists.intro, HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
K : Set β
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g t

Tactic:
exact ⟨K, nhdsWithin_le_nhds hK1,
    HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact (h.mono hK3) hK2⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
⊢ TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn, HasProdLocallyUniformlyOn] at *

Premises used: HasProdLocallyUniformlyOn, hasProdUniformlyOn_iff_tendstoUniformlyOn