-- Mathlib/Topology/ClopenBox.lean
lemma countable_iff_secondCountable [T2Space X]
    [TotallyDisconnectedSpace X] : Countable (Clopens X) ↔ SecondCountableTopology X

Proof state:
case refine_2.self
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
exact loc_compact_Haus_tot_disc_of_zero_dim

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ ↑s = ↑t

Tactic:
change s.carrier = t.carrier

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ s.carrier = t.carrier

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ s = t

Tactic:
ext1

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ ↑s = ↑t

Proof state:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
hf : Injective f
⊢ Countable (Clopens X)

Tactic:
exact hf.countable

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
⊢ Countable (Clopens X) ↔ SecondCountableTopology X

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

Result:
case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ {s | IsClopen s}.Countable

case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)

Proof state:
case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
f : ↑{s | IsClopen s} → Clopens X := fun s => { carrier := ↑s, isClopen' := ⋯ }
⊢ {s | IsClopen s}.Countable

Tactic:
exact (injective_of_le_imp_le f fun a ↦ a).countable

Result:
no goals

Proof state:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
⊢ Countable (Clopens X)

Tactic:
let f : Clopens X → Finset (countableBasis X) := fun s ↦ (this s).choose

Result:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
⊢ Countable (Clopens X)

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
⊢ Injective f

Tactic:
intro s t (h : Exists.choose _ = Exists.choose _)

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ s = t

Proof state:
case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ {s | IsClopen s}.Countable

Tactic:
let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩

Result:
case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
f : ↑{s | IsClopen s} → Clopens X := fun s => { carrier := ↑s, isClopen' := ⋯ }
⊢ {s | IsClopen s}.Countable

Proof state:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)

Tactic:
have : ∀ (s : Clopens X), ∃ (t : Finset (countableBasis X)), s.1 = t.toSet.sUnion :=
  fun s ↦ eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _
    (isBasis_countableBasis X) s.1 s.2.1.isCompact s.2.2

Result:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
⊢ Countable (Clopens X)

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h✝ : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
s t : Clopens X
h : ⋯.choose = ⋯.choose
⊢ s.carrier = t.carrier

Tactic:
rw [(this s).choose_spec, (this t).choose_spec, h]

Result:
no goals

Proof state:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
⊢ Countable (Clopens X)

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]

Result:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this : ∀ (s : Clopens X), ∃ t, s.carrier = ⋃₀ (Subtype.val '' ↑t)
f : Clopens X → Finset ↑(countableBasis X) := fun s => ⋯.choose
hf : Injective f
⊢ Countable (Clopens X)

Proof state:
case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

Tactic:
apply IsTopologicalBasis.eq_generateFrom

Result:
case refine_2.self
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ IsTopologicalBasis {s | IsClopen s}