-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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)
⊢ ∃ (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
have 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
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₄
Cleared hypotheses: U, h₁, h₂, h₃, h₄, hi