awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
rw :
  TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_2)) ↦ F i (↑x : α))
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop
⊢ TendstoLocallyUniformlyOn F f atTop s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe]

Premises used: tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_2)) ↦ F i (↑x : α))
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop

Tactic:
tendstoLocallyUniformly_of_forall_tendsto (hF_cont · |>.restrict)
    (fun _ _ h x ↦ hF_mono _ x.2 h) hf.restrict (fun x ↦ h_tendsto x x.2)

Premises used: ContinuousOn.restrict, Subtype.val, Monotone.tendstoLocallyUniformly_of_forall_tendsto, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_2)) ↦ F i (↑x : α))
    (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) atTop

Tactic:
exact tendstoLocallyUniformly_of_forall_tendsto (hF_cont · |>.restrict)
    (fun _ _ h x ↦ hF_mono _ x.2 h) hf.restrict (fun x ↦ h_tendsto x x.2)

Premises used: ContinuousOn.restrict, Subtype.val, Monotone.tendstoLocallyUniformly_of_forall_tendsto, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
inst_6 : CompactSpace α
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoUniformly F f atTop

Tactic:
tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace.mp <|
    tendstoLocallyUniformly_of_forall_tendsto hF_cont hF_mono hf h_tendsto

Premises used: tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, Iff.mp, Monotone.tendstoLocallyUniformly_of_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hs : IsCompact s
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoUniformlyOn F f atTop s

Tactic:
tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hs |>.mp <|
    tendstoLocallyUniformlyOn_of_forall_tendsto hF_cont hF_mono hf h_tendsto

Premises used: tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact, Iff.mp, Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_anti : Antitone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly F f atTop

Tactic:
Monotone.tendstoLocallyUniformly_of_forall_tendsto (G := Gᵒᵈ) hF_cont hF_anti hf h_tendsto

Premises used: OrderDual, Monotone.tendstoLocallyUniformly_of_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_anti : ∀ x ∈ s, Antitone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformlyOn F f atTop s

Tactic:
Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto (G := Gᵒᵈ) hF_cont hF_anti hf h_tendsto

Premises used: Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto, OrderDual
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
inst_6 : CompactSpace α
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_anti : Antitone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoUniformly F f atTop

Tactic:
Monotone.tendstoUniformly_of_forall_tendsto (G := Gᵒᵈ) hF_cont hF_anti hf h_tendsto

Premises used: Monotone.tendstoUniformly_of_forall_tendsto, OrderDual
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hs : IsCompact s
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_anti : ∀ x ∈ s, Antitone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoUniformlyOn F f atTop s

Tactic:
Monotone.tendstoUniformlyOn_of_forall_tendsto (G := Gᵒᵈ) hs hF_cont hF_anti hf h_tendsto

Premises used: Monotone.tendstoUniformlyOn_of_forall_tendsto, OrderDual
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → C(α, G)
f : C(α, G)
hF_mono : Monotone F
h_tendsto :
  ∀ (x : α),
    Tendsto.{u_1, u_3} (β := G) (fun (x_1 : ι) ↦ ((F x_1 : (a : α) → G) x : G)) atTop
      (𝓝 ((f : (a : α) → G) x) : Filter G)
⊢ Tendsto F atTop (𝓝 f)

Tactic:
tendsto_of_tendstoLocallyUniformly <|
    hF_mono.tendstoLocallyUniformly_of_forall_tendsto (F · |>.continuous) f.continuous h_tendsto

Premises used: ContinuousMap.continuous, ContinuousMap.tendsto_of_tendstoLocallyUniformly, Monotone.tendstoLocallyUniformly_of_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → C(α, G)
f : C(α, G)
hF_anti : Antitone F
h_tendsto :
  ∀ (x : α),
    Tendsto.{u_1, u_3} (β := G) (fun (x_1 : ι) ↦ ((F x_1 : (a : α) → G) x : G)) atTop
      (𝓝 ((f : (a : α) → G) x) : Filter G)
⊢ Tendsto F atTop (𝓝 f)

Tactic:
tendsto_of_monotone_of_pointwise (G := Gᵒᵈ) hF_anti h_tendsto

Premises used: ContinuousMap.tendsto_of_monotone_of_pointwise, OrderDual
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
⊢ DiscreteUniformity X

Tactic:
@DiscreteUniformity.mk X ⊥ rfl

Premises used: DiscreteUniformity.mk, rfl
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_2
inst : UniformSpace X
rw : inst = ⊥ ↔ uniformity X = 𝓟 SetRel.id
rw₁ : (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ uniformity X = 𝓟 SetRel.id
rw₂ :
  (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔
    ∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s
rw₃ rw₄ :
  (∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s) ↔
    ∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id

Tactic:
rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]

Premises used: bot_uniformity, Filter.ext_iff, discreteUniformity_iff_eq_bot, UniformSpace.ext_iff
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
⊢ uniformity X = 𝓟 SetRel.id

Tactic:
discreteUniformity_iff_eq_principal_setRelId.mp inferInstance

Premises used: inferInstance, discreteUniformity_iff_eq_principal_setRelId, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
rw : Eq.{u_1 + 1} (α := TopologicalSpace X) toTopologicalSpace ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := TopologicalSpace X) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := TopologicalSpace X) toTopologicalSpace ⊥

