awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have rcases : ∀ (I : Finset (X × Y)) (hIW : ∀ x ∈ I, x ∈ W.carrier) (hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)),
  ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
Tactic: rcases W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
    (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have h : W =
  Finset.sup (Finset.image (fun (x : X × Y) ↦ (U x, V x)) I) fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦
    i.1 ×ˢ i.2
Tactic: use I.image fun x ↦ (U x, V x)
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
⊢ W =
    Finset.sup (Finset.image (fun (x : X × Y) ↦ (U x, V x)) I) fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦
      i.1 ×ˢ i.2
have h : W = I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))
Tactic: rw [Finset.sup_image]
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
⊢ W = I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))
have h : ∀ (x : X × Y) (hx : x ∈ W),
  Membership.mem (γ := Clopens (X × Y))
    (I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
h :
  ∀ (x : X × Y) (hx : x ∈ W),
    Membership.mem (γ := Clopens (X × Y))
      (I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))) x
⊢ W = I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))
have h₁ : ∀ (x : X × Y) (hx : x ∈ I),
  ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x)) x ≤ W
Tactic: refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
x : X × Y
hx : x ∈ W
⊢ Membership.mem (γ := Clopens (X × Y))
    (I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))) x
have h : ∀ (i : X × Y) (hi : i ∈ I) (hxi : x ∈ (↑(U i) : Set X) ×ˢ (↑(V i) : Set Y)),
  Membership.mem (γ := Clopens (X × Y))
    (I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))) x
Tactic: rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have w : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))
Tactic: classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
w : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have h : W =
  Finset.sup (Finset.image (fun (x : X × Y) ↦ (U x, V x)) I) fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦
    i.1 ×ˢ i.2
Tactic: classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
w : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))
h h₁ :
  W =
    Finset.sup (Finset.image (fun (x : X × Y) ↦ (U x, V x)) I) fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦
      i.1 ×ˢ i.2
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have h₂ : W = I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))
Tactic: classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
w : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))
h h₁ :
  W =
    Finset.sup (Finset.image (fun (x : X × Y) ↦ (U x, V x)) I) fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦
      i.1 ×ˢ i.2
h₂ : W = I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have h₃ : ∀ (x : X × Y) (hx : x ∈ W),
  Membership.mem (γ := Clopens (X × Y))
    (I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))) x
Tactic: classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
U : (x : X × Y) → Clopens X
hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x
V : (x : X × Y) → Clopens Y
hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x
hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W
I : Finset (X × Y)
hIW : ∀ x ∈ I, x ∈ W.carrier
hWI : W.carrier ⊆ ⋃ x ∈ I, (↑(U x) : Set X) ×ˢ (↑(V x) : Set Y)
w : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))
h h₁ :
  W =
    Finset.sup (Finset.image (fun (x : X × Y) ↦ (U x, V x)) I) fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦
      i.1 ×ˢ i.2
h₂ : W = I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))
h₃ :
  ∀ (x : X × Y) (hx : x ∈ W),
    Membership.mem (γ := Clopens (X × Y))
      (I.sup ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x))) x
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have h₄ : ∀ (x : X × Y) (hx : x ∈ I),
  ((fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2) ∘ fun (x : X × Y) ↦ (U x, V x)) x ≤ W
Tactic: classical
  use I.image fun x ↦ (U x, V x)
  rw [Finset.sup_image]
  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
  · exact hUV _ <| hIW _ hx
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
inst_4 : Finite.{u_1 + 1} (Clopens X)
inst_5 : Finite.{u_2 + 1} (Clopens Y)
⊢ Finite (Clopens (X × Y))
have intro : ∀ (val : Fintype (Clopens X)), Finite (Clopens (X × Y))
Tactic: cases nonempty_fintype (Clopens X)
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
inst_4 : Finite.{u_1 + 1} (Clopens X)
inst_5 : Finite.{u_2 + 1} (Clopens Y)
val : Fintype (Clopens X)
⊢ Finite (Clopens (X × Y))
have intro : ∀ (val : Fintype (Clopens Y)), Finite (Clopens (X × Y))
Tactic: cases nonempty_fintype (Clopens Y)
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
⊢ Countable.{u_1 + 1} (Clopens X) ↔ SecondCountableTopology X
have refine_1 : ∀ (h : Countable.{u_1 + 1} (Clopens X)), Set.Countable.{u_1} (α := Set X) {s : Set X | IsClopen s}
Tactic: refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
refine_1 : ∀ (h : Countable.{u_1 + 1} (Clopens X)), Set.Countable.{u_1} (α := Set X) {s : Set X | IsClopen s}
⊢ Countable.{u_1 + 1} (Clopens X) ↔ SecondCountableTopology X
have refine_2 : ∀ (h : Countable.{u_1 + 1} (Clopens X)), inst = generateFrom {s : Set X | IsClopen s}
Tactic: refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
refine_1 : ∀ (h : Countable.{u_1 + 1} (Clopens X)), Set.Countable.{u_1} (α := Set X) {s : Set X | IsClopen s}
refine_2 : ∀ (h : Countable.{u_1 + 1} (Clopens X)), inst = generateFrom {s : Set X | IsClopen s}
⊢ Countable.{u_1 + 1} (Clopens X) ↔ SecondCountableTopology X
have refine_3 : ∀ (h : SecondCountableTopology X), Countable.{u_1 + 1} (Clopens X)
Tactic: refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : Countable.{u_1 + 1} (Clopens X)
⊢ inst = generateFrom {s : Set X | IsClopen s}
have refine_2 : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
Tactic: apply IsTopologicalBasis.eq_generateFrom
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable.{u_1 + 1} (Clopens X)
have this : ∀ (s : Clopens X),
  ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
    s.carrier =
      ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
