-- 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_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
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))) =
    ⋃₀
      (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
        (↑(⋯.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)))
h₃ h₄ :
  ⋃₀
      (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
        (↑(⋯.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))) =
    ⋃₀
      (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) ''
        (↑(⋯.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)))
⊢ s.carrier = t.carrier

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

Premises used: Exists.choose_spec