Tactic:
rw [DiscreteUniformity.eq_bot (X := X), UniformSpace.toTopologicalSpace_bot]

Premises used: DiscreteUniformity.eq_bot, UniformSpace.toTopologicalSpace_bot
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_2
inst : UniformSpace X
rw : DiscreteUniformity X ↔ inst = ⊥
rw₁ rw₂ : inst = ⊥ ↔ inst = ⊥
⊢ DiscreteUniformity X ↔ SetRel.id ∈ uniformity X

Tactic:
rw [← uniformSpace_eq_bot, discreteUniformity_iff_eq_bot]

Premises used: discreteUniformity_iff_eq_bot, UniformSpace.uniformSpace_eq_bot
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
⊢ SetRel.id ∈ uniformity X

Tactic:
discreteUniformity_iff_setRelId_mem_uniformity.mp inferInstance

Premises used: inferInstance, discreteUniformity_iff_setRelId_mem_uniformity, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h :
  ∀ (x : Y × Y),
    Membership.mem (γ := Set (Y × Y)) SetRel.id x ↔
      Membership.mem (γ := Set (Y × Y)) (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1}) x
⊢ Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})

Tactic:
ext x
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
x : Y × Y
⊢ Membership.mem (γ := Set (Y × Y)) SetRel.id x ↔
    Membership.mem (γ := Set (Y × Y)) (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1}) x

Tactic:
simp [SetRel.id]

Premises used: SetRel.id
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
⊢ Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})

Tactic:
have h : SetRel.id = ⋂ y : Y, {p | p.2 = y → p.1 ∈ ({y} : Set Y)} := by
    ext x
    simp [SetRel.id]
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
simp_rw₂ : ∀ (i : Y), {p : Y × Y | p.2 = i → Membership.mem (γ := Set Y) {i} p.1} ∈ uniformity Y
simp_rw₃ : ∀ (i : Y), {i} ∈ nhds i
simp_rw₄ : ∀ (i : Y), Membership.mem (γ := Filter Y) (pure i) {i}
simp_rw₅ : ∀ (i : Y), Membership.mem (γ := Set Y) {i} i
simp_rw₆ : ∀ (i : Y), True
⊢ DiscreteUniformity Y

Tactic:
simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]

Premises used: mem_nhds_uniformity_iff_left, discreteUniformity_iff_setRelId_mem_uniformity, Set.mem_singleton_iff, Filter.iInter_mem, nhds_discrete, implies_true, Filter.mem_pure
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : UniformSpace Y
inst_2 : DiscreteUniformity Y
⊢ DiscreteUniformity (X × Y)

Tactic:
simp [discreteUniformity_iff_eq_principal_setRelId, uniformity_prod_eq_comap_prod,
    eq_principal_setRelId, SetRel.id, Set.prod_eq, Prod.ext_iff, Set.setOf_and]

Premises used: Set.setOf_and, SetRel.id, Prod.ext_iff, Set.prod_eq, discreteUniformity_iff_eq_principal_setRelId, DiscreteUniformity.eq_principal_setRelId, uniformity_prod_eq_comap_prod
-- Module: Mathlib.Topology.UniformSpace.DiscreteUniformity
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : UniformSpace Y
f : X → Y
⊢ UniformContinuous f

Tactic:
simp only [uniformContinuous_iff, DiscreteUniformity.eq_bot, bot_le]

Premises used: DiscreteUniformity.eq_bot, uniformContinuous_iff, bot_le
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
H : EquicontinuousAt F x₀
S : Set X
⊢ EquicontinuousWithinAt F S x₀

Tactic:
fun U hU ↦ (H U hU).filter_mono inf_le_left

Premises used: Filter.Eventually.filter_mono, EquicontinuousWithinAt, nhdsWithin, inf_le_left
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
S T : Set X
H : EquicontinuousWithinAt F T x₀
hST : S ⊆ T
⊢ EquicontinuousWithinAt F S x₀

Tactic:
fun U hU ↦ (H U hU).filter_mono <| nhdsWithin_mono x₀ hST

