-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_4
I : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I
Z D : I → Set X
Z_closed : ∀ (i : I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : I), IsClopen (D i)
Z_subset_D : ∀ (i : I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
of_equiv :
  ∀ {α β : Type u_5} (e : α ≃ β)
    (IH :
      ∀ {Z D : α → Set X} (Z_closed : ∀ (i : α), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : α), IsClopen (D i))
        (Z_subset_D : ∀ (i : α), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
        ∃ (C : α → Set X),
          (∀ (i : α), IsClopen (C i)) ∧
            (∀ (i : α), Z i ⊆ C i) ∧
              (∀ (i : α), C i ⊆ D i) ∧
                Subset.{u_4} (α := Set X) (⋃ (i : α), D i) (⋃ (i : α), C i) ∧ PairwiseDisjoint univ C)
    {Z D : β → Set X} (Z_closed : ∀ (i : β), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : β), IsClopen (D i))
    (Z_subset_D : ∀ (i : β), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : β → Set X),
      (∀ (i : β), IsClopen (C i)) ∧
        (∀ (i : β), Z i ⊆ C i) ∧
          (∀ (i : β), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), C i) ∧ PairwiseDisjoint univ C
h_empty :
  ∀ {Z D : PEmpty.{u_5 + 1} → Set X} (Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst] (Z i))
    (D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)) (Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i)
    (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : PEmpty.{u_5 + 1} → Set X),
      (∀ (i : PEmpty.{u_5 + 1}), IsClopen (C i)) ∧
        (∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ C i) ∧
          (∀ (i : PEmpty.{u_5 + 1}), C i ⊆ D i) ∧
            Subset.{u_4} (α := Set X) (⋃ (i : PEmpty.{u_5 + 1}), D i) (⋃ (i : PEmpty.{u_5 + 1}), C i) ∧
              PairwiseDisjoint univ C
h_option :
  ∀ {I : Type u_5} [Fintype I]
    (IH :
      ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
        (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
        ∃ (C : I → Set X),
          (∀ (i : I), IsClopen (C i)) ∧
            (∀ (i : I), Z i ⊆ C i) ∧
              (∀ (i : I), C i ⊆ D i) ∧
                Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C)
    {Z D : Option I → Set X} (Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i))
    (D_clopen : ∀ (i : Option I), IsClopen (D i)) (Z_subset_D : ∀ (i : Option I), Z i ⊆ D i)
    (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : Option I → Set X),
      (∀ (i : Option I), IsClopen (C i)) ∧
        (∀ (i : Option I), Z i ⊆ C i) ∧
          (∀ (i : Option I), C i ⊆ D i) ∧
            Subset.{u_4} (α := Set X) (⋃ (i : Option I), D i) (⋃ (i : Option I), C i) ∧ PairwiseDisjoint univ C
