awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝 a
hfs : closure[inst_4] (f '' s) ∈ 𝓝 (f a)
⊢ ContinuousAt f a

Tactic:
continuousAt_iff_continuous_left_right.2
    ⟨continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono
        (mem_nhdsWithin_of_mem_nhds hs) (mem_nhdsWithin_of_mem_nhds hfs),
      continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono
        (mem_nhdsWithin_of_mem_nhds hs) (mem_nhdsWithin_of_mem_nhds hfs)⟩

Premises used: Iff.mpr, continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin, continuousAt_iff_continuous_left_right, mem_nhdsWithin_of_mem_nhds, continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin, And.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝 a
hfs : f '' s ∈ 𝓝 (f a)
⊢ ContinuousAt f a

Tactic:
continuousAt_of_monotoneOn_of_closure_image_mem_nhds h_mono hs
    (mem_of_superset hfs subset_closure)

Premises used: subset_closure, continuousAt_of_monotoneOn_of_closure_image_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure[inst_4] (f '' univ) ∈ 𝓝 (f a)

Tactic:
simp only [image_univ, h_dense.closure_eq, univ_mem]

Premises used: Set.image_univ, Dense.closure_eq, Filter.univ_mem
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_surj : Function.Surjective f
⊢ Continuous[inst_1, inst_4] f

Tactic:
h_mono.continuous_of_denseRange h_surj.denseRange

Premises used: Function.Surjective.denseRange, Monotone.continuous_of_denseRange
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
rw :
  ∀ (s : Set β),
    Membership.mem (γ := Set (Set β)) {s : Set β | ∃ (a : β), s = Ioi a ∨ s = Iio a} s →
      IsOpen[inst_2] ((⇑e : (a : α) → β) ⁻¹' s)
⊢ Continuous[inst_2, inst_3] (⇑e : (a : α) → β)

Tactic:
rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]

Premises used: OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
a : β
inl : IsOpen[inst_2] (Ioi ((e.symm : (a : β) → α) a) : Set α)
⊢ IsOpen[inst_2] ((⇑e : (a : α) → β) ⁻¹' Ioi a)

Tactic:
rw [e.preimage_Ioi]

Premises used: OrderIso.preimage_Ioi
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst_2] (Ioi ((e.symm : (a : β) → α) a) : Set α)

Tactic:
apply isOpen_lt'

Premises used: isOpen_lt'
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
a : β
inr : IsOpen[inst_2] (Iio ((e.symm : (a : β) → α) a) : Set α)
⊢ IsOpen[inst_2] ((⇑e : (a : α) → β) ⁻¹' Iio a)

Tactic:
rw [e.preimage_Iio]

Premises used: OrderIso.preimage_Iio
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst_2] (Iio ((e.symm : (a : β) → α) a) : Set α)

Tactic:
apply isOpen_gt'

