awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
t : Finset (↑univ : Type u_1)
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : ↥t), ∀ y ∈ U (↑(↑i_1 : (↑univ : Type u_1)) : α), (f y, F i y) ∈ V
x : α
ht :
  ∃ (x_1 : α),
    (∃ (x : Membership.mem (γ := Set α) univ x_1),
        Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) x_1 ⋯ ∈ t) ∧
      x ∈ U x_1
⊢ (f x, F i x) ∈ V
have obtain : ∀ (y : α) (hy₃ : x ∈ U y) (hy₁ : Membership.mem (γ := Set α) univ y)
  (hy₂ : Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) y sorry ∈ t), (f x, F i x) ∈ V
Tactic: obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
have this : CompactSpace.{u_1} (↑s : Type u_1)
Tactic: haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace.{u_1} (↑s : Type u_1)
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
have refine : ∀ (h : TendstoLocallyUniformlyOn F f p s), TendstoUniformlyOn F f p s
Tactic: refine ⟨fun h => ?_, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace.{u_1} (↑s : Type u_1)
h : TendstoLocallyUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
have rwa : ∀
  (h :
    TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p),
  TendstoUniformlyOn F f p s
Tactic: rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
    tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace.{u_1} (↑s : Type u_1)
h : TendstoLocallyUniformlyOn F f p s
rwa :
  ∀
    (h :
      TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α))
        (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p),
    TendstoUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
have rwa₁ : ∀
  (h :
    TendstoUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p),
  TendstoUniformlyOn F f p s
Tactic: rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
    tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace.{u_1} (↑s : Type u_1)
h : TendstoLocallyUniformlyOn F f p s
rwa :
  ∀
    (h :
      TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α))
        (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p),
    TendstoUniformlyOn F f p s
rwa₁ :
  ∀
    (h :
      TendstoUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
        p),
    TendstoUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
have rwa₂ : ∀ (h : TendstoUniformlyOn F f p s), TendstoUniformlyOn F f p s
Tactic: rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
    tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun (n : ι) ↦ F n ∘ g) n y) ∈ u
have rcases : ∀ (a : Set α) (ha : a ∈ 𝓝[s] g x) (H : ∀ᶠ (n : ι) in p, ∀ y ∈ a, (f y, F n y) ∈ u),
  ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun (n : ι) ↦ F n ∘ g) n y) ∈ u