⊢ ∃ (C : I → Set X),
    (∀ (i : I), IsClopen (C i)) ∧
      (∀ (i : I), Z i ⊆ C i) ∧
        (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C

Tactic:
induction I using Finite.induction_empty_option with
  | of_equiv e IH =>
    obtain ⟨C, h1, h2, h3, h4, h5⟩ := IH (Z := Z ∘ e) (D := D ∘ e)
      (fun i ↦ Z_closed (e i)) (fun i ↦ D_clopen (e i))
      (fun i ↦ Z_subset_D (e i)) (by simpa [← e.injective.injOn.pairwiseDisjoint_image])
    refine ⟨C ∘ e.symm, fun i ↦ h1 (e.symm i), fun i ↦ by simpa using h2 (e.symm i),
      fun i ↦ by simpa using h3 (e.symm i), ?_,
      by simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]⟩
    simp only [Function.comp_apply, iUnion_subset_iff] at h4
    simpa [e.symm.surjective.iUnion_comp C] using fun i ↦ h4 (e.symm i)
  | h_empty => exact ⟨fun _ ↦ univ, by simp, by simp, by simp, by simp, fun i ↦ PEmpty.elim i⟩
  | @h_option I _ IH =>
    -- let `Z'` be the restriction of `Z` along `some : I → Option I`
    let Z' : I → Set X := fun i ↦ Z (some i)
    have Z'_closed (i : I) : IsClosed (Z (some i)) := Z_closed (some i)
    have Z'_disj : univ.PairwiseDisjoint (Z ∘ some) := by
      rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image]
      exact PairwiseDisjoint.subset Z_disj (by simp)
    -- find `Z none ⊆ V ⊆ D none \ ⋃ Z'` using `exists_clopen_of_closed_subset_open`
    let U : Set X := D none \ ⋃ i, Z (some i)
    have U_open : IsOpen U := IsOpen.sdiff (D_clopen none).2
      (isClosed_iUnion_of_finite (fun i ↦ Z_closed (some i)))
    have Z0_subset_U : Z none ⊆ U := by
      rw [subset_diff]
      simpa using ⟨Z_subset_D none, fun i ↦ (by apply Z_disj; all_goals simp)⟩
    obtain ⟨V, V_clopen, Z0_subset_V, V_subset_U⟩ :=
      exists_clopen_of_closed_subset_open (Z_closed none) U_open Z0_subset_U
    have V_subset_D0 : V ⊆ D none := subset_trans V_subset_U diff_subset
    -- choose `Z' i ⊆ C' i ⊆ D' i = D i.succ \ V` using the inductive hypothesis
    let D' : I → Set X := fun i ↦ D (some i) \ V
    have D'_clopen (i : I) : IsClopen (D' i) := (D_clopen (some i)).diff V_clopen
    have Z'_subset_D' (i : I) : Z' i ⊆ D' i := by
      rw [subset_diff]
      refine ⟨by grind, Disjoint.mono_right V_subset_U ?_⟩
      exact Disjoint.mono_left (subset_iUnion_of_subset i fun _ h ↦ h) (by grind)
    obtain ⟨C', C'_clopen, Z'_subset_C', C'_subset_D', C'_cover_D', C'_disj⟩ :=
      IH Z'_closed D'_clopen Z'_subset_D' Z'_disj
    -- now choose `C0 = D none \ ⋃ C' i`
    let C0 : Set X := D none \ ⋃ i, C' i
    have : IsClopen C0 := (D_clopen none).diff (isClopen_iUnion_of_finite C'_clopen)
    have : Z none ⊆ C0 := by
      simp only [C0, subset_diff]
      exact ⟨by grind, Disjoint.mono_left Z0_subset_V (by simp; grind)⟩
    -- patch together to define `C none := C0`, `C (some i) := C' i`
    -- and verify the needed properties
    let C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
    refine ⟨C, ?_, ?_, ?_, ?_, ?_⟩
    all_goals try rintro (_ | i); all_goals grind
    · intro x hx
      rw [mem_iUnion] at hx ⊢
      by_cases hx0 : x ∈ C0; { exact ⟨none, hx0⟩ }
      by_cases hxD : x ∈ D none
      · have hxC' : x ∈ ⋃ i, C' i := by grind
        obtain ⟨i, hi⟩ := mem_iUnion.mp hxC'
        exact ⟨some i, hi⟩
      · obtain ⟨none | j, hi⟩ := hx; {grind}
        have hxD' : x ∈ ⋃ i, D' i := mem_iUnion.mpr ⟨j, by grind⟩
        obtain ⟨k, hk⟩ := mem_iUnion.mp <| C'_cover_D' hxD'
        exact ⟨some k, hk⟩
    · rw [Set.pairwiseDisjoint_iff]
      rintro (_ | i) _ (_ | j) _
      · simp
      · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_right (subset_iUnion C' j) disjoint_sdiff_left
      · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using
          Disjoint.mono_left (subset_iUnion C' i) disjoint_sdiff_right
      · simpa using (Set.pairwiseDisjoint_iff.mp C'_disj) (by trivial) (by trivial)

Premises used: Finite.induction_empty_option, Set.iUnion_subset_iff, Set.not_nonempty_iff_eq_empty, Set.mem_iUnion, Set.disjoint_iff_inter_eq_empty, Option.none, Iff.mp, Set.pairwiseDisjoint_iff, Function.comp_apply