awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Clopen
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ IsClopen (X := Sigma X) (range (Sigma.mk (β := X) i))

Tactic:
⟨IsClosedEmbedding.sigmaMk.isClosed_range, IsOpenEmbedding.sigmaMk.isOpen_range⟩

Premises used: Topology.IsClosedEmbedding.sigmaMk, Topology.IsOpenEmbedding.isOpen_range, And.intro, Topology.IsOpenEmbedding.sigmaMk, IsClopen, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap f
s : Set Y
⊢ IsClopen (f ⁻¹' s) ↔ IsClopen s

Tactic:
and_congr hf.isClosed_preimage hf.isOpen_preimage

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsCoinducing.isClosed_preimage, Topology.IsQuotientMap.isCoinducing, IsClopen, and_congr
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
U : Set X
rw : IsClopen (U.boolIndicator ⁻¹' {true}) ↔ IsClopen U
rw₁ rw₂ : IsClopen U ↔ IsClopen U
⊢ Continuous[inst, _] U.boolIndicator ↔ IsClopen U

Tactic:
rw [continuous_bool_rng true, preimage_boolIndicator_true]

Premises used: continuous_bool_rng, Set.preimage_boolIndicator_true, Bool.true
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s U : Set X
rw :
  Continuous[instTopologicalSpaceSubtype, _] (s.restrict (π := fun (a : X) ↦ Bool) U.boolIndicator) ↔
    Continuous[instTopologicalSpaceSubtype, _] (boolIndicator (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U))
⊢ ContinuousOn U.boolIndicator s ↔ IsClopen (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U)

Tactic:
rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]

Premises used: continuous_boolIndicator_iff_isClopen, continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s U : Set X
⊢ Continuous[instTopologicalSpaceSubtype, _] (s.restrict (π := fun (a : X) ↦ Bool) U.boolIndicator) ↔
    Continuous[instTopologicalSpaceSubtype, _] (boolIndicator (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U))

Tactic:
rfl
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
⊢ Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)

Tactic:
have hp : Continuous (fun y : Y ↦ (a.1, y)) := .prodMk_right _
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
V : Set Y := {y : Y | (a.1, y) ∈ W}
⊢ IsCompact V

Tactic:
have hV : IsCompact V := (W.2.1.preimage hp).isCompact
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
V : Set Y := {y : Y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x : X | MapsTo (Prod.mk x) V (↑W : Set (X × Y))}
⊢ U ×ˢ V ⊆ (↑W : Set (X × Y))

Tactic:
have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
V : Set Y := {y : Y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x : X | MapsTo (Prod.mk x) V (↑W : Set (X × Y))}
hUV : U ×ˢ V ⊆ (↑W : Set (X × Y))
⊢ Membership.mem (γ := Clopens X) { carrier := U, isClopen' := ⋯ } a.1

Tactic:
simp [U, V, MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
V : Set Y := {y : Y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x : X | MapsTo (Prod.mk x) V (↑W : Set (X × Y))}
hUV : U ×ˢ V ⊆ (↑W : Set (X × Y))
⊢ ∃ (U : Clopens X), a.1 ∈ U ∧ ∃ (V : Clopens Y), a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
exact ⟨⟨U, (ContinuousMap.isClopen_setOf_mapsTo hV W.2).preimage
    (ContinuousMap.id (X × Y)).curry.2⟩, by simp [U, V, MapsTo], ⟨V, W.2.preimage hp⟩, h, hUV⟩
-- Module: Mathlib.Topology.ClopenBox
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)
choose! :
  ∀ (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
⊢ ∃ (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:
choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)

Premises used: TopologicalSpace.Clopens.exists_prod_subset
-- Module: Mathlib.Topology.ClopenBox
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
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
⊢ ∃ (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⟩

Premises used: SProd.sprod, IsCompact.elim_nhds_subcover, IsClopen.isOpen, SetLike.coe, And.left, TopologicalSpace.Clopens.isClopen', And.intro, IsOpen.mem_nhds, IsClosed.isCompact
-- Module: Mathlib.Topology.ClopenBox
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 :
  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

Tactic:
use I.image fun x ↦ (U x, V x)

Premises used: Prod.mk, Finset.image
-- Module: Mathlib.Topology.ClopenBox
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 : 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))
⊢ 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:
rw [Finset.sup_image]

Premises used: Finset.sup_image
-- Module: Mathlib.Topology.ClopenBox
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))

Tactic:
le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)

Premises used: Finset.sup_le, le_antisymm
-- Module: Mathlib.Topology.ClopenBox
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
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
⊢ 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:
refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)

Premises used: Finset.sup_le, le_antisymm
-- Module: Mathlib.Topology.ClopenBox
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
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
⊢ 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⟩

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.ClopenBox
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
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:
SetLike.le_def.1 (Finset.le_sup hi) hxi

Premises used: Set.Mem, SetLike.le_def, Iff.mp, Finset.le_sup
-- Module: Mathlib.Topology.ClopenBox
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
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:
exact SetLike.le_def.1 (Finset.le_sup hi) hxi