Tactic: rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ a, (f y, F n y) ∈ u
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun (n : ι) ↦ F n ∘ g) n y) ∈ u
have this : g ⁻¹' a ∈ 𝓝[t] x
Tactic: have : g ⁻¹' a ∈ 𝓝[t] x :=
    (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous[inst_2, inst] g
⊢ TendstoLocallyUniformly (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p
have rw : ∀ (h : TendstoLocallyUniformlyOn F f p univ) (g : γ → α) (cg : Continuous[inst_2, inst] g),
  TendstoLocallyUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p univ
Tactic: rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
Cleared hypotheses: h, g, cg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous[inst_2, inst] g
⊢ TendstoLocallyUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p univ
have cg₁ : ContinuousOn g univ
Tactic: rw [← continuousOn_univ] at cg
Cleared hypotheses: cg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p s
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
⊢ TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p s
have rw : ∀ (hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)) (hfs : MapsTo f s t)
  (hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t),
  ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ ((g ∘ f) y.2, (g ∘ F y.1) y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
Cleared hypotheses: hf, hfs, hFs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ ((g ∘ f) y.2, (g ∘ F y.1) y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
have refine : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (a : ι × α) in p ×ˢ 𝓝[s] x, (f a.2, F a.1 a.2) ∈ t ×ˢ t
Tactic: refine fun x hx ↦ Tendsto.comp hg (tendsto_inf.mpr ⟨hf x hx, tendsto_principal.mpr ?_⟩)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
x : α
hx : x ∈ s
⊢ ∀ᶠ (a : ι × α) in p ×ˢ 𝓝[s] x, (f a.2, F a.1 a.2) ∈ t ×ˢ t
have h : ∀ (a : ι × α),
  Membership.mem (γ := Set (ι × α))
    {x : ι × α |
      Membership.mem (γ := Set (ι × α)) {x : ι × α | (fun (p : ι × α) ↦ MapsTo (F p.1) s t ∧ p.2 ∈ s) x} x →
        Membership.mem (γ := Set (ι × α)) {x : ι × α | (fun (a : ι × α) ↦ (f a.2, F a.1 a.2) ∈ t ×ˢ t) x} x}
    a
Tactic: filter_upwards [hFs.prod_mk eventually_mem_nhdsWithin] with y hy using ⟨hfs hy.2, hy.1 hy.2⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
x : α
hx : x ∈ s
h :
  ∀ (a : ι × α),
    Membership.mem (γ := Set (ι × α))
      {x : ι × α |
        Membership.mem (γ := Set (ι × α)) {x : ι × α | (fun (p : ι × α) ↦ MapsTo (F p.1) s t ∧ p.2 ∈ s) x} x →
          Membership.mem (γ := Set (ι × α)) {x : ι × α | (fun (a : ι × α) ↦ (f a.2, F a.1 a.2) ∈ t ×ˢ t) x} x}
      a
⊢ ∀ᶠ (a : ι × α) in p ×ˢ 𝓝[s] x, (f a.2, F a.1 a.2) ∈ t ×ˢ t
have h₁ : ∀ (a : ι × α), MapsTo (F a.1) s t ∧ a.2 ∈ s → (f a.2, F a.1 a.2) ∈ t ×ˢ t
Tactic: filter_upwards [hFs.prod_mk eventually_mem_nhdsWithin] with y hy using ⟨hfs hy.2, hy.1 hy.2⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformly F f p
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformly (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p
have rw : ∀ (hf : TendstoLocallyUniformlyOn F f p univ) (hfs : ∀ (x : α), f x ∈ t) (hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t),
  TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p univ
Tactic: rw [← tendstoLocallyUniformlyOn_univ] at *
Cleared hypotheses: hf, hfs, hFs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p univ
have hfs₁ : MapsTo f univ t
Tactic: apply hg.comp_tendstoLocallyUniformlyOn hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
hfs₁ : MapsTo f univ t
⊢ TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p univ
have hFs₁ : ∀ᶠ (n : ι) in p, MapsTo (F n) univ t
Tactic: apply hg.comp_tendstoLocallyUniformlyOn hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p s
hG : TendstoLocallyUniformlyOn G g p s
⊢ TendstoLocallyUniformlyOn (β := β × γ) (fun (n : ι) (x : α) ↦ (F n x, G n x)) (fun (x : α) ↦ (f x, g x)) p s
have rw : ∀ (hF : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β))
  (hG : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)),
  ∀ x ∈ s,
    Tendsto (β := (β × γ) × β × γ) (fun (y : ι × α) ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *
Cleared hypotheses: hF, hG
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto (β := (β × γ) × β × γ) (fun (y : ι × α) ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))
have rw : Tendsto
  ((fun (p : (β × γ) × β × γ) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun (y : ι × α) ↦
    ((f y.2, g y.2), F y.1 y.2, G y.1 y.2))
  (p ×ˢ 𝓝[s] x) (𝓤 β ×ˢ 𝓤 γ)
Tactic: rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformly F f p
hG : TendstoLocallyUniformly G g p
⊢ TendstoLocallyUniformly (β := β × γ) (fun (n : ι) (x : α) ↦ (F n x, G n x)) (fun (x : α) ↦ (f x, g x)) p
have rw : ∀ (hF : TendstoLocallyUniformlyOn F f p univ) (hG : TendstoLocallyUniformlyOn G g p univ),
  TendstoLocallyUniformlyOn (β := β × γ) (fun (n : ι) (x : α) ↦ (F n x, G n x)) (fun (x : α) ↦ (f x, g x)) p univ
Tactic: rw [← tendstoLocallyUniformlyOn_univ] at *
Cleared hypotheses: hF, hG
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
⊢ TendstoLocallyUniformlyOn F f p s
have refine : ∀ (x : α) (hx : x ∈ s), Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Tactic: refine tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
have obtain : ∀ (t : Set α) (ht : t ∈ 𝓝[s] x) (htr : TendstoUniformlyOn F f p t),
  Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Tactic: obtain ⟨t, ht, htr⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
htr : TendstoUniformlyOn F f p t
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
have htr₁ : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 t) (𝓤 β)
Tactic: rw [tendstoUniformlyOn_iff_tendsto] at htr
Cleared hypotheses: htr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst] s
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE
have tfae_1_to_2 : ∀ (a : TendstoLocallyUniformlyOn G g p s), ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
Tactic: tfae_have 1 → 2
  | h, K, hK1, hK2 =>
    (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst] s
tfae_1_to_2 : ∀ (a : TendstoLocallyUniformlyOn G g p s), ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
h : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
have obtain : ∀ (K : Set α) (hK3 : K ⊆ s) (hK1 : K ∈ 𝓝 x) (hK2 : IsCompact K), ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
Tactic: obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst] s
tfae_1_to_2 : ∀ (a : TendstoLocallyUniformlyOn G g p s), ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE
have tfae_2_to_3 : ∀ (a : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K), ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
Tactic: tfae_have 2 → 3
  | h, x, hx => by
    obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
    exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst] s
tfae_1_to_2 : ∀ (a : TendstoLocallyUniformlyOn G g p s), ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  ∀ (a : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K), ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
h : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u
have obtain : ∀ (v : Set α) (hv1 : v ∈ 𝓝[s] x) (hv2 : TendstoUniformlyOn G g p v),
  ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u
Tactic: obtain ⟨v, hv1, hv2⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst] s
tfae_1_to_2 : ∀ (a : TendstoLocallyUniformlyOn G g p s), ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  ∀ (a : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K), ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE
have tfae_3_to_1 : ∀ (a : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v), TendstoLocallyUniformlyOn G g p s
Tactic: tfae_have 3 → 1
  | h, u, hu, x, hx => by
    obtain ⟨v, hv1, hv2⟩ := h x hx
    exact ⟨v, hv1, hv2 u hu⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)
have simp : TendstoLocallyUniformlyOn F f p s ↔
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
Tactic: simp only [TendstoUniformlyOnFilter, eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
have mp : TendstoLocallyUniformlyOn F f p s →
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
mp :
  TendstoLocallyUniformlyOn F f p s →
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
have mpr : (∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
  TendstoLocallyUniformlyOn F f p s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ (pa : ι → Prop),
    (∀ᶠ (x : ι) in p, pa x) ∧
      ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
have mp : ∀ (s_1 : Set α) (hs1 : s_1 ∈ 𝓝[s] x) (hs2 : ∀ᶠ (n : ι) in p, ∀ y ∈ s_1, (f y, F n y) ∈ u),
  ∃ (pa : ι → Prop),
    (∀ᶠ (x : ι) in p, pa x) ∧
      ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
Tactic: obtain ⟨s, hs1, hs2⟩ := h u hu x hx