-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
i : Fin (n + 1)
U : (b : Fin (n + 1)) → Set α
h₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
          (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
        U i_1)
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
          (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
        U i_1)
h₃ :
  Pairwise (α := Fin (n + 1))
    (onFun.{1, u + 1, 1} (β := Set α) Disjoint
      ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
          (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
        U))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      (Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
          (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
        U i_1)
    univ
hi :
  ¬IsConnected.{u} (α := α)
      ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
          (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
        U i)
inr :
  ∀ (s : Set α) (U : (i : Fin n) → Set α)
    (h₁ :
      ∀ (i_1 : Fin (n + 1)),
        IsClopen.{u} (X := α)
          ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
              (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
            (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U) i_1))
    (h₂ :
      ∀ (i_1 : Fin (n + 1)),
        Set.Nonempty.{u} (α := α)
          ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
              (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
            (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U) i_1))
    (h₃ :
      Pairwise (α := Fin (n + 1))
        (onFun.{1, u + 1, 1} (β := Set α) Disjoint
          ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
              (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
            (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U))))
    (h₄ :
      Eq.{u + 1} (α := Set α)
        (⋃ (i_1 : Fin (n + 1)),
          (Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
              (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
            (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U) i_1)
        univ)
    (hi :
      ¬IsConnected.{u} (α := α)
          ((Equiv.symm (Equiv.piCongrLeft.{u + 1, 1, 1} (fun (x : Fin (n + 1)) ↦ Set α) (Equiv.swap 0 i)) :
              (a : (b : Fin (n + 1)) → Set α) → (a : Fin (n + 1)) → Set α)
            (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U) i)),
    ∃ (U : Fin (n + 1 + 1) → Set α),
      (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
        (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧
          Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1 + 1)), U i) univ
⊢ ∃ (U : Fin (n + 1 + 1) → Set α),
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧
        Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1 + 1)), U i) univ

Tactic:
cases U using Fin.consCases with | cons s U =>
    simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
    obtain ⟨a, b, ha, hb, ha', hb', hab, rfl⟩ := (show IsClopen s by simpa using h₁ i)
      |>.not_isPreconnected_iff.mp (mt (⟨by simpa using h₂ i, ·⟩) hi)
    refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₂ (Equiv.swap 0 i (.succ x))
    · have h₃' (j : _) : Disjoint (U j) a ∧ Disjoint (U j) b := by
        simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))
      simpa [Pairwise, Fin.forall_iff_succ, onFun, hab, disjoint_comm (a := a),
        disjoint_comm (a := b), h₃'] using
        h₃.comp_of_injective ((Equiv.swap 0 i).injective.comp (Fin.succ_injective _))
    · simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

Premises used: Function.onFun, Equiv.piCongrLeft_symm_apply, Fin.succ, Equiv.swap, Fin.succ_injective, Pairwise.comp_of_injective, Fin.forall_iff_succ, Function.Injective.comp, Pairwise, Function.Surjective.iUnion_comp, Equiv.injective, Equiv.surjective, Set.union_assoc, OfNat.ofNat, Equiv.swap_apply_right, DFunLike.coe, rfl, Fin.cons_zero