awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
k : Fin #t
⊢ Ne.{u_2 + 1} (α := Clopens X) ((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) ⊥

Tactic:
(Finset.mem_filter.mp (t.equivFin.symm k).2).2

Premises used: Finset.equivFin, And.right, Iff.mp, Finset.mem_filter, Equiv.symm, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
k : Fin #t
⊢ Ne.{u_2 + 1} (α := Clopens X) ((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) ⊥

Tactic:
exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2

Premises used: Finset.equivFin, And.right, Iff.mp, Finset.mem_filter, Equiv.symm, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
k : Fin #t
⊢ ∃ (i : ι),
    (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) : Set X) ⊆ (↑(U i) : Set X)

Tactic:
match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩

Premises used: Finset.equivFin, subset_trans, Exists, HasSubset.Subset, SetLike.coe, Exists.intro, Equiv.symm, Subtype.val, DFunLike.coe, _private.0.TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover.match_2
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
k : Fin #t
⊢ ∃ (i : ι),
    (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) : Set X) ⊆ (↑(U i) : Set X)

Tactic:
exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
refine_3 :
  ∀ (j : Fin n) (hj : x ∈ (↑(W j) : Set X)),
    Membership.mem (γ := Set X)
      (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
⊢ Membership.mem (γ := Set X)
    (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x

Tactic:
obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
j : Fin n
hj : x ∈ (↑(W j) : Set X)
⊢ W j ≠ ⊥

Tactic:
simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩

Premises used: SetLike.coe_ne_coe, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
j : Fin n
hj : x ∈ (↑(W j) : Set X)
⊢ W j ≠ ⊥

Tactic:
have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
j : Fin n
hj : x ∈ (↑(W j) : Set X)
this : W j ≠ ⊥
⊢ x ∈
    (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))
          ((t.equivFin : (a : ↥t) → Fin #t) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ t) j ⋯))) :
      Set X)

Tactic:
simpa
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
j : Fin n
hj : x ∈ (↑(W j) : Set X)
this : W j ≠ ⊥
⊢ Membership.mem (γ := Set X)
    (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x

Tactic:
exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.equivFin, Set.mem_iUnion, Subtype.mk, And.intro, Exists.intro, Finset.mem_filter, DFunLike.coe
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
⊢ Pairwise (α := Fin #t)
    (Function.onFun.{1, u_2 + 1, 1} (β := Clopens X) Disjoint fun (k : Fin #t) ↦
      W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))

Tactic:
hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective

Premises used: Finset.equivFin, Subtype.val_injective, Pairwise.comp_of_injective, Function.Injective.comp, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
⊢ Pairwise (α := Fin #t)
    (Function.onFun.{1, u_2 + 1, 1} (β := Clopens X) Disjoint fun (k : Fin #t) ↦
      W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))

Tactic:
exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective

Premises used: Finset.equivFin, Subtype.val_injective, Pairwise.comp_of_injective, Function.Injective.comp, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
⊢ S ∈ 𝓝 (x, x)

Tactic:
have : S ∈ 𝓝 (x, x) := mem_nhdsSet_iff_forall.mp hS _ rfl
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S),
    ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S

Tactic:
rwa [mem_nhds_prod_iff'] at this

Premises used: mem_nhds_prod_iff'
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
obtain :
  ∀ (u v : Set X) (huo : IsOpen[inst] u) (hux : x ∈ u) (hvo : IsOpen[inst] v) (hvx : x ∈ v) (H : u ×ˢ v ⊆ S),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

Tactic:
obtain ⟨u, v, huo, hux, hvo, hvx, H⟩ := by rwa [mem_nhds_prod_iff'] at this
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
u v : Set X
huo : IsOpen[inst] u
hux : x ∈ u
hvo : IsOpen[inst] v
hvx : x ∈ v
H : u ×ˢ v ⊆ S
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

Tactic:
⟨_, huo.inter hvo, ⟨hux, hvx⟩, fun p hp ↦ H ⟨hp.1.1, hp.2.2⟩⟩

Premises used: And.right, And.left, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
u v : Set X
huo : IsOpen[inst] u
hux : x ∈ u
hvo : IsOpen[inst] v
hvx : x ∈ v
H : u ×ˢ v ⊆ S
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

Tactic:
exact ⟨_, huo.inter hvo, ⟨hux, hvx⟩, fun p hp ↦ H ⟨hp.1.1, hp.2.2⟩⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
choose :
  ∀ (U : (x : X) → Set X) (hUo : ∀ (x : X), IsOpen[inst] (U x)) (hUx : ∀ (x : X), x ∈ U x)
    (hUp : ∀ (x : X), U x ×ˢ U x ⊆ S),
    ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S

Tactic:
choose U hUo hUx hUp using exists_open_prod_subset_of_mem_nhds_diagonal hS

Premises used: TopologicalSpace.exists_open_prod_subset_of_mem_nhds_diagonal
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : (x : X) → Set X
hUo : ∀ (x : X), IsOpen[inst] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
obtain :
  ∀ (t : Finset X) (ht : Subset.{u_1} (α := Set X) univ (⋃ i ∈ t, U i)),
    ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S

Tactic:
obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover _ hUo (fun x _ ↦ mem_iUnion.mpr ⟨_, hUx x⟩)

Premises used: Iff.mpr, Set.mem_iUnion, IsCompact.elim_finite_subcover, isCompact_univ, Exists.intro
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : (x : X) → Set X
hUo : ∀ (x : X), IsOpen[inst] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
t : Finset X
ht : Subset.{u_1} (α := Set X) univ (⋃ i ∈ t, U i)
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S

Tactic:
⟨t, fun i ↦ ⟨_, hUo i⟩, .of_sets _ ?_, (hUp ·)⟩

Premises used: TopologicalSpace.Opens.mk, And.intro, Exists.intro, TopologicalSpace.IsOpenCover.of_sets, Subtype.val
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : (x : X) → Set X
hUo : ∀ (x : X), IsOpen[inst] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
t : Finset X
ht : Subset.{u_1} (α := Set X) univ (⋃ i ∈ t, U i)
refine : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ↥t), U (↑i : X)) univ
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S

Tactic:
refine ⟨t, fun i ↦ ⟨_, hUo i⟩, .of_sets _ ?_, (hUp ·)⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : (x : X) → Set X
hUo : ∀ (x : X), IsOpen[inst] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
t : Finset X
ht : Subset.{u_1} (α := Set X) univ (⋃ i ∈ t, U i)
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (i : ↥t), U (↑i : X)) univ

Tactic:
simpa [iUnion_subtype, ← univ_subset_iff] using ht

Premises used: Set.univ_subset_iff, Set.iUnion_subtype
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
obtain :
  ∀ (t : Finset X) (U : ↥t → Opens X) (hUc : IsOpenCover U)
    (hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S),
    ∃ (n : ℕ) (D : Fin n → Clopens X),
      (∀ (i : Fin n), D i ≠ ⊥) ∧
        (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
          Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)

Tactic:
obtain ⟨t, U, hUc, hUS⟩ := exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact hS

Premises used: TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
obtain :
  ∀ (n : ℕ) (W : Fin n → Clopens X) (hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X))
    (hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))) (hW₃ : Pairwise (Disjoint on W)),
    ∃ (n : ℕ) (D : Fin n → Clopens X),
      (∀ (i : Fin n), D i ≠ ⊥) ∧
        (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
          Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)

