awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
hunion : ∀ (p : α) (hp : p ∈ v ∩ v') (x : β) (hx : x ∈ t ∪ t'), (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u

Tactic:
refine ⟨v ∩ v', inter_mem v_mem v'_mem, fun p hp x hx ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
hx : x ∈ t ∪ t'
hunion : ∀ (h'x : x ∈ t), (f p x, f q x) ∈ u
hunion₁ : ∀ (h'x : x ∈ t'), (f p x, f q x) ∈ u
⊢ (f p x, f q x) ∈ u

Tactic:
rcases hx with h'x | h'x
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t
⊢ (f p x, f q x) ∈ u

Tactic:
hv p hp.1 x h'x

Premises used: And.left
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t
⊢ (f p x, f q x) ∈ u

Tactic:
exact hv p hp.1 x h'x

Premises used: And.left
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t'
⊢ (f p x, f q x) ∈ u

Tactic:
hv' p hp.2 x h'x

Premises used: And.right
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
h'x : x ∈ t'
⊢ (f p x, f q x) ∈ u

Tactic:
exact hv' p hp.2 x h'x

Premises used: And.right
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
hnhds :
  ∀ (u' : Set (E × E)) (u'_mem : u' ∈ 𝓤 E) (u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u')
    (hu' : SetRel.comp u' u' ⊆ u), ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
rcases comp_symm_of_uniformity hu with ⟨u', u'_mem, u'_symm, hu'⟩

Premises used: comp_symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
⊢ ∃ v ∈ 𝓝[s] q, ∃ w ∈ 𝓝[k] x, v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}

Tactic:
mem_nhdsWithin_prod_iff.1 (hf (q, x) ⟨hq, hx⟩ (mem_nhds_left (f q x) u'_mem))

Premises used: mem_nhds_left, Prod.mk, mem_nhdsWithin_prod_iff, And.intro, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
hnhds :
  ∀ (v : Set α) (hv : v ∈ 𝓝[s] q) (w : Set β) (hw : w ∈ 𝓝[k] x)
    (hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}),
    ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
obtain ⟨v, hv, w, hw, hvw⟩ :
      ∃ v ∈ 𝓝[s] q, ∃ w ∈ 𝓝[k] x, v ×ˢ w ⊆ f.uncurry ⁻¹' {z | (f q x, z) ∈ u'} :=
        mem_nhdsWithin_prod_iff.1 (hf (q, x) ⟨hq, hx⟩ (mem_nhds_left (f q x) u'_mem))

Premises used: mem_nhds_left, Prod.mk, mem_nhdsWithin_prod_iff, And.intro, Iff.mp, Function.uncurry
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
⟨w, hw, v, hv, fun p hp y hy ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
hnhds : ∀ (p : α) (hp : p ∈ v) (y : β) (hy : y ∈ w), (f p y, f q y) ∈ u
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
refine ⟨w, hw, v, hv, fun p hp y hy ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
⊢ (f q x, f p y) ∈ u'

Tactic:
have A : (f q x, f p y) ∈ u' := hvw (⟨hp, hy⟩ : (p, y) ∈ v ×ˢ w)
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
⊢ (f q x, f q y) ∈ u'

Tactic:
have B : (f q x, f q y) ∈ u' := hvw (⟨mem_of_mem_nhdsWithin hq hv, hy⟩ : (q, y) ∈ v ×ˢ w)
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
B : (f q x, f q y) ∈ u'
⊢ (f p y, f q y) ∈ u

Tactic:
hu' <| SetRel.prodMk_mem_comp (u'_symm A) B

Premises used: SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
B : (f q x, f q y) ∈ u'
⊢ (f p y, f q y) ∈ u

Tactic:
exact hu' <| SetRel.prodMk_mem_comp (u'_symm A) B

Premises used: SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Type u_4
F : ι → β → α
inst_2 : CompactSpace β
h : Equicontinuous F
⊢ Continuous[inst_1.toTopologicalSpace, UniformFun.topologicalSpace ι α]
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)

Tactic:
rw [equicontinuous_iff_continuous] at h

Premises used: equicontinuous_iff_continuous
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Type u_4
F : ι → β → α
inst_2 : CompactSpace β
h :
  Continuous[inst_1.toTopologicalSpace, UniformFun.topologicalSpace ι α]
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
rw :
  UniformContinuous (β := UniformFun ι α)
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
⊢ UniformEquicontinuous F

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous]

Premises used: uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Type u_4
F : ι → β → α
inst_2 : CompactSpace β
h :
  Continuous[inst_1.toTopologicalSpace, UniformFun.topologicalSpace ι α]
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
⊢ UniformContinuous (β := UniformFun ι α)
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)

Tactic:
CompactSpace.uniformContinuous_of_continuous h

Premises used: CompactSpace.uniformContinuous_of_continuous
-- Module: Mathlib.Topology.UniformSpace.HeineCantor
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Type u_4
F : ι → β → α
inst_2 : CompactSpace β
h :
  Continuous[inst_1.toTopologicalSpace, UniformFun.topologicalSpace ι α]
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
⊢ UniformContinuous (β := UniformFun ι α)
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)

Tactic:
exact CompactSpace.uniformContinuous_of_continuous h

Premises used: CompactSpace.uniformContinuous_of_continuous
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p

Tactic:
simp [TendstoLocallyUniformlyOn, TendstoLocallyUniformly, nhdsWithin_univ]

