awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
h : TotallyDisconnectedSpace X
rw : ∀ (x : X), IsClosed[inst] {x}
⊢ T1Space X

Tactic:
rw [((t1Space_TFAE X).out 0 1 :)]

Premises used: t1Space_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
h : TotallyDisconnectedSpace X
x : X
rw : IsClosed[inst] (connectedComponent x)
⊢ IsClosed[inst] {x}

Tactic:
rw [← totallyDisconnectedSpace_iff_connectedComponent_singleton.mp h x]

Premises used: totallyDisconnectedSpace_iff_connectedComponent_singleton, Iff.mp
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
h : TotallyDisconnectedSpace X
x : X
⊢ IsClosed[inst] (connectedComponent x)

Tactic:
isClosed_connectedComponent

Premises used: isClosed_connectedComponent
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
h : TotallyDisconnectedSpace X
x : X
⊢ IsClosed[inst] (connectedComponent x)

Tactic:
exact isClosed_connectedComponent

Premises used: isClosed_connectedComponent
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : DiscreteTopology X
by_contra! : ∀ (x y : X) (hxy : x ≠ y), False
⊢ Subsingleton X

Tactic:
by_contra! ⟨x, y, hxy⟩
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : DiscreteTopology X
x y : X
hxy : x ≠ y
⊢ x ∉ univ

Tactic:
rw [Ne, ← mem_singleton_iff, (isClopen_discrete _).eq_univ <| singleton_nonempty y] at hxy

Premises used: Set.singleton_nonempty, isClopen_discrete, Ne, IsClopen.eq_univ, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : DiscreteTopology X
x y : X
hxy : x ∉ univ
⊢ False

Tactic:
hxy (mem_univ x)

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : DiscreteTopology X
x y : X
hxy : x ∉ univ
⊢ False

Tactic:
exact hxy (mem_univ x)

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
⊢ s.Infinite

Tactic:
mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)

Premises used: Set.not_subsingleton_iff, Iff.mpr, mt, Iff.mp, Set.subsingleton_coe, Set.Infinite
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
refine : ∀ (hf : s.Finite), Subsingleton.{u_1 + 1} (↑s : Type u_1)
⊢ s.Infinite

Tactic:
refine mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)

Premises used: Set.not_subsingleton_iff, Iff.mpr, mt, Iff.mp, Set.subsingleton_coe
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
⊢ DiscreteTopology.{u_1} (↑s : Type u_1)

Tactic:
haveI := @Finite.instDiscreteTopology s _ _ hf.to_subtype
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
this : DiscreteTopology.{u_1} (↑s : Type u_1)
⊢ Subsingleton.{u_1 + 1} (↑s : Type u_1)

Tactic:
@PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _

Premises used: PreconnectedSpace.trivial_of_discrete
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
this : DiscreteTopology.{u_1} (↑s : Type u_1)
⊢ Subsingleton.{u_1 + 1} (↑s : Type u_1)

Tactic:
exact @PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _

Premises used: PreconnectedSpace.trivial_of_discrete
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : Nontrivial X
inst_3 : T1Space X
⊢ Infinite X

Tactic:
infinite_univ_iff.mp <| isPreconnected_univ.infinite_of_nontrivial nontrivial_univ

Premises used: IsPreconnected.infinite_of_nontrivial, Iff.mp, PreconnectedSpace.isPreconnected_univ, Set.nontrivial_univ, Set.infinite_univ_iff
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Subsingleton X ↔ DiscreteTopology X ∧ IndiscreteTopology X

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ PreconnectedSpace.trivial_of_discrete⟩

Premises used: inferInstance, And.intro, Iff.intro, Subsingleton, PreconnectedSpace.trivial_of_discrete, _private.0.subsingleton_iff_discrete_and_indiscrete.match_1
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ConnectedSpace X
inst_2 : Nontrivial X
inst_3 : T1Space X
x : X
by_contra : ∀ (contra : ¬(𝓝[≠] x).NeBot), False
⊢ (𝓝[≠] x).NeBot

Tactic:
by_contra contra
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ConnectedSpace X
inst_2 : Nontrivial X
inst_3 : T1Space X
x : X
contra : ¬(𝓝[≠] x).NeBot
⊢ IsOpen[inst] {x}

Tactic:
rw [not_neBot, ← isOpen_singleton_iff_punctured_nhds] at contra

