awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this_1 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
obtain : ∀ (u v : γ) (u_in : (u, v).1 ∈ V₁) (v_in : (u, v).2 ∈ V₂) (w : γ) (huw : (u, w) ∈ W) (hwv : (w, v) ∈ W), False
⊢ False

Tactic:
obtain ⟨⟨u, v⟩, ⟨u_in, v_in⟩, w, huw, hwv⟩ :=
      clusterPt_iff_nonempty.mp hxy.of_inf_left hV₁₂ this

Premises used: clusterPt_iff_nonempty, Iff.mp, ClusterPt.of_inf_left
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this_1 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
u v : γ
u_in : (u, v).1 ∈ V₁
v_in : (u, v).2 ∈ V₂
w : γ
huw : (u, w) ∈ W
hwv : (w, v) ∈ W
⊢ (u ∈ U₁ ∧ w ∈ U₁ ∨ u ∈ U₂ ∧ w ∈ U₂) ∨ u ∈ (V₁ ∪ V₂)ᶜ ∧ w ∈ (V₁ ∪ V₂)ᶜ

Tactic:
simp only [W, U₃, mem_union, mem_prod] at huw hwv

Premises used: Set.mem_union, Set.mem_prod
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this_1 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
u v : γ
u_in : (u, v).1 ∈ V₁
v_in : (u, v).2 ∈ V₂
w : γ
huw : (u, w) ∈ W
hwv : (w, v) ∈ W
huw₁ : (u ∈ U₁ ∧ w ∈ U₁ ∨ u ∈ U₂ ∧ w ∈ U₂) ∨ u ∈ (V₁ ∪ V₂)ᶜ ∧ w ∈ (V₁ ∪ V₂)ᶜ
⊢ (w ∈ U₁ ∧ v ∈ U₁ ∨ w ∈ U₂ ∧ v ∈ U₂) ∨ w ∈ (V₁ ∪ V₂)ᶜ ∧ v ∈ (V₁ ∪ V₂)ᶜ

Tactic:
simp only [W, U₃, mem_union, mem_prod] at huw hwv

Premises used: Set.mem_union, Set.mem_prod
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this_1 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst] V₁
V₂_cl : IsClosed[inst] V₂
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
U₃ : Set γ := (V₁ ∪ V₂)ᶜ
U₃_op : IsOpen[inst] U₃
W : Set (γ × γ) := U₁ ×ˢ U₁ ∪ U₂ ×ˢ U₂ ∪ U₃ ×ˢ U₃
W_in : W ∈ 𝓝Δ
this : W ○ W ∈ F
hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
u v : γ
u_in : (u, v).1 ∈ V₁
v_in : (u, v).2 ∈ V₂
w : γ
huw : (u ∈ U₁ ∧ w ∈ U₁ ∨ u ∈ U₂ ∧ w ∈ U₂) ∨ u ∈ (V₁ ∪ V₂)ᶜ ∧ w ∈ (V₁ ∪ V₂)ᶜ
hwv : (w ∈ U₁ ∧ v ∈ U₁ ∨ w ∈ U₂ ∧ v ∈ U₂) ∨ w ∈ (V₁ ∪ V₂)ᶜ ∧ v ∈ (V₁ ∪ V₂)ᶜ
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (VU₁ : ∀ x ∈ V₁, x ∈ U₁) (VU₂ : ∀ x ∈ V₂, x ∈ U₂)
    (hU₁₂ : ∀ (x : γ), x ∈ U₁ ∧ x ∈ U₂ → Membership.mem (γ := Set γ) ∅ x) (U₃_op : IsOpen[inst] U₃) (W_in : W ∈ 𝓝Δ)
    (this : W ○ W ∈ F) (hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)) (u_in : u ∈ V₁) (v_in : v ∈ V₂)
    (huw : (True ∧ w ∈ U₁ ∨ u ∈ U₂ ∧ w ∈ U₂) ∨ ¬(True ∨ u ∈ V₂) ∧ ¬(w ∈ V₁ ∨ w ∈ V₂))
    (hwv : (w ∈ U₁ ∧ v ∈ U₁ ∨ w ∈ U₂ ∧ True) ∨ ¬(w ∈ V₁ ∨ w ∈ V₂) ∧ ¬(v ∈ V₁ ∨ True)), False
