awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : β → γ
hg : UniformContinuous g
hf : TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn (fun (x : ι) ↦ g ∘ F x) (g ∘ f) p s

Tactic:
hg.uniformContinuousOn.comp_tendstoLocallyUniformlyOn hf (mapsTo_univ _ _) <| .of_forall fun _ ↦
    mapsTo_univ _ _

Premises used: Set.mapsTo_univ, Filter.Eventually.of_forall, UniformContinuousOn.comp_tendstoLocallyUniformlyOn, UniformContinuous.uniformContinuousOn
-- 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 : β → γ
hg : UniformContinuous g
hf : TendstoLocallyUniformly F f p
⊢ ∀ (x : α), Membership.mem (γ := Set β) univ (f x)

Tactic:
simp
-- 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 : β → γ
hg : UniformContinuous g
hf : TendstoLocallyUniformly F f p
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), Membership.mem (γ := Set β) univ (F n x)

Tactic:
simp
-- 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 : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p s
hG : TendstoLocallyUniformlyOn G g p s
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)
        (𝓤 (β × γ))
⊢ TendstoLocallyUniformlyOn (β := β × γ) (fun (n : ι) (x : α) ↦ (F n x, G n x)) (fun (x : α) ↦ (f x, g x)) p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *

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 : ι → α → γ
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
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) (𝓤 β ×ˢ 𝓤 γ)
⊢ Tendsto (β := (β × γ) × β × γ) (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]

Premises used: Filter.tendsto_comap_iff, uniformity_prod_eq_comap_prod
-- 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 : ι → α → γ
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 (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:
(hF x hx).prodMk (hG x hx)

Premises used: Filter.Tendsto.prodMk
-- 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 : ι → α → γ
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 (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:
exact (hF x hx).prodMk (hG x hx)

Premises used: Filter.Tendsto.prodMk
-- 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 : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p s
hG : TendstoLocallyUniformlyOn G g p s
⊢ TendstoLocallyUniformlyOn (fun (n : ι) ↦ Function.prod (α := fun (a : α) ↦ β) (β := fun (a : α) ↦ γ) (F n) (G n))
    (Function.prod (α := fun (a : α) ↦ β) (β := fun (a : α) ↦ γ) f g) p s

Tactic:
hF.prodMk hG

Premises used: Function.prod, TendstoLocallyUniformlyOn.prodMk
-- 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 : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformly F f p
hG : TendstoLocallyUniformly G g p
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
⊢ TendstoLocallyUniformly (β := β × γ) (fun (n : ι) (x : α) ↦ (F n x, G n x)) (fun (x : α) ↦ (f x, g x)) 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 : ι → α → γ
g : α → γ
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:
hF.prodMk hG

Premises used: TendstoLocallyUniformlyOn.prodMk
-- 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 : ι → α → γ
g : α → γ
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:
exact hF.prodMk hG

Premises used: TendstoLocallyUniformlyOn.prodMk
-- 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 : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformly F f p
hG : TendstoLocallyUniformly G g p
⊢ TendstoLocallyUniformly (fun (n : ι) ↦ Function.prod (α := fun (a : α) ↦ β) (β := fun (a : α) ↦ γ) (F n) (G n))
    (Function.prod (α := fun (a : α) ↦ β) (β := fun (a : α) ↦ γ) f g) p

Tactic:
hF.prodMk hG

Premises used: TendstoLocallyUniformly.prodMk, Function.prod
-- 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 : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
⊢ TendstoLocallyUniformlyOn F f p s

Tactic:
tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, tendstoLocallyUniformlyOn_iff_forall_tendsto
-- 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 : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
refine : ∀ (x : α) (hx : x ∈ s), Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ TendstoLocallyUniformlyOn F f p s

Tactic:
refine tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, tendstoLocallyUniformlyOn_iff_forall_tendsto
-- 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 : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
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) (𝓤 β)
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
obtain ⟨t, ht, htr⟩ := h x hx
-- 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 : ∀ 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 (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 t) (𝓤 β)

Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at htr

Premises used: tendstoUniformlyOn_iff_tendsto
-- 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 : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
htr : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 t) (𝓤 β)
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
htr.mono_left <| prod_mono_right _ <| le_principal_iff.mpr ht

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.Tendsto.mono_left, Filter.prod_mono_right
-- 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 : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
htr : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 t) (𝓤 β)
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
exact htr.mono_left <| prod_mono_right _ <| le_principal_iff.mpr ht

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.Tendsto.mono_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 ι
h : ∀ (x : α), ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t
⊢ ∀ (x : α), Membership.mem (γ := Set α) univ x → ∃ t ∈ 𝓝[univ] x, TendstoUniformlyOn F f p t

Tactic:
simpa using h
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ (a : TendstoLocallyUniformlyOn G g p s), ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ (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)
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ (a : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K), ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
obtain : ∀ (K : Set α) (hK3 : K ⊆ s) (hK1 : K ∈ 𝓝 x) (hK2 : IsCompact K), ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
⊢ ∃ 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)

Premises used: Filter.HasBasis.mem_iff, compact_basis_nhds, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩

Premises used: nhdsWithin_le_nhds, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ (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⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ (a : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v), TendstoLocallyUniformlyOn G g p s

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
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
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u

Tactic:
obtain ⟨v, hv1, hv2⟩ := h x hx
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
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:
⟨v, hv1, hv2 u hu⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
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:
exact ⟨v, hv1, hv2 u hu⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
⊢ ∀ (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⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
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
tfae_3_to_1 : ∀ (a : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v), TendstoLocallyUniformlyOn G g p 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

Tactic:
tfae_finish
-- 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 ι
inst_2 : LocallyCompactSpace α
hs : IsOpen[inst] s
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn F f p K

Tactic:
(tendstoLocallyUniformlyOn_TFAE F f p hs).out 0 1

Premises used: tendstoLocallyUniformlyOn_TFAE, List.TFAE.out, OfNat.ofNat
-- 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 : LocallyCompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K

Tactic:
simp only [← tendstoLocallyUniformlyOn_univ,
    tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_univ, Set.subset_univ, forall_true_left]

Premises used: forall_true_left, Set.subset_univ, isOpen_univ, tendstoLocallyUniformlyOn_iff_forall_isCompact, tendstoLocallyUniformlyOn_univ