Premises used: isOpen_singleton_iff_punctured_nhds, Filter.not_neBot
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ConnectedSpace X
inst_2 : Nontrivial X
inst_3 : T1Space X
x : X
contra : IsOpen[inst] {x}
⊢ Set.Nonempty (α := X) ({x}ᶜ ∩ {x})

Tactic:
replace contra := nonempty_inter isOpen_compl_singleton
    contra (compl_union_self _) (Set.nonempty_compl_of_nontrivial _) (singleton_nonempty _)
-- Module: Mathlib.Topology.Separation.Connected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ConnectedSpace X
inst_2 : Nontrivial X
inst_3 : T1Space X
x : X
contra : Set.Nonempty (α := X) ({x}ᶜ ∩ {x})
⊢ False

Tactic:
simp [compl_inter_self {x}] at contra

Premises used: Set.compl_inter_self, Singleton.singleton
-- Module: Mathlib.Topology.Separation.CountableSeparatingOn
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T0Space.{u_1} (↑s : Type u_1)
inst_2 : SecondCountableTopology.{u_1} (↑s : Type u_1)
suffices : HasCountableSeparatingOn.{u_1} (↑s : Type u_1) IsOpen univ
⊢ HasCountableSeparatingOn X IsOpen s

Tactic:
suffices HasCountableSeparatingOn s IsOpen univ from .of_subtype fun _ ↦ isOpen_induced_iff.1
-- Module: Mathlib.Topology.Separation.CountableSeparatingOn
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T0Space.{u_1} (↑s : Type u_1)
inst_2 : SecondCountableTopology.{u_1} (↑s : Type u_1)
⊢ HasCountableSeparatingOn.{u_1} (↑s : Type u_1) IsOpen univ

Tactic:
⟨⟨countableBasis s, countable_countableBasis _, fun _ ↦ isOpen_of_mem_countableBasis,
    fun x _ y _ h ↦ ?_⟩⟩

Premises used: TopologicalSpace.countableBasis, TopologicalSpace.countable_countableBasis, Set.Elem, And.intro, HasCountableSeparatingOn.mk, Exists.intro, TopologicalSpace.isOpen_of_mem_countableBasis
-- Module: Mathlib.Topology.Separation.CountableSeparatingOn
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T0Space.{u_1} (↑s : Type u_1)
inst_2 : SecondCountableTopology.{u_1} (↑s : Type u_1)
refine :
  ∀ (x : (↑s : Type u_1)),
    Membership.mem (γ := Set (↑s : Type u_1)) univ x →
      ∀ (y : (↑s : Type u_1)),
        Membership.mem (γ := Set (↑s : Type u_1)) univ y →
          ∀
            (h :
              ∀ (s_1 : Set (↑s : Type u_1)),
                Membership.mem (γ := Set (Set (↑s : Type u_1))) (countableBasis (↑s : Type u_1)) s_1 →
                  (x ∈ s_1 ↔ y ∈ s_1)),
            x = y
⊢ HasCountableSeparatingOn.{u_1} (↑s : Type u_1) IsOpen univ

Tactic:
refine ⟨⟨countableBasis s, countable_countableBasis _, fun _ ↦ isOpen_of_mem_countableBasis,
    fun x _ y _ h ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Separation.CountableSeparatingOn
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T0Space.{u_1} (↑s : Type u_1)
inst_2 : SecondCountableTopology.{u_1} (↑s : Type u_1)
x : (↑s : Type u_1)
h_1 : Membership.mem (γ := Set (↑s : Type u_1)) univ x
y : (↑s : Type u_1)
h_2 : Membership.mem (γ := Set (↑s : Type u_1)) univ y
h :
  ∀ (s_1 : Set (↑s : Type u_1)),
    Membership.mem (γ := Set (Set (↑s : Type u_1))) (countableBasis (↑s : Type u_1)) s_1 → (x ∈ s_1 ↔ y ∈ s_1)
⊢ x = y

Tactic:
((isBasis_countableBasis _).inseparable_iff.2 h).eq

Premises used: Iff.mpr, Inseparable.eq, TopologicalSpace.IsTopologicalBasis.inseparable_iff, TopologicalSpace.isBasis_countableBasis
-- Module: Mathlib.Topology.Separation.CountableSeparatingOn
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T0Space.{u_1} (↑s : Type u_1)
inst_2 : SecondCountableTopology.{u_1} (↑s : Type u_1)
x : (↑s : Type u_1)
h_1 : Membership.mem (γ := Set (↑s : Type u_1)) univ x
y : (↑s : Type u_1)
h_2 : Membership.mem (γ := Set (↑s : Type u_1)) univ y
h :
  ∀ (s_1 : Set (↑s : Type u_1)),
    Membership.mem (γ := Set (Set (↑s : Type u_1))) (countableBasis (↑s : Type u_1)) s_1 → (x ∈ s_1 ↔ y ∈ s_1)