Tactic:
obtain ⟨n, W, hW₁, hW₂, hW₃⟩ := hUc.exists_finite_nonempty_disjoint_clopen_cover

Premises used: TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)
hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))
hW₃ : Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)

Tactic:
⟨n, W, fun j ↦ (hW₁ j).1, fun j y hy z hz ↦ ?_, hW₂, hW₃⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)
hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))
hW₃ : Pairwise (Disjoint on W)
refine : ∀ (j : Fin n) (y : X) (hy : y ∈ W j) (z : X) (hz : z ∈ W j), (y, z) ∈ S
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)

Tactic:
refine ⟨n, W, fun j ↦ (hW₁ j).1, fun j y hy z hz ↦ ?_, hW₂, hW₃⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)
hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))
hW₃ : Pairwise (Disjoint on W)
j : Fin n
y : X
hy : y ∈ W j
z : X
hz : z ∈ W j
⊢ (y, z) ∈ S

Tactic:
match (hW₁ j).2 with | ⟨i, hi⟩ => hUS i ⟨hi hy, hi hz⟩

Premises used: Membership.mem, Prod.mk, _private.0.TopologicalSpace.exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite.match_1, And.right, And.intro
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)
hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))
hW₃ : Pairwise (Disjoint on W)
j : Fin n
y : X
hy : y ∈ W j
z : X
hz : z ∈ W j
⊢ (y, z) ∈ S

Tactic:
exact match (hW₁ j).2 with | ⟨i, hi⟩ => hUS i ⟨hi hy, hi hz⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
rw : ∀ (hS : ∀ x ∈ diagonal V, S ∈ 𝓝 x), ∀ x ∈ diagonal X, (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝 x
⊢ (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝ˢ (diagonal X)

Tactic:
rw [mem_nhdsSet_iff_forall] at hS ⊢

Premises used: mem_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : ∀ x ∈ diagonal V, S ∈ 𝓝 x
x : X
⊢ (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝 (x, x)

Tactic:
(map_continuous _).continuousAt.preimage_mem_nhds (hS _ rfl)

Premises used: Set.Mem, ContinuousAt.preimage_mem_nhds, Continuous.continuousAt, ContinuousMapClass.map_continuous, rfl
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : ∀ x ∈ diagonal V, S ∈ 𝓝 x
x : X
⊢ (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝 (x, x)

Tactic:
exact (map_continuous _).continuousAt.preimage_mem_nhds (hS _ rfl)

Premises used: ContinuousAt.preimage_mem_nhds, Continuous.continuousAt, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝ˢ (diagonal X)

Tactic:
have : (f.prodMap f) ⁻¹' S ∈ nhdsSet (diagonal X) := by
    rw [mem_nhdsSet_iff_forall] at hS ⊢
    rintro ⟨x, y⟩ (rfl : x = y)
    exact (map_continuous _).continuousAt.preimage_mem_nhds (hS _ rfl)
-- Module: Mathlib.Topology.Separation.DisjointCover
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
this : (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n),
          ∀ y ∈ D i, ∀ z ∈ D i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)

Tactic:
exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite this

Premises used: Set.Mem, setOf, Prod.map, _private.0.TopologicalSpace.exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite, Set.preimage