Tactic: have : ∀ (s : Clopens X), ∃ (t : Finset (countableBasis X)), s.1 = (SetLike.coe t).sUnion :=
      fun s ↦ eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _
        (isBasis_countableBasis X) s.1 s.2.1.isCompact s.2.2
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h_1 : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
s t : Clopens X
h :
  ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))) =
    ⋯.choose (p := fun (t_1 : Finset (↑(countableBasis X) : Type u_1)) ↦
      t.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t_1 : Set (↑(countableBasis X) : Type u_1))))
⊢ s = t
have h₁ : (↑s : Set X) = (↑t : Set X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h_1 : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
s t : Clopens X
h :
  ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))) =
    ⋯.choose (p := fun (t_1 : Finset (↑(countableBasis X) : Type u_1)) ↦
      t.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t_1 : Set (↑(countableBasis X) : Type u_1))))
⊢ s.carrier = t.carrier
have h₁ : ⋃₀
    (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
      (↑(sorry.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
            s.carrier =
              ⋃₀
                (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
                  (↑t : Set (↑(countableBasis X) : Type u_1))))) :
        Set (↑(countableBasis X) : Type u_1))) =
  t.carrier
Tactic: rw [(this s).choose_spec, (this t).choose_spec, h]
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h_1 : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
s t : Clopens X
h :
  ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))) =
    ⋯.choose (p := fun (t_1 : Finset (↑(countableBasis X) : Type u_1)) ↦
      t.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t_1 : Set (↑(countableBasis X) : Type u_1))))
h₁ :
  ⋃₀
      (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
        (↑(⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
              s.carrier =
                ⋃₀
                  (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
                    (↑t : Set (↑(countableBasis X) : Type u_1))))) :
          Set (↑(countableBasis X) : Type u_1))) =
    t.carrier
⊢ s.carrier = t.carrier
have h₂ : ⋃₀
    (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
      (↑(sorry.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
            s.carrier =
              ⋃₀
                (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
                  (↑t : Set (↑(countableBasis X) : Type u_1))))) :
        Set (↑(countableBasis X) : Type u_1))) =
  ⋃₀
    (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
      (↑(sorry.choose (p := fun (t_1 : Finset (↑(countableBasis X) : Type u_1)) ↦
            t.carrier =
              ⋃₀
                (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
                  (↑t_1 : Set (↑(countableBasis X) : Type u_1))))) :
        Set (↑(countableBasis X) : Type u_1)))
Tactic: rw [(this s).choose_spec, (this t).choose_spec, h]
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
⊢ Countable.{u_1 + 1} (Clopens X)
have hf : Injective f
Tactic: have hf : f.Injective := by
      intro s t (h : Exists.choose _ = Exists.choose _)
      ext1; change s.carrier = t.carrier
      rw [(this s).choose_spec, (this t).choose_spec, h]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s, f i)) (⋂ i ∈ s, interior (f i))
have empty : Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), f i))
  (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), interior (f i))
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ _ => simp [*]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Set ι
hs : s.Finite
f : ι → Set X
empty :
  Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), f i))
    (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), interior (f i))
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s, f i)) (⋂ i ∈ s, interior (f i))
have insert : ∀ {a : ι} {s : Set ι},
  a ∉ s →
    s.Finite →
      Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s, f i)) (⋂ i ∈ s, interior (f i)) →
        Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ insert a s, f i)) (⋂ i ∈ insert a s, interior (f i))
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ _ => simp [*]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s
have rw : Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ S, i)) (⋂ s ∈ S, interior s)
Tactic: rw [sInter_eq_biInter, hS.interior_biInter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
rw : Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ S, i)) (⋂ s ∈ S, interior s)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s
have rw₁ : Eq.{u + 1} (α := Set X) (⋂ i ∈ S, interior i) (⋂ s ∈ S, interior s)
Tactic: rw [sInter_eq_biInter, hS.interior_biInter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), f i)) (⋂ (i : ι), interior (f i))
have rw : interior (⋂₀ range f) = ⋂ (i : ι), interior (f i)
Tactic: rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]