⊢ x = y

Tactic:
exact ((isBasis_countableBasis _).inseparable_iff.2 h).eq

Premises used: Iff.mpr, Inseparable.eq, TopologicalSpace.IsTopologicalBasis.inseparable_iff, TopologicalSpace.isBasis_countableBasis
-- Module: Mathlib.Topology.Separation.CountableSeparatingOn
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : HasCountableSeparatingOn X IsOpen s
⊢ HasCountableSeparatingOn X IsClosed s

Tactic:
let ⟨S, hSc, hSo, hS⟩ := h.1
  ⟨compl '' S, hSc.image _, forall_mem_image.2 fun U hU ↦ (hSo U hU).isClosed_compl,
    fun x hx y hy h ↦ hS x hx y hy fun _U hU ↦ not_iff_not.1 <| h _ (mem_image_of_mem _ hU)⟩

Premises used: not_iff_not, Iff.mpr, _private.0.instHasCountableSeparatingOnIsClosedOfIsOpen.match_1, Compl.compl, Set.Countable.image, IsOpen.isClosed_compl, IsClosed, Set.mem_image_of_mem, And.intro, HasCountableSeparatingOn, HasCountableSeparatingOn.mk, Exists.intro, Iff.mp, HasCountableSeparatingOn.exists_countable_separating, Set.image, Set.forall_mem_image
-- 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
choose :
  ∀ (r : (a : X) → ι) (hr : ∀ (a : X), a ∈ U (r a)),
    ∃ (n : ℕ) (V : Fin n → Clopens X),
      (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
⊢ ∃ (n : ℕ) (V : Fin n → Clopens X),
    (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))

Tactic:
choose r hr using hU.exists_mem

Premises used: TopologicalSpace.IsOpenCover.exists_mem
-- 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
choose :
  ∀ (V : (x : X) → Set X) (hV : ∀ (x : X), IsClopen (V x)) (hVx : ∀ (x : X), x ∈ V x)
    (hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)),
    ∃ (n : ℕ) (V : Fin n → Clopens X),
      (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
⊢ ∃ (n : ℕ) (V : Fin n → Clopens X),
    (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))

Tactic:
choose V hV hVx hVU using fun x ↦ compact_exists_isClopen_in_isOpen (U _).isOpen (hr x)

Premises used: TopologicalSpace.Opens.isOpen, compact_exists_isClopen_in_isOpen
-- 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
⊢ ∃ (t : Finset X), Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)

Tactic:
isCompact_univ.elim_finite_subcover V (fun x ↦ (hV x).2) (fun x _ ↦ mem_iUnion.mpr ⟨x, hVx x⟩)

Premises used: Iff.mpr, Set.mem_iUnion, IsCompact.elim_finite_subcover, And.right, isCompact_univ, Exists.intro
-- 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
obtain :
  ∀ (t : Finset X) (ht : Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)),
    ∃ (n : ℕ) (V : Fin n → Clopens X),
      (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
⊢ ∃ (n : ℕ) (V : Fin n → Clopens X),
    (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))

Tactic:
obtain ⟨t, ht⟩ : ∃ t, univ ⊆ ⋃ i ∈ t, V i :=
    isCompact_univ.elim_finite_subcover V (fun x ↦ (hV x).2) (fun x _ ↦ mem_iUnion.mpr ⟨x, hVx x⟩)

Premises used: Iff.mpr, Set.univ, Set.mem_iUnion, IsCompact.elim_finite_subcover, And.right, isCompact_univ, Exists.intro
-- 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
t : Finset X
ht : Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)
⊢ ∃ (n : ℕ) (V : Fin n → Clopens X),
    (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))

Tactic:
⟨_, fun j ↦ ⟨_, hV (t.equivFin.symm j)⟩, fun j ↦ ⟨_, hVU _⟩, fun x hx ↦ ?_⟩

