awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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 : (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₃
z : γ
⊢ (z ∈ U₁ ∧ z ∈ U₁ ∨ z ∈ U₂ ∧ z ∈ U₂) ∨ z ∈ (V₁ ∪ V₂)ᶜ ∧ z ∈ (V₁ ∪ V₂)ᶜ
have refine_2 : ∀ (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₃),
  (z ∈ U₁ ∧ z ∈ U₁ ∨ z ∈ U₂ ∧ z ∈ U₂) ∨ ¬(z ∈ V₁ ∨ z ∈ V₂) ∧ ¬(z ∈ V₁ ∨ z ∈ V₂)
Tactic: tauto_set
Cleared hypotheses: VU₁, VU₂, hU₁₂, U₃_op
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
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 : (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₃
⊢ False
have W_in : W ∈ 𝓝Δ
Tactic: have W_in : W ∈ 𝓝Δ := by
      rw [mem_nhdsSet_iff_forall]
      rintro ⟨z, z'⟩ hzz'
      refine IsOpen.mem_nhds ?_ ?_
      · apply_rules [IsOpen.union, IsOpen.prod]
      · cases hzz'
        simp only [W, U₃, mem_union, mem_prod]
        tauto_set
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
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 : (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 ∈ 𝓝Δ
⊢ False
have this₁ : W ○ W ∈ F
Tactic: have : W ○ W ∈ F := mem_lift' W_in
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
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
⊢ False
have hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y)
Tactic: have hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y) := prod_mem_nhds V₁_in V₂_in
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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)
⊢ False
have 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
Tactic: obtain ⟨⟨u, v⟩, ⟨u_in, v_in⟩, w, huw, hwv⟩ :=
      clusterPt_iff_nonempty.mp hxy.of_inf_left hV₁₂ this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
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
⊢ False
have huw₁ : (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
Cleared hypotheses: huw, hwv
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (hypothesis)
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₂)ᶜ
⊢ False
have hwv₁ : (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
Cleared hypotheses: huw, hwv
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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₂)ᶜ
⊢ False
have 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
Tactic: tauto_set
Cleared hypotheses: VU₁, VU₂, hU₁₂, U₃_op, W_in, this, hV₁₂, u_in, v_in, huw, hwv
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
⊢ 𝓝 x = comap (Prod.mk x) (𝓝ˢ (diagonal γ))
have simp_rw : 𝓝 x = ⨆ (i : γ), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
Tactic: simp_rw [nhdsSet_diagonal, comap_iSup, nhds_prod_eq, comap_prod, Function.comp_def, comap_id']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
⊢ 𝓝 x = ⨆ (i : γ), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have rw : 𝓝 x =
  (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
Tactic: rw [iSup_split _ (Inseparable x)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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
| (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a₁ : ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ∀ (i : γ) (hi : Inseparable x i), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
Tactic: enter [1, i, 1, hi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x i : γ
hi : Inseparable x i
| comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ⊤ ⊓ 𝓝 x
Tactic: rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| ⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ∀ (i : γ) (hi : Inseparable x i), ⊤ ⊓ 𝓝 x
Tactic: enter [1, i, 1, hi]
        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ∀ (i : γ) (hi : ¬Inseparable x i), comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
Tactic: enter [1, i, 1, hi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x i : γ
hi : ¬Inseparable x i
| comap (fun (x_1 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ⊥ ⊓ 𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ∀ (i : γ) (hi : ¬Inseparable 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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : fun (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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a₁ : ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a₂ : ∀ (i : γ), fun (x_1 : ¬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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a₃ : ∀ (i : γ) (hi : ¬Inseparable x i), comap (fun (x_1 : γ) ↦ 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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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
| ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a₄ : ∀ (i : γ) (hi : ¬Inseparable 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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
| (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a : ⨆ (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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
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
| (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
    ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have a₁ : ⨆ (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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
⊢ 𝓝 x =
    (⨆ (i : γ), ⨆ (_ : Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i) ⊔
      ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), comap (fun (x_2 : γ) ↦ x) (𝓝 i) ⊓ 𝓝 i
have conv_rhs : 𝓝 x = (⨆ (i : γ), ⨆ (_ : Inseparable x i), ⊤ ⊓ 𝓝 x) ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable 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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfCompactT2 (goal)
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
x : γ
⊢ 𝓝 x = (⨆ (i : γ), ⨆ (_ : Inseparable x i), ⊤ ⊓ 𝓝 x) ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i
have rw : 𝓝 x = ⊤ ⊓ 𝓝 x ⊔ ⨆ (i : γ), ⨆ (_ : ¬Inseparable x i), ⊥ ⊓ 𝓝 i
Tactic: rw [iSup_subtype', @iSup_const _ _ _ _ ⟨⟨x, .rfl⟩⟩]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕 ↔
    𝓐 ≤ (fun (𝓕 : Filter (β × β)) ↦ UniformFun.filter α β 𝓕) 𝓕
have symm : 𝓐 ≤ (fun (𝓕 : Filter (β × β)) ↦ UniformFun.filter α β 𝓕) 𝓕 ↔
  (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
have rw : 𝓐 ≤ (UniformFun.basis α β 𝓕).filter ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
Tactic: rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
rw : 𝓐 ≤ (UniformFun.basis α β 𝓕).filter ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
have rw₁ : 𝓐 ≤ generate (UniformFun.basis α β 𝓕).sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
Tactic: rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
have rw₂ : (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
Tactic: rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (fun (𝓕 : Filter (β × β)) ↦ UniformFun.filter α β 𝓕) 𝓕 ↔
    (fun (𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))) ↦ map (UniformFun.phi α β) (SProd.sprod (β := Filter α) 𝓐 ⊤)) 𝓐 ≤ 𝓕
have 𝓐₁ : 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
x : α
⊢ 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))
      (𝓤 (α →ᵤ β)) ≤
    𝓤 β
have 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'
Tactic: rw [map_le_iff_le_comap,
    (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ uniformSpace α γ = ⨅ (i : ι), uniformSpace α γ
have h : Eq (α := Filter ((α →ᵤ γ) × (α →ᵤ γ))) (𝓤 (α →ᵤ γ)) (𝓤 (α →ᵤ γ))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)
have h : UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)
Tactic: rw [iInf_uniformity, iInf_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ
have rw : Eq (α := UniformSpace (α →ᵤ γ)) (⨅ (i : Bool), uniformSpace α γ)
  (⨅ (b : Bool), bif b then uniformSpace α γ else uniformSpace α γ)
Tactic: rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ Eq (α := UniformSpace (α →ᵤ γ)) (⨅ (i : Bool), uniformSpace α γ)
    (⨅ (b : Bool), bif b then uniformSpace α γ else uniformSpace α γ)
have refine : ∀ (i : Bool), uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
Tactic: refine iInf_congr fun i => ?_