Premises used: TendstoLocallyUniformlyOn, nhdsWithin_univ, TendstoLocallyUniformly
-- 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 ι
x : α
h : x ∈ s
x_1 : Set (β × β)
h_1 : x_1 ∈ 𝓤 β
simp_rw :
  (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
    (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ⁻¹' x_1 ∈ p ×ˢ 𝓝[s] x
simp_rw₁ :
  (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
    ∃ t ∈ 𝓝[s] x,
      ∀ᶠ (x : ι) in p,
        ∀ y ∈ t, Membership.mem (γ := Set (ι × α)) ((fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ⁻¹' x_1) (x, y)
⊢ (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
    Membership.mem (γ := Filter (β × β)) (map (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x)) x_1

Tactic:
simp_rw [mem_map, mem_prod_iff_right, mem_preimage]

Premises used: Filter.mem_prod_iff_right, Filter.mem_map, Set.mem_preimage
-- 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 : IsOpen[inst] s
x : α
hx : x ∈ s
rw rw₁ :
  Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) ↔
    Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
⊢ 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 ×ˢ 𝓝 x) (𝓤 β)

Tactic:
rw [hs.nhdsWithin_eq hx]

Premises used: IsOpen.nhdsWithin_eq
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

Premises used: IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto, isOpen_univ, tendstoLocallyUniformlyOn_univ
-- 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 ι
simp :
  (∀ (x : { a : α // a ∈ s }),
      Tendsto ((fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ∘ Prod.map id (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (p ×ˢ 𝓝 x)
        (𝓤 β)) ↔
    ∀ (x : (↑s : Type u_1)),
      Tendsto
        (fun (y : Prod.{u_4, u_1} ι (↑s : Type u_1)) ↦
          ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) y.2, F y.1 (↑y.2 : α)))
        (p ×ˢ 𝓝 x) (𝓤 β)
⊢ TendstoLocallyUniformlyOn F f p s ↔
    TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p

Tactic:
simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
    tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]

Premises used: Filter.tendsto_map'_iff, Filter.prod_map_right, tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendstoLocallyUniformlyOn_iff_forall_tendsto, map_nhds_subtype_val
-- 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 ι
⊢ (∀ (x : { a : α // a ∈ s }),
      Tendsto ((fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ∘ Prod.map id (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (p ×ˢ 𝓝 x)
        (𝓤 β)) ↔
    ∀ (x : (↑s : Type u_1)),
      Tendsto
        (fun (y : Prod.{u_4, u_1} ι (↑s : Type u_1)) ↦
          ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) y.2, F y.1 (↑y.2 : α)))
        (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
rfl
-- 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 : TendstoUniformlyOn F f p s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
h_1 : x ∈ s
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u

Tactic:
simpa using h u hu
-- 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 : TendstoUniformly F f p
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
⊢ ∀ᶠ (n : ι) in p, ∀ (y : α), Membership.mem (γ := Set α) univ y → (f y, F n y) ∈ u

Tactic:
simpa using h u hu
-- 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 ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
rcases :
  ∀ (t : Set α) (ht : t ∈ 𝓝[s] x) (H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u),
    ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases h u hu x (h' hx) with ⟨t, ht, H⟩
-- 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 ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

Premises used: id, Filter.Eventually.mono, And.intro, Exists.intro, nhdsWithin_mono
-- 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 ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Sort u_5
S : ι' → Set α
hS : ∀ (i : ι'), IsOpen[inst] (S i)
h : ∀ (i : ι'), TendstoLocallyUniformlyOn F f p (S i)
⊢ TendstoLocallyUniformlyOn F f p (⋃ (i : ι'), S i)

Tactic:
(isOpen_iUnion hS).tendstoLocallyUniformlyOn_iff_forall_tendsto.2 fun _x hx =>
    let ⟨i, hi⟩ := mem_iUnion.1 hx
    (hS i).tendstoLocallyUniformlyOn_iff_forall_tendsto.1 (h i) _ hi

Premises used: IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto, Iff.mpr, SProd.sprod, uniformity, Set.mem_iUnion, nhds, Prod.mk, Prod.fst, isOpen_iUnion, Filter.Tendsto, Iff.mp, _private.0.tendstoLocallyUniformlyOn_iUnion.match_1, Prod.snd
-- 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 ι
s : Set γ
S : γ → Set α
hS : ∀ i ∈ s, IsOpen[inst] (S i)
h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)
⊢ TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i)

Tactic:
tendstoLocallyUniformlyOn_iUnion (fun i => isOpen_iUnion (hS i))
    fun i ↦ tendstoLocallyUniformlyOn_iUnion (hS i) (h i)

Premises used: isOpen_iUnion, tendstoLocallyUniformlyOn_iUnion
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen[inst] s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
rw : TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen[inst] s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)

Tactic:
tendstoLocallyUniformlyOn_biUnion hS h

Premises used: tendstoLocallyUniformlyOn_biUnion
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen[inst] s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)

Tactic:
exact tendstoLocallyUniformlyOn_biUnion hS h

Premises used: tendstoLocallyUniformlyOn_biUnion
-- 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'
rw : TendstoLocallyUniformlyOn F f p (⋃₀ {s, s'})
⊢ TendstoLocallyUniformlyOn F f p (s ∪ s')

Tactic:
rw [← sUnion_pair]

Premises used: Set.sUnion_pair
-- 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'
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s, s'})

Tactic:
tendstoLocallyUniformlyOn_sUnion _ ?_ ?_

Premises used: tendstoLocallyUniformlyOn_sUnion
-- 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'
refine_1 : ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → IsOpen[inst] s_1
refine_2 : ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → TendstoLocallyUniformlyOn F f p s_1
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s, s'})

Tactic:
refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_

Premises used: tendstoLocallyUniformlyOn_sUnion