Premises used: Finset.equivFin, And.intro, TopologicalSpace.Clopens.mk, Exists.intro, Equiv.symm, Subtype.val, 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
t : Finset X
ht : Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)
refine :
  ∀ (x : X) (hx : Membership.mem (γ := Set X) univ x),
    Membership.mem (γ := Set X)
      (⋃ (j : Fin #t),
        (↑((fun (j : Fin #t) ↦
                { carrier := V (↑((t.equivFin.symm : (a : Fin #t) → ↥t) j) : X), isClopen' := ⋯ : Clopens X })
              j) :
          Set X))
      x
⊢ ∃ (n : ℕ) (V : Fin n → Clopens X),
    (∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))

Tactic:
refine ⟨_, fun j ↦ ⟨_, hV (t.equivFin.symm j)⟩, fun j ↦ ⟨_, hVU _⟩, fun x hx ↦ ?_⟩
-- 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
t : Finset X
ht : Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)
x : X
hx : Membership.mem (γ := Set X) univ x
obtain :
  ∀ (m : X) (hm : m ∈ t) (hm' : x ∈ V m),
    Membership.mem (γ := Set X)
      (⋃ (j : Fin #t),
        (↑((fun (j : Fin #t) ↦
                { carrier := V (↑((t.equivFin.symm : (a : Fin #t) → ↥t) j) : X), isClopen' := ⋯ : Clopens X })
              j) :
          Set X))
      x
⊢ Membership.mem (γ := Set X)
    (⋃ (j : Fin #t),
      (↑((fun (j : Fin #t) ↦
              { carrier := V (↑((t.equivFin.symm : (a : Fin #t) → ↥t) j) : X), isClopen' := ⋯ : Clopens X })
            j) :
        Set X))
    x

Tactic:
obtain ⟨m, hm, hm'⟩ := mem_iUnion₂.mp (ht 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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
t : Finset X
ht : Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)
x : X
hx : Membership.mem (γ := Set X) univ x
m : X
hm : m ∈ t
hm' : x ∈ V m
⊢ x ∈
    (↑((fun (j : Fin #t) ↦
            { carrier := V (↑((t.equivFin.symm : (a : Fin #t) → ↥t) j) : X), isClopen' := ⋯ : Clopens X })
          ((t.equivFin : (a : ↥t) → Fin #t) (Subtype.mk (p := fun (x : X) ↦ x ∈ t) m hm))) :
      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
r : (a : X) → ι
hr : ∀ (a : X), a ∈ U (r a)
V : (x : X) → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ (↑(U (r x)) : Set X)
t : Finset X
ht : Subset.{u_2} (α := Set X) univ (⋃ i ∈ t, V i)
x : X
hx : Membership.mem (γ := Set X) univ x
m : X
hm : m ∈ t
hm' : x ∈ V m
⊢ Membership.mem (γ := Set X)
    (⋃ (j : Fin #t),
      (↑((fun (j : Fin #t) ↦
              { carrier := V (↑((t.equivFin.symm : (a : Fin #t) → ↥t) j) : X), isClopen' := ⋯ : Clopens X })
            j) :
        Set X))
    x

Tactic:
exact Set.mem_iUnion_of_mem (t.equivFin ⟨m, hm⟩) (by simpa)

Premises used: Finset.equivFin, Subtype.mk, Set.mem_iUnion_of_mem, 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
obtain :
  ∀ (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))),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)

Tactic:
obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover

Premises used: TopologicalSpace.IsOpenCover.exists_finite_clopen_cover
-- 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))
obtain :
  ∀ (W : Fin n → Clopens X) (hWle : W ≤ V) (hWun : Finset.sup Finset.univ W = Finset.sup Finset.univ V)
    (hWd : Pairwise (Disjoint on W)),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)

Tactic:
obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V

Premises used: Fintype.exists_disjointed_le
-- 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
hWun : Finset.sup Finset.univ W = Finset.sup Finset.univ V
hWd : Pairwise (Disjoint on W)
⊢ Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))

Tactic:
simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun

Premises used: Finset.mem_univ, TopologicalSpace.Clopens.coe_finset_sup, Set.iUnion_true, SetLike.coe_set_eq
-- 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 ≠ ⊥}
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)

Tactic:
⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩

Premises used: Finset.equivFin, And.intro, Exists.intro, Finset.card, Equiv.symm, Subtype.val, 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 ≠ ⊥}
refine_1 :
  ∀ (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) ⊥
refine_2 :
  ∀ (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)
refine_3 :
  ∀ (x : X) (hx : Membership.mem (γ := Set X) univ 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
refine_4 :
  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))
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)

Tactic:
refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