awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst] s
hs₂ : IsOpen[inst] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → IsOpen[inst] s_1

Tactic:
simp [*]
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst] s
hs₂ : IsOpen[inst] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → TendstoLocallyUniformlyOn F f p s_1

Tactic:
simp [*]
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformly F f p
⊢ TendstoLocallyUniformlyOn F f p s

Tactic:
(tendstoLocallyUniformlyOn_univ.mpr h).mono (subset_univ _)

Premises used: Iff.mpr, Set.subset_univ, TendstoLocallyUniformlyOn.mono, tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Tactic:
⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩

Premises used: TendstoUniformly.tendstoLocallyUniformly, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
refine :
  ∀ (h : TendstoLocallyUniformly F f p) (V : Set (β × β)) (hV : V ∈ 𝓤 β), ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Tactic:
refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 ∈ 𝓤 β
choose :
  ∀ (U : (x : α) → Set α) (hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V),
    ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
choose U hU using h V hV
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
obtain :
  ∀ (t : Finset (↑univ : Type u_1)) (ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))),
    ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1

Premises used: IsCompact.elim_nhds_subcover', isCompact_univ, And.left
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
t : Finset (↑univ : Type u_1)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
⊢ ∀ (x : ↥t), ∀ᶠ (n : ι) in p, ∀ y ∈ U (↑(↑x : (↑univ : Type u_1)) : α), (f y, F n y) ∈ V

Tactic:
replace hU := fun x : t => (hU x).2
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
hU : ∀ (x : ↥t), ∀ᶠ (n : ι) in p, ∀ y ∈ U (↑(↑x : (↑univ : Type u_1)) : α), (f y, F n y) ∈ V
⊢ ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V

Tactic:
rw [← eventually_all] at hU

Premises used: Filter.eventually_all
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
hU.mono fun i hi x => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
refine :
  ∀ (i : ι) (hi : ∀ (i_1 : ↥t), ∀ y ∈ U (↑(↑i_1 : (↑univ : Type u_1)) : α), (f y, F i y) ∈ V) (x : α), (f x, F i x) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
refine hU.mono fun i hi x => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
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 : α
⊢ Membership.mem (γ := Set α) (⋃ x ∈ t, U (↑x : α)) x

Tactic:
specialize ht (mem_univ x)

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 : Membership.mem (γ := Set α) (⋃ x ∈ t, U (↑x : α)) x
⊢ ∃ (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

Tactic:
simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht

Premises used: Set.mem_iUnion, SetCoe.exists, exists_and_right, exists_prop
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
obtain :
  ∀ (y : α) (hy₃ : x ∈ U y) (hy₁ : Membership.mem (γ := Set α) univ y)
    (hy₂ : Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) y ⋯ ∈ t), (f x, F i x) ∈ V
⊢ (f x, F i x) ∈ V

Tactic:
obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 y : α
hy₃ : x ∈ U y
hy₁ : Membership.mem (γ := Set α) univ y
hy₂ : Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) y ⋯ ∈ t
⊢ (f x, F i x) ∈ V

Tactic:
hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

Premises used: Subtype.mk
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 y : α
hy₃ : x ∈ U y
hy₁ : Membership.mem (γ := Set α) univ y
hy₂ : Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) y ⋯ ∈ t
⊢ (f x, F i x) ∈ V

Tactic:
exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

Premises used: Subtype.mk
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
⊢ CompactSpace.{u_1} (↑s : Type u_1)

Tactic:
haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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

Tactic:
⟨fun h => ?_, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩

Premises used: Iff.intro, TendstoUniformlyOn.tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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)
refine : ∀ (h : TendstoLocallyUniformlyOn F f p s), TendstoUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

Tactic:
refine ⟨fun h => ?_, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : TendstoUniformlyOn F f p s), 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

Premises used: tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
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
⊢ ∃ 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⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ g ⁻¹' a ∈ 𝓝[t] x

Tactic:
have : g ⁻¹' a ∈ 𝓝[t] x :=
    (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun (n : ι) ↦ F n ∘ g) n y) ∈ u

Tactic:
⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩

Premises used: Filter.Eventually.mono, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun (n : ι) ↦ F n ∘ g) n y) ∈ u

Tactic:
exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
rw :
  ∀ (h : TendstoLocallyUniformlyOn F f p univ) (g : γ → α) (cg : Continuous[inst_2, inst] g),
    TendstoLocallyUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p univ
⊢ TendstoLocallyUniformly (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at h ⊢

Premises used: tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ContinuousOn g univ

Tactic:
rw [← continuousOn_univ] at cg

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p univ

Tactic:
h.comp _ (mapsTo_univ _ _) cg

Premises used: Set.mapsTo_univ, TendstoLocallyUniformlyOn.comp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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 : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p univ

Tactic:
exact h.comp _ (mapsTo_univ _ _) cg

Premises used: Set.mapsTo_univ, TendstoLocallyUniformlyOn.comp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
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) (𝓤 γ)
⊢ TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢

Premises used: tendstoLocallyUniformlyOn_iff_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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) (𝓤 γ)

Tactic:
fun x hx ↦ Tendsto.comp hg (tendsto_inf.mpr ⟨hf x hx, tendsto_principal.mpr ?_⟩)

Premises used: Iff.mpr, Filter.tendsto_inf, Filter.tendsto_principal, And.intro, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
refine : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (a : ι × α) in p ×ˢ 𝓝[s] x, (f a.2, F a.1 a.2) ∈ t ×ˢ t
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ ((g ∘ f) y.2, (g ∘ F y.1) y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)

Tactic:
refine fun x hx ↦ Tendsto.comp hg (tendsto_inf.mpr ⟨hf x hx, tendsto_principal.mpr ?_⟩)

Premises used: Iff.mpr, Filter.tendsto_inf, Filter.tendsto_principal, And.intro, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
y : ι × α
hy : MapsTo (F y.1) s t ∧ y.2 ∈ s
⊢ (f y.2, F y.1 y.2) ∈ t ×ˢ t

Tactic:
⟨hfs hy.2, hy.1 hy.2⟩

Premises used: Set.Mem, setOf, Set.prod, And.right, And.left, And.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
h₁ h₂ : ∀ (y : ι × α) (hy : MapsTo (F y.1) s t ∧ y.2 ∈ s), (f y.2, F y.1 y.2) ∈ t ×ˢ t
⊢ ∀ᶠ (a : ι × α) in p ×ˢ 𝓝[s] x, (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⟩

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.prod_mk
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
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
⊢ TendstoLocallyUniformly (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at *

Premises used: tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
hFs₁ : ∀ᶠ (n : ι) in p, MapsTo (F n) univ t
⊢ TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p univ

Tactic:
apply hg.comp_tendstoLocallyUniformlyOn hf

Premises used: UniformContinuousOn.comp_tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ MapsTo f univ t

Tactic:
simpa [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ᶠ (n : ι) in p, MapsTo (F n) univ t

Tactic:
simpa [MapsTo]

Premises used: Set.MapsTo