Premises used: isOpen_gt'
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
⊢ Eq (α := (a : α) → β) (⇑e.toHomeomorph : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology α
inst_5 : OrderTopology β
e : α ≃o β
⊢ Eq (α := (a : β) → α) (⇑(Homeomorph.symm e.toHomeomorph) : (a : β) → α) (⇑e.symm : (a : β) → α)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
set :
  let 𝓝Δ := 𝓝ˢ (diagonal γ);
  (𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s) ≤ 𝓝Δ
⊢ ((𝓝ˢ (diagonal γ)).lift' fun (s : Set (γ × γ)) ↦ s ○ s) ≤ 𝓝ˢ (diagonal γ)

Tactic:
set 𝓝Δ := 𝓝ˢ (diagonal γ)

Premises used: Set.diagonal, nhdsSet
-- Module: Mathlib.Topology.UniformSpace.OfCompactT2
Goal:
γ : Type u_1
inst : TopologicalSpace γ
inst_1 : CompactSpace γ
inst_2 : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
set :
  let F : Filter (γ × γ) := 𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s;
  F ≤ 𝓝Δ
⊢ (𝓝Δ.lift' fun (s : Set (γ × γ)) ↦ s ○ s) ≤ 𝓝Δ

Tactic:
set F := 𝓝Δ.lift' fun s : Set (γ × γ) => s ○ s

Premises used: SetRel.comp, Filter.lift'
-- 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
rw : ∀ V ∈ 𝓝Δ, F ⊓ 𝓟 Vᶜ = ⊥
⊢ F ≤ 𝓝Δ

Tactic:
rw [le_iff_forall_inf_principal_compl]

Premises used: Filter.le_iff_forall_inf_principal_compl
-- 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 ∈ 𝓝Δ
by_contra : ∀ (H : ¬F ⊓ 𝓟 Vᶜ = ⊥), False
⊢ F ⊓ 𝓟 Vᶜ = ⊥

Tactic:
by_contra H
-- 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ᶜ = ⊥
⊢ (F ⊓ 𝓟 Vᶜ).NeBot

Tactic:
haveI : NeBot (F ⊓ 𝓟 Vᶜ) := ⟨H⟩
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
⊢ ∃ (p : γ × γ), ClusterPt p (F ⊓ 𝓟 Vᶜ)

Tactic:
exists_clusterPt_of_compactSpace _

Premises used: exists_clusterPt_of_compactSpace
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
obtain : ∀ (x y : γ) (hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)), False
⊢ False

Tactic:
obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) := exists_clusterPt_of_compactSpace _

Premises used: exists_clusterPt_of_compactSpace
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
⊢ ClusterPt (x, y) (𝓟 Vᶜ)

Tactic:
have clV : ClusterPt (x, y) (𝓟 <| Vᶜ) := hxy.of_inf_right
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
h : Inseparable x y
⊢ (y, y) ∈ (interior V)ᶜ

Tactic:
rw [← mem_closure_iff_clusterPt, (h.prod .rfl).mem_closed_iff isClosed_closure,
        closure_compl] at clV

Premises used: Inseparable.rfl, mem_closure_iff_clusterPt, Inseparable.mem_closed_iff, closure_compl, Inseparable.prod, isClosed_closure
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
h : Inseparable x y
clV₁ : (y, y) ∈ (interior V)ᶜ
⊢ Inseparable x y

Tactic:
rw [← mem_closure_iff_clusterPt, (h.prod .rfl).mem_closed_iff isClosed_closure,
        closure_compl] at clV

Premises used: Inseparable.rfl, mem_closure_iff_clusterPt, Inseparable.mem_closed_iff, closure_compl, Inseparable.prod, isClosed_closure
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
apply : (y, y) ∈ interior V
⊢ False

Tactic:
apply clV
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
rw : V ∈ 𝓝 (y, y)
⊢ (y, y) ∈ interior V

Tactic:
rw [mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ V ∈ 𝓝 (y, y)

Tactic:
nhds_le_nhdsSet (mem_diagonal y) V_in

Premises used: nhds_le_nhdsSet, Set.mem_diagonal
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : (y, y) ∈ (interior V)ᶜ
h : Inseparable x y
⊢ V ∈ 𝓝 (y, y)

Tactic:
exact nhds_le_nhdsSet (mem_diagonal y) V_in

Premises used: nhds_le_nhdsSet, Set.mem_diagonal
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
⊢ ¬Inseparable x y

Tactic:
have ninsep_xy : ¬Inseparable x y := by
      intro h
      rw [← mem_closure_iff_clusterPt, (h.prod .rfl).mem_closed_iff isClosed_closure,
        closure_compl] at clV
      apply clV
      rw [mem_interior_iff_mem_nhds]
      exact nhds_le_nhdsSet (mem_diagonal y) V_in
-- 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 : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
disjoint_nested_nhds_of_not_inseparable :
  ∀ (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₂), False
⊢ False

Tactic:
obtain
      ⟨U₁, -, V₁, V₁_in, U₂, -, V₂, V₂_in, V₁_cl, V₂_cl, U₁_op, U₂_op, VU₁, VU₂, hU₁₂⟩ :=
      disjoint_nested_nhds_of_not_inseparable ninsep_xy

Premises used: disjoint_nested_nhds_of_not_inseparable
-- 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 : (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₂)ᶜ
⊢ IsOpen[inst] U₃

Tactic:
have U₃_op : IsOpen U₃ := (V₁_cl.union V₂_cl).isOpen_compl
-- 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 : (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₃
rw : ∀ x ∈ diagonal γ, W ∈ 𝓝 x
⊢ W ∈ 𝓝Δ

Tactic:
rw [mem_nhdsSet_iff_forall]

Premises used: mem_nhdsSet_iff_forall
-- 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 : (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' : γ
hzz' : (z, z') ∈ diagonal γ
⊢ W ∈ 𝓝 (z, z')

Tactic:
IsOpen.mem_nhds ?_ ?_

Premises used: IsOpen.mem_nhds
-- 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 : (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' : γ
hzz' : (z, z') ∈ diagonal γ
refine_1 : IsOpen[instTopologicalSpaceProd] W
refine_2 : (z, z') ∈ W
⊢ W ∈ 𝓝 (z, z')

Tactic:
refine IsOpen.mem_nhds ?_ ?_

Premises used: IsOpen.mem_nhds
-- 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 : (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' : γ
hzz' : (z, z') ∈ diagonal γ
⊢ IsOpen[instTopologicalSpaceProd] W

Tactic:
apply_rules [IsOpen.union, IsOpen.prod]

Premises used: IsOpen.union, IsOpen.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 : (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' : γ
hzz' : (z, z') ∈ diagonal γ
refine_2 : (z, z) ∈ W
⊢ (z, z') ∈ W

Tactic:
cases hzz'
-- 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 : (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 : γ
refine_2 : (z ∈ U₁ ∧ z ∈ U₁ ∨ z ∈ U₂ ∧ z ∈ U₂) ∨ z ∈ (V₁ ∪ V₂)ᶜ ∧ z ∈ (V₁ ∪ V₂)ᶜ
⊢ (z, z) ∈ W

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

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 : (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 : γ
refine_2 refine_2₁ refine_2₂ 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₂)
⊢ (z ∈ U₁ ∧ z ∈ U₁ ∨ z ∈ U₂ ∧ z ∈ U₂) ∨ z ∈ (V₁ ∪ V₂)ᶜ ∧ z ∈ (V₁ ∪ V₂)ᶜ

Tactic:
tauto_set
-- 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 : (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 ∈ 𝓝Δ

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
-- 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 : (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 ∈ 𝓝Δ
⊢ W ○ W ∈ F

Tactic:
have : W ○ W ∈ F := mem_lift' W_in
-- 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
⊢ V₁ ×ˢ V₂ ∈ 𝓝 (x, y)

Tactic:
have hV₁₂ : V₁ ×ˢ V₂ ∈ 𝓝 (x, y) := prod_mem_nhds V₁_in V₂_in