-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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) ⊥
refine_2 :
  ∀ (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),
      ∃ (i : ι),
        (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) : Set X) ⊆ (↑(U i) : Set X)
refine_3 :
  ∀ (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 ≠ ⊥};
    ∀ (x : X) (hx : Membership.mem (γ := Set X) univ x),
      Membership.mem (γ := Set X)
        (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
refine_4 :
  ∀ (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 ≠ ⊥};
    Pairwise (α := Fin #t)
      (Function.onFun.{1, u_2 + 1, 1} (β := Clopens X) Disjoint fun (k : Fin #t) ↦
        W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))
refine_2₁ :
  ∀ (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),
      ∃ (i : ι),
        (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) : Set X) ⊆ (↑(U i) : Set X)
refine_3₁ :
  ∀ (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 ≠ ⊥};
    ∀ (x : X) (hx : Membership.mem (γ := Set X) univ x),
      Membership.mem (γ := Set X)
        (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
refine_4₁ :
  ∀ (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 ≠ ⊥};
    Pairwise (α := Fin #t)
      (Function.onFun.{1, u_2 + 1, 1} (β := Clopens X) Disjoint fun (k : Fin #t) ↦
        W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))
refine_3₂ :
  ∀ (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 ≠ ⊥};
    ∀ (x : X) (hx : Membership.mem (γ := Set X) univ x),
      Membership.mem (γ := Set X)
        (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
refine_4₂ refine_4₃ :
  ∀ (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 ≠ ⊥};
    Pairwise (α := Fin #t)
      (Function.onFun.{1, u_2 + 1, 1} (β := Clopens X) Disjoint fun (k : Fin #t) ↦
        W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))
⊢ ∃ (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)

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

Premises used: Finset.mem_univ, Set.mem_iUnion, TopologicalSpace.Clopens.coe_finset_sup, Set.iUnion_true, Iff.mp, SetLike.coe_set_eq, TopologicalSpace.IsOpenCover.exists_finite_clopen_cover