Premises used: SetLike.le_def, Iff.mp, Finset.le_sup
-- Module: Mathlib.Topology.ClopenBox
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 ∈ 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:
hUV _ <| hIW _ hx

Premises used: Set.Mem
-- Module: Mathlib.Topology.ClopenBox
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 ∈ 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:
exact hUV _ <| hIW _ hx
-- Module: Mathlib.Topology.ClopenBox
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
h₄ 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
⊢ ∃ (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:
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

Premises used: Finset.sup_le, le_antisymm, Finset.sup_image
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
⊢ Surjective (β := Clopens (X × Y)) fun (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))) ↦
    I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2

Tactic:
fun W ↦
  let ⟨I, hI⟩ := W.exists_finset_eq_sup_prod; ⟨I, hI.symm⟩

Premises used: SProd.sprod, Exists, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, Prod.fst, _private.0.TopologicalSpace.Clopens.surjective_finset_sup_prod.match_1, Exists.intro, Finset.sup, Eq.symm, Eq, Prod.snd, Function.Surjective
-- Module: Mathlib.Topology.ClopenBox
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 : Countable.{u_1 + 1} (Clopens X)
inst_5 : Countable.{u_2 + 1} (Clopens Y)
⊢ Countable (Clopens (X × Y))

Tactic:
surjective_finset_sup_prod.countable

Premises used: Function.Surjective.countable, TopologicalSpace.Clopens.surjective_finset_sup_prod
-- Module: Mathlib.Topology.ClopenBox
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)
intro : ∀ (val : Fintype (Clopens X)), Finite (Clopens (X × Y))
⊢ Finite (Clopens (X × Y))

Tactic:
cases nonempty_fintype (Clopens X)

Premises used: nonempty_fintype, TopologicalSpace.Clopens
-- Module: Mathlib.Topology.ClopenBox
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)
intro : ∀ (val : Fintype (Clopens Y)), Finite (Clopens (X × Y))
⊢ Finite (Clopens (X × Y))

Tactic:
cases nonempty_fintype (Clopens Y)

Premises used: nonempty_fintype, TopologicalSpace.Clopens
-- Module: Mathlib.Topology.ClopenBox
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)
val_1 : Fintype (Clopens Y)
⊢ Finite (Clopens (X × Y))

Tactic:
.of_surjective _ surjective_finset_sup_prod

Premises used: TopologicalSpace.Clopens.surjective_finset_sup_prod, Finite.of_surjective
-- Module: Mathlib.Topology.ClopenBox
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)
val_1 : Fintype (Clopens Y)
⊢ Finite (Clopens (X × Y))

Tactic:
exact .of_surjective _ surjective_finset_sup_prod
-- Module: Mathlib.Topology.ClopenBox
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

Tactic:
⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩

Premises used: setOf, SecondCountableTopology.mk, And.intro, Iff.intro, Exists.intro, IsClopen
-- Module: Mathlib.Topology.ClopenBox
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}
refine_3 : ∀ (h : SecondCountableTopology X), Countable.{u_1 + 1} (Clopens X)
⊢ Countable.{u_1 + 1} (Clopens X) ↔ SecondCountableTopology X

Tactic:
refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.ClopenBox
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)
f : (↑{s : Set X | IsClopen s} : Type u_1) → Clopens X :=
  fun (s : (↑{s : Set X | IsClopen s} : Type u_1)) ↦ { carrier := (↑s : Set X), isClopen' := ⋯ }
⊢ Set.Countable.{u_1} (α := Set X) {s : Set X | IsClopen s}

Tactic:
Injective.of_eq_imp_le (f := f) (·.le) |>.countable

Premises used: Function.Injective.countable, Eq.le, Set.Countable, Function.Injective.of_eq_imp_le
-- Module: Mathlib.Topology.ClopenBox
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)
f : (↑{s : Set X | IsClopen s} : Type u_1) → Clopens X :=
  fun (s : (↑{s : Set X | IsClopen s} : Type u_1)) ↦ { carrier := (↑s : Set X), isClopen' := ⋯ }
⊢ Set.Countable.{u_1} (α := Set X) {s : Set X | IsClopen s}

Tactic:
exact Injective.of_eq_imp_le (f := f) (·.le) |>.countable

Premises used: Function.Injective.countable, Eq.le, Function.Injective.of_eq_imp_le
-- Module: Mathlib.Topology.ClopenBox
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)
refine_2 : IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
⊢ inst = generateFrom {s : Set X | IsClopen s}

Tactic:
apply IsTopologicalBasis.eq_generateFrom

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.ClopenBox
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)
⊢ IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}

Tactic:
loc_compact_Haus_tot_disc_of_zero_dim

Premises used: loc_compact_Haus_tot_disc_of_zero_dim
-- Module: Mathlib.Topology.ClopenBox
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)
⊢ IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}

Tactic:
exact loc_compact_Haus_tot_disc_of_zero_dim

Premises used: loc_compact_Haus_tot_disc_of_zero_dim
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ ∀ (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
-- Module: Mathlib.Topology.ClopenBox
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))))
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
⊢ f s = f t → s = t

Tactic:
(h : Exists.choose _ = Exists.choose _)