-- 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
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)))
⊢ s.carrier = t.carrier
have h₃ : ⋃₀
    (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))) =
  ⋃₀
    (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]