⊢ False

Tactic:
tauto_set
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
simp_rw : 𝓝 x = ⨆ (i : γ), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
⊢ 𝓝 x = comap (Prod.mk x) (𝓝ˢ (diagonal γ))

Tactic:
simp_rw [nhdsSet_diagonal, comap_iSup, nhds_prod_eq, comap_prod, Function.comp_def, comap_id']

Premises used: Filter.comap_prod, Function.comp_def, Filter.comap_iSup, nhdsSet_diagonal, nhds_prod_eq, Filter.comap_id'
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
rw :
  𝓝 x =
    (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
      ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
⊢ 𝓝 x = ⨆ (i : γ), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
rw [iSup_split _ (Inseparable x)]

Premises used: iSup_split, Inseparable
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
a₁ : ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
| (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
congr
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : ∀ (i : γ) (hi : Inseparable x i), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
| ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
enter [1, i, 1, hi]
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x i : γ
hi : Inseparable x i
a : ⊤ ⊓ 𝓝 x
| comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]

Premises used: Inseparable.nhds_eq, mem_of_mem_nhds, Filter.comap_const_of_mem
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : ∀ (i : γ) (hi : Inseparable x i), ⊤ ⊓ 𝓝 x
| ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
enter [1, i, 1, hi]
        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]

Premises used: mem_of_mem_nhds, Filter.comap_const_of_mem
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
· enter [1, i, 1, hi]
        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]

Premises used: mem_of_mem_nhds, Filter.comap_const_of_mem
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : ∀ (i : γ) (hi : ¬Inseparable x i), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
enter [1, i, 1, hi]
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x i : γ
hi : ¬Inseparable x i
a : ⊥ ⊓ 𝓝 i
| comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]

Premises used: mt, not_specializes_iff_exists_open, Filter.comap_const_of_notMem, Specializes.inseparable, And.right, And.left, IsOpen.mem_nhds, Iff.mp, Exists.elim
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : ∀ (i : γ) (hi : ¬Inseparable x i), ⊥ ⊓ 𝓝 i
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
enter [1, i, 1, hi]
        rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : fun (i : γ) ↦ ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
a₁ : ∀ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
a₂ : ∀ (i : γ), fun (x_1 : ¬Inseparable x i) ↦ comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
a₃ : ∀ (i : γ) (hi : ¬Inseparable x i), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
a₄ : ∀ (i : γ) (hi : ¬Inseparable x i), ⊥ ⊓ 𝓝 i
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
· enter [1, i, 1, hi]
        rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
a : ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
a₁ a₂ : ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
| (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
congr
      · enter [1, i, 1, hi]
        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]
      · enter [1, i, 1, hi]
        rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]

Premises used: mem_of_mem_nhds, Filter.comap_const_of_mem
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
conv_rhs : 𝓝 x = (⨆ (i : γ), ⨆ (_ : Inseparable x i), ⊤ ⊓ 𝓝 x) ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i
⊢ 𝓝 x =
    (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
      ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
conv_rhs =>
      congr
      · enter [1, i, 1, hi]
        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]
      · enter [1, i, 1, hi]
        rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]

Premises used: mem_of_mem_nhds, Filter.comap_const_of_mem
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
rw : 𝓝 x = ⊤ ⊓ 𝓝 x ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i
⊢ 𝓝 x = (⨆ (i : γ), ⨆ (_ : Inseparable x i), ⊤ ⊓ 𝓝 x) ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i