Premises used: Filter.Eventually.filter_mono, EquicontinuousWithinAt, nhdsWithin_mono
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
rw : (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔ EquicontinuousAt F x₀
rw₁ :
  (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
rw₂ rw₃ :
  (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
⊢ EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀

Tactic:
rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]

Premises used: EquicontinuousWithinAt, nhdsWithin_univ, EquicontinuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : (↑S : Type u_3)
⊢ EquicontinuousAt (S.restrict (π := fun (a : X) ↦ α) ∘ F) x₀ ↔ EquicontinuousWithinAt F S (↑x₀ : X)

Tactic:
simp [EquicontinuousWithinAt, EquicontinuousAt,
    ← eventually_nhds_subtype_iff]

Premises used: EquicontinuousWithinAt, eventually_nhds_subtype_iff, EquicontinuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
H : Equicontinuous F
S : Set X
⊢ EquicontinuousOn F S

Tactic:
fun x _ ↦ (H x).equicontinuousWithinAt S

Premises used: EquicontinuousOn, EquicontinuousAt.equicontinuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S T : Set X
H : EquicontinuousOn F T
hST : S ⊆ T
⊢ EquicontinuousOn F S

Tactic:
fun x hx ↦ (H x (hST hx)).mono hST

Premises used: EquicontinuousOn, EquicontinuousWithinAt.mono
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ EquicontinuousOn F univ ↔ Equicontinuous F

Tactic:
simp [EquicontinuousOn, Equicontinuous]

Premises used: Equicontinuous, EquicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ Equicontinuous (S.restrict (π := fun (a : X) ↦ α) ∘ F) ↔ EquicontinuousOn F S

Tactic:
simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff]

Premises used: Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
H : UniformEquicontinuous F
S : Set β
⊢ UniformEquicontinuousOn F S

Tactic:
fun U hU ↦ (H U hU).filter_mono inf_le_left

Premises used: Filter.Eventually.filter_mono, UniformEquicontinuousOn, inf_le_left
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S T : Set β
H : UniformEquicontinuousOn F T
hST : S ⊆ T
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ 𝓤 β ⊓ 𝓟 (S ×ˢ S) ≤ 𝓤 β ⊓ 𝓟 (T ×ˢ T)

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuousOn F univ ↔ UniformEquicontinuous F

Tactic:
simp [UniformEquicontinuousOn, UniformEquicontinuous]

Premises used: UniformEquicontinuousOn, UniformEquicontinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
U : Set (α × α)
rw :
  map (α := { x : β // x ∈ S } × { x : β // x ∈ S })
    (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
    (Filter.comap (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S))) (𝓤 β))
| 𝓤 β ⊓ 𝓟 (S ×ˢ S)

Tactic:
rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]

Premises used: Filter.map_comap, Subtype.range_val, Set.range_prodMap
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
conv :
  (∀ U ∈ 𝓤 α,
      ∀ᶠ (xy : (↑S : Type u_8) × (↑S : Type u_8)) in 𝓤 (↑S : Type u_8),
        ∀ (i : ι),
          ((S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.1, (S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.2) ∈ U) ↔
    ∀ U ∈ 𝓤 α,
      ∀ᶠ (xy : β × β) in
        map (α := { x : β // x ∈ S } × { x : β // x ∈ S })
          (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
          (Filter.comap (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
            (𝓤 β)),
        ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
⊢ (∀ U ∈ 𝓤 α,
      ∀ᶠ (xy : (↑S : Type u_8) × (↑S : Type u_8)) in 𝓤 (↑S : Type u_8),
        ∀ (i : ι),
          ((S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.1, (S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.2) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U

Tactic:
conv in _ ⊓ _ => rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]

Premises used: Filter.map_comap, Subtype.range_val, Set.range_prodMap
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ (∀ U ∈ 𝓤 α,
      ∀ᶠ (xy : (↑S : Type u_8) × (↑S : Type u_8)) in 𝓤 (↑S : Type u_8),
        ∀ (i : ι),
          ((S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.1, (S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.2) ∈ U) ↔
    ∀ U ∈ 𝓤 α,
      ∀ᶠ (xy : β × β) in
        map (α := { x : β // x ∈ S } × { x : β // x ∈ S })
          (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
          (Filter.comap (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
            (𝓤 β)),
        ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
h : IsEmpty ι
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀

Tactic:
fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Premises used: IsEmpty.elim, Filter.Eventually.of_forall, EquicontinuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
h : IsEmpty ι
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀

Tactic:
fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Premises used: EquicontinuousWithinAt, IsEmpty.elim, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : IsEmpty ι
F : ι → X → α
⊢ Equicontinuous F

Tactic:
equicontinuousAt_empty F

Premises used: Equicontinuous, equicontinuousAt_empty
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : IsEmpty ι
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S

Tactic:
fun x₀ _ ↦ equicontinuousWithinAt_empty F S x₀

Premises used: equicontinuousWithinAt_empty, EquicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
h : IsEmpty ι
F : ι → β → α
⊢ UniformEquicontinuous F

Tactic:
fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Premises used: IsEmpty.elim, Filter.Eventually.of_forall, UniformEquicontinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
h : IsEmpty ι
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S

Tactic:
fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Premises used: IsEmpty.elim, UniformEquicontinuousOn, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Finite ι
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀

Tactic:
simp [EquicontinuousAt, ContinuousAt, (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff,
    UniformSpace.ball, @forall_comm _ ι]

Premises used: ContinuousAt, nhds_basis_uniformity', uniformity, forall_comm, UniformSpace.ball, Filter.basis_sets, EquicontinuousAt, Filter.HasBasis.tendsto_right_iff