-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
obtain :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
obtain₁ :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
    (hWun : Finset.sup Finset.univ W = Finset.sup Finset.univ V) (hWd : Pairwise (Disjoint on W)),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
obtain₂ :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
    (hWd : Pairwise (Disjoint on W))
    (hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
obtain₃ :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
    (hWd : Pairwise (Disjoint on W))
    (hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
have refine_1 : ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
  (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
  (hWd : Pairwise (Disjoint on W))
  (hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))),
  let t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥};
  ∀ (k : Fin #t),
    Ne.{u_2 + 1} (α := Clopens X) ((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) ⊥
Tactic: classical
  obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective