awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hf : Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ
hfc : Continuous[inst, _] f
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hf₀ : f x = 0
Tactic: obtain ⟨hfc, hf₀, hf₁⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hf : Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ
hfc : Continuous[inst, _] f
hf₀ : f x = 0
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hf₁ : EqOn f 1 sᶜ
Tactic: obtain ⟨hfc, hf₀, hf₁⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hR : lift.{u, 0} #(↑R : Type) < lift.{0, u} 𝔠
Tactic: have hR : lift.{u, 0} (Cardinal.mk R) < lift.{0, u} continuum := by
    simpa [R] using mk_range_le_lift.trans_lt (lift_strictMono hX)
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : lift.{u, 0} #(↑R : Type) < lift.{0, u} 𝔠
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hR₁ : #(↑R : Type) < #(↑I : Type)
Tactic: rw [lift_continuum, ← lift_continuum.{u, 0}, lift_lt, ← mk_Icc_real zero_lt_one, ← unitInterval]
    at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have obtain : ∀ (r : (↑I : Type)) (hr : r ∈ Rᶜ),
  ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
Tactic: obtain ⟨r, hr⟩ : ∃ r : I, r ∈ Rᶜ := compl_nonempty_of_mk_lt_mk hR
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hr' : ∀ (x : X), f x ≠ r
Tactic: have hr' : ∀ (x : X), f x ≠ r := by simpa [R] using hr
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
⊢ f ⁻¹' Iio r = f ⁻¹' Iic r
have h : ∀ (x : X), x ∈ f ⁻¹' Iio r ↔ x ∈ f ⁻¹' Iic r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
Tactic: have hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r := by
    ext; simp [le_iff_lt_or_eq, hr']
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have refine_1 : x ∈ f ⁻¹' Iio r
Tactic: refine ⟨f ⁻¹' Iio r, ⟨hrclopen ▸ isClosed_Iic.preimage hfc, isOpen_Iio.preimage hfc⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
refine_1 : x ∈ f ⁻¹' Iio r
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have refine_2 : f ⁻¹' Iio r ⊆ s
Tactic: refine ⟨f ⁻¹' Iio r, ⟨hrclopen ▸ isClosed_Iic.preimage hfc, isOpen_Iio.preimage hfc⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ f ⁻¹' Iio r ⊆ s
have refine_2 : ∀ (x : X), f x ∈ Iio r → x ∈ s
Tactic: refine preimage_subset_iff.mpr (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x_1 : X
s : Set X
hxs : x_1 ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x_1 = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
x : X
⊢ f x ∈ Iio r → x ∈ s
have refine_2 : x ∉ s → f x ∉ Iio r
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ (f : X → ℝ), Membership.mem (γ := Set (X → ℝ)) {f : X → ℝ | Continuous[inst, _] f} f ∧ f x ≠ f y
have obtain : ∀ (f : X → (↑I : Type)) (f_cont : Continuous[inst, _] f) (f_zero : f x = 0) (f_one : EqOn f 1 {y}),
  ∃ (f : X → ℝ), Membership.mem (γ := Set (X → ℝ)) {f : X → ℝ | Continuous[inst, _] f} f ∧ f x ≠ f y
Tactic: obtain ⟨f, f_cont, f_zero, f_one⟩ :=
    CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ (f : X → (↑I : Type)),
    Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f ∧ f x ≠ f y
have obtain : ∀ (f : X → (↑I : Type)) (f_cont : Continuous[inst, _] f) (f_zero : f x = 0) (f_one : EqOn f 1 {y}),
  ∃ (f : X → (↑I : Type)),
    Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f ∧ f x ≠ f y
Tactic: obtain ⟨f, f_cont, f_zero, f_one⟩ :=
    CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
a b : X
hab : Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
⊢ a = b
have contrapose : ∀ (hab : ¬a = b), ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
Tactic: contrapose hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
a b : X
hab : ¬a = b
⊢ ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
have obtain : ∀ (f : X → (↑I : Type))
  (fc : Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f) (fab : f a ≠ f b),
  ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
Tactic: obtain ⟨f, fc, fab⟩ := separatesPoints_continuous_of_t35Space_Icc hab
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : TotallyDisconnectedSpace X
⊢ T1Space X
have rw : ∀ (x : X), IsClosed[inst] {x}
Tactic: rw [((t1Space_TFAE X).out 0 1 :)]
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : TotallyDisconnectedSpace X
x : X
⊢ IsClosed[inst] {x}
have rw : IsClosed[inst] (connectedComponent x)
Tactic: rw [← totallyDisconnectedSpace_iff_connectedComponent_singleton.mp h x]
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : DiscreteTopology X
⊢ Subsingleton X
have by_contra! : ∀ (x y : X) (hxy : x ≠ y), False
Tactic: by_contra! ⟨x, y, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PreconnectedSpace X
inst_2 : DiscreteTopology X
x y : X
hxy : x ≠ y
⊢ False
have hxy₁ : x ∉ univ
Tactic: rw [Ne, ← mem_singleton_iff, (isClopen_discrete _).eq_univ <| singleton_nonempty y] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
⊢ s.Infinite
have refine : ∀ (hf : s.Finite), Subsingleton.{u_1 + 1} (↑s : Type u_1)
Tactic: refine mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
⊢ Subsingleton.{u_1 + 1} (↑s : Type u_1)
have this : DiscreteTopology.{u_1} (↑s : Type u_1)
Tactic: haveI := @Finite.instDiscreteTopology s _ _ hf.to_subtype
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ConnectedSpace X
inst_2 : Nontrivial X
inst_3 : T1Space X
x : X
⊢ (𝓝[≠] x).NeBot
have by_contra : ∀ (contra : ¬(𝓝[≠] x).NeBot), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (hypothesis)
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
⊢ False
have contra₁ : IsOpen[inst] {x}
Tactic: rw [not_neBot, ← isOpen_singleton_iff_punctured_nhds] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Topology.Separation.Connected (hypothesis)
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}
⊢ False
have contra₁ : Set.Nonempty (α := X) ({x}ᶜ ∩ {x})
Tactic: replace contra := nonempty_inter isOpen_compl_singleton
    contra (compl_union_self _) (Set.nonempty_compl_of_nontrivial _) (singleton_nonempty _)
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Topology.Separation.CountableSeparatingOn (goal)
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 X IsOpen s
have suffices : HasCountableSeparatingOn.{u_1} (↑s : Type u_1) IsOpen univ
Tactic: suffices HasCountableSeparatingOn s IsOpen univ from .of_subtype fun _ ↦ isOpen_induced_iff.1
-- Lean 4 proof step from Mathlib.Topology.Separation.CountableSeparatingOn (goal)
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
have 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
Tactic: refine ⟨⟨countableBasis s, countable_countableBasis _, fun _ ↦ isOpen_of_mem_countableBasis,
    fun x _ y _ h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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),
    (∀ (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))
have 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))
Tactic: choose r hr using hU.exists_mem
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: choose V hV hVx hVU using fun x ↦ compact_exists_isClopen_in_isOpen (U _).isOpen (hr x)
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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)
⊢ ∃ (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))
have 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))
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⟩)
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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))
have 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' := sorry : Clopens X })
            j) :
        Set X))
    x
Tactic: refine ⟨_, fun j ↦ ⟨_, hV (t.equivFin.symm j)⟩, fun j ↦ ⟨_, hVU _⟩, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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
⊢ 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
have 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' := sorry : Clopens X })
            j) :
        Set X))
    x
Tactic: obtain ⟨m, hm, hm'⟩ := mem_iUnion₂.mp (ht hx)
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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 : ℕ) (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)
have 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)
Tactic: obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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))
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (hypothesis)
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)
⊢ ∃ (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)
have hWun₁ : 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
Cleared hypotheses: hWun
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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)
have 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) ⊥
Tactic: refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
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) ⊥
⊢ ∃ (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)
have 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)
Tactic: refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