Tactic:
rw [iSup_subtype', @iSup_const _ _ _ _ ⟨⟨x, .rfl⟩⟩]

Premises used: iSup_subtype', iSup_const
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
⊢ 𝓝 x = ⊤ ⊓ 𝓝 x ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Nonempty β
⊢ Nonempty (α →ᵤ β)

Tactic:
Pi.instNonempty

Premises used: UniformFun, Pi.instNonempty
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Nonempty β
⊢ Nonempty (α →ᵤ[𝔖] β)

Tactic:
Pi.instNonempty

Premises used: Pi.instNonempty, UniformOnFun
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Subsingleton β
⊢ Subsingleton (α →ᵤ β)

Tactic:
inferInstanceAs <| Subsingleton <| α → β

Premises used: _private.0.instSubsingletonUniformFun._proof_1
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Subsingleton β
⊢ Subsingleton (α →ᵤ[𝔖] β)

Tactic:
inferInstanceAs <| Subsingleton <| α → β

Premises used: _private.0.instSubsingletonUniformOnFun._proof_1
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (toFun : (a : α →ᵤ β) → α → β) ((ofFun : (a : α → β) → α →ᵤ β) f : α →ᵤ β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
f : α →ᵤ β
⊢ (ofFun : (a : α → β) → α →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
f : α → β
⊢ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) f : α →ᵤ[𝔖] β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
⊢ (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓑 : Filter (β × β)
⊢ IsBasis (fun (V : Set (β × β)) ↦ V ∈ 𝓑) (UniformFun.gen α β)

Tactic:
⟨⟨univ, univ_mem⟩, @fun U V hU hV =>
    ⟨U ∩ V, inter_mem hU hV, fun _ huv => ⟨fun x => (huv x).left, fun x => (huv x).right⟩⟩⟩

Premises used: Set.univ, Filter.inter_mem, Filter.IsBasis.mk, Inter.inter, And.right, And.left, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
symm :
  𝓐 ≤ (fun (𝓕 : Filter (β × β)) ↦ UniformFun.filter α β 𝓕) 𝓕 ↔
    (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕
⊢ (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕 ↔
    𝓐 ≤ (fun (𝓕 : Filter (β × β)) ↦ UniformFun.filter α β 𝓕) 𝓕

Tactic:
symm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
rw : 𝓐 ≤ (UniformFun.basis α β 𝓕).filter ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
rw₁ : 𝓐 ≤ generate (UniformFun.basis α β 𝓕).sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
rw₂ rw₃ : (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets

Tactic:
rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]

Premises used: Filter.le_generate_iff, UniformFun.filter, FilterBasis.generate
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐) ↔
    ∀ U ∈ 𝓕,
      {uv : (α →ᵤ β) × (α →ᵤ β) |
          ∀ (x : α),
            Membership.mem (γ := Set (((α →ᵤ β) × (α →ᵤ β)) × α))
              {t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U} (uv, x)} ∈
        𝓐

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, UniformFun.gen
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (∀ U ∈ 𝓕,
      {uv : (α →ᵤ β) × (α →ᵤ β) |
          ∀ (x : α),
            Membership.mem (γ := Set (((α →ᵤ β) × (α →ᵤ β)) × α))
              {t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U} (uv, x)} ∈
        𝓐) ↔
    ∀ U ∈ 𝓕, {uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U} ∈ SProd.sprod (β := Filter α) 𝓐 ⊤

Tactic:
forall₂_congr fun U _hU => mem_prod_top.symm

Premises used: forall₂_congr, Filter.mem_prod_top, Iff.symm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (∀ U ∈ 𝓕, {uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U} ∈ SProd.sprod (β := Filter α) 𝓐 ⊤) ↔
    (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, UniformFun.phi, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
𝓐₁ : 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
⊢ 𝓐 ≤ (fun (𝓕 : Filter (β × β)) ↦ UniformFun.filter α β 𝓕) 𝓕 ↔
    (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕

Tactic:
calc
    𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
      rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
    _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
    _ ↔ ∀ U ∈ 𝓕,
          { uv | ∀ x, (uv, x) ∈ { t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U } } ∈
            𝓐 :=
      Iff.rfl
    _ ↔ ∀ U ∈ 𝓕,
          { uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U } ∈
            𝓐 ×ˢ (⊤ : Filter α) :=
      forall₂_congr fun U _hU => mem_prod_top.symm
    _ ↔ lowerAdjoint 𝓐 ≤ 𝓕 := Iff.rfl

Premises used: Iff.rfl, UniformFun.basis, Filter.sets, FilterBasis.sets, forall₂_congr, UniformFun, Filter.mem_prod_top, UniformFun.filter, Set.image_subset_iff, Prod, Top.top, Iff.symm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ HasBasis (𝓤 (α →ᵤ β)) (fun (x : Set (β × β)) ↦ x ∈ 𝓤 β) (UniformFun.gen α β)

Tactic:
(UniformFun.isBasis_gen α β (𝓤 β)).hasBasis

Premises used: Filter.IsBasis.hasBasis, Set.Mem, uniformity, setOf, Filter.IsBasis.filter, UniformFun.isBasis_gen, FilterBasis.filter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
ι : Sort u_5
p : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis p s
⊢ HasBasis (𝓤 (α →ᵤ β)) p (UniformFun.gen α β ∘ s)

Tactic:
(UniformFun.hasBasis_uniformity α β).to_hasBasis
    (fun _ hU =>
      let ⟨i, hi, hiU⟩ := h.mem_iff.mp hU
      ⟨i, hi, fun _ huv x => hiU (huv x)⟩)
    fun i hi => ⟨s i, h.mem_of_mem hi, subset_rfl⟩

Premises used: Filter.HasBasis.mem_iff, UniformFun.hasBasis_uniformity, Function.comp, Exists, UniformFun.gen, HasSubset.Subset, And, And.intro, Exists.intro, Iff.mp, _private.0.UniformFun.hasBasis_uniformity_of_basis.match_1, Filter.HasBasis.to_hasBasis, subset_rfl, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
f : α →ᵤ β
p : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis p s
⊢ (𝓝 f).HasBasis p fun (i : ι) ↦ {g : α →ᵤ β | (f, g) ∈ UniformFun.gen α β (s i)}

Tactic:
nhds_basis_uniformity' (UniformFun.hasBasis_uniformity_of_basis α β h)

Premises used: Set.Mem, nhds_basis_uniformity', setOf, UniformFun.gen, UniformFun.hasBasis_uniformity_of_basis, UniformSpace.ball, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
f : α →ᵤ β
⊢ (𝓝 f).HasBasis (fun (V : Set (β × β)) ↦ V ∈ 𝓤 β) fun (V : Set (β × β)) ↦ {g : α →ᵤ β | (f, g) ∈ UniformFun.gen α β V}

Tactic:
UniformFun.hasBasis_nhds_of_basis α β f (Filter.basis_sets _)

Premises used: Filter.basis_sets, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
x : α
rw :
  ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆
        (fun (x_1 : (α →ᵤ β) × (α →ᵤ β)) ↦
            (Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β) x_1.1,
              Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β)
                x_1.2)) ⁻¹'
          id i'
⊢ map
      (fun (x_1 : (α →ᵤ β) × (α →ᵤ β)) ↦
        (Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β) x_1.1,
          Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β) x_1.2))
      (𝓤 (α →ᵤ β)) ≤
    𝓤 β

Tactic:
rw [map_le_iff_le_comap,
    (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]

Premises used: UniformFun.hasBasis_uniformity, uniformity, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Filter.basis_sets, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆
        (fun (x_1 : (α →ᵤ β) × (α →ᵤ β)) ↦
            (Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β) x_1.1,
              Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β)
                x_1.2)) ⁻¹'
          id i'

Tactic:
fun U hU => ⟨U, hU, fun uv huv => huv x⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆
        (fun (x_1 : (α →ᵤ β) × (α →ᵤ β)) ↦
            (Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β) x_1.1,
              Function.comp (β := α → β) (Function.eval (β := fun (x : α) ↦ β) x) (⇑toFun : (a : α →ᵤ β) → α → β)
                x_1.2)) ⁻¹'
          id i'

Tactic:
exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_5
f g : α →ᵤ β
V : Set (β × β)
⊢ (f, g) ∈ UniformFun.gen α β V ↔
    ∀ (x : α),
      Membership.mem (α := β × β) V (((toFun : (a : α →ᵤ β) → α → β) f x, (toFun : (a : α →ᵤ β) → α → β) g x) : β × β)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, UniformFun.gen
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
⊢ Monotone (@uniformSpace α γ)

Tactic:
fun _ _ hu =>
  (UniformFun.gc α γ).monotone_u hu

Premises used: GaloisConnection.monotone_u, Set.Mem, Monotone, setOf, UniformFun.gc
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
h : Eq (α := Filter ((α →ᵤ γ) × (α →ᵤ γ))) (𝓤 (α →ᵤ γ)) (𝓤 (α →ᵤ γ))
⊢ uniformSpace α γ = ⨅ (i : ι), uniformSpace α γ

Tactic:
ext : 1
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
h : UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)

Tactic:
rw [iInf_uniformity, iInf_uniformity]

Premises used: iInf_uniformity