awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
s : Set α
U : (i : Fin n) → Set α
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₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) s U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
    univ
hi : ¬IsConnected s
⊢ ∃ (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 : ∀ (a b : Set α) (ha : IsClopen a) (hb : IsClopen b) (ha' : a.Nonempty) (hb' : b.Nonempty) (hab : Disjoint a b)
  (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 α) (a ∪ b) U))))
  (h₁ :
    ∀ (i_1 : Fin (n + 1)),
      IsClopen.{u} (X := α)
        (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U
          ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1)))
  (h₂ :
    ∀ (i_1 : Fin (n + 1)),
      Set.Nonempty.{u} (α := α)
        (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U
          ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1)))
  (h₄ :
    Eq.{u + 1} (α := Set α)
      (⋃ (i_1 : Fin (n + 1)),
        Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U
          ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
      univ)
  (hi : ¬IsConnected (a ∪ b)),
  ∃ (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: 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)
Cleared hypotheses: s, h₃, h₁, h₂, h₄, hi
-- 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 : (i : Fin n) → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
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 α) (a ∪ b) U)))
h₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
    univ
hi : ¬IsConnected (a ∪ b)
⊢ ∃ (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 : ∀ (i : Fin (n + 1 + 1)),
  IsClopen.{u} (X := α)
    (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U) i)
Tactic: refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
-- 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 : (i : Fin n) → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
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 α) (a ∪ b) U)))
h₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
    univ
hi : ¬IsConnected (a ∪ b)
inr :
  ∀ (i : Fin (n + 1 + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b 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₁ : ∀ (i : Fin (n + 1 + 1)),
  Set.Nonempty.{u} (α := α)
    (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U) i)
Tactic: refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
-- 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 : (i : Fin n) → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
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 α) (a ∪ b) U)))
h₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
    univ
hi : ¬IsConnected (a ∪ b)
inr :
  ∀ (i : Fin (n + 1 + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U) i)
inr₁ :
  ∀ (i : Fin (n + 1 + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b 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₂ : Pairwise (α := Fin (n + 1 + 1))
  (onFun.{1, u + 1, 1} (β := Set α) Disjoint
    (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U)))
Tactic: refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
-- 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 : (i : Fin n) → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
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 α) (a ∪ b) U)))
h₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
    univ
hi : ¬IsConnected (a ∪ b)
inr :
  ∀ (i : Fin (n + 1 + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U) i)
inr₁ :
  ∀ (i : Fin (n + 1 + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U) i)
inr₂ :
  Pairwise (α := Fin (n + 1 + 1))
    (onFun.{1, u + 1, 1} (β := Set α) Disjoint
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U)))
⊢ ∃ (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₃ : Eq.{u + 1} (α := Set α)
  (⋃ (i : Fin (n + 1 + 1)),
    Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U) i)
  univ
Tactic: refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
i : Fin (n + 1)
U : (i : Fin n) → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
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 α) (a ∪ b) U)))
h₁ :
  ∀ (i_1 : Fin (n + 1)),
    IsClopen.{u} (X := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₂ :
  ∀ (i_1 : Fin (n + 1)),
    Set.Nonempty.{u} (α := α)
      (Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
h₄ :
  Eq.{u + 1} (α := Set α)
    (⋃ (i_1 : Fin (n + 1)),
      Fin.cons (α := fun (b : Fin (n + 1)) ↦ Set α) (a ∪ b) U ((Equiv.swap 0 i : (a : Fin (n + 1)) → Fin (n + 1)) i_1))
    univ
hi : ¬IsConnected (a ∪ b)
⊢ Pairwise (α := Fin (n + 1 + 1))
    (onFun.{1, u + 1, 1} (β := Set α) Disjoint
      (Fin.cons (α := fun (a : Fin (n + 1 + 1)) ↦ Set α) a (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Set α) b U)))
have h₃' : ∀ (j : Fin n), Disjoint (U j) a ∧ Disjoint (U j) b
Tactic: 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))
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
⊢ ∃ (U : Fin (n + 1) → Set α),
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧
        Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
have inr : ∃ (U : Fin (HAdd.hAdd (α := ℕ) 0 1) → Set α),
  (∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), IsClopen (U i)) ∧
    (∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), (U i).Nonempty) ∧
      Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), U i) univ
Tactic: induction n with
  | zero => exact ⟨![.univ], by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]⟩
  | succ n IH =>
    obtain ⟨U, h₁, h₂, h₃, h₄⟩ := IH
    obtain ⟨i, hi⟩ : ∃ i, ¬ IsConnected (U i) := by
      simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)
    obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U
    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: n
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
inr :
  ∃ (U : Fin (HAdd.hAdd (α := ℕ) 0 1) → Set α),
    (∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), (U i).Nonempty) ∧
        Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), U i) univ
⊢ ∃ (U : Fin (n + 1) → Set α),
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧
        Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
have inr₁ : ∀ (n : ℕ)
  (IH :
    ∃ (U : Fin (n + 1) → Set α),
      (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
        (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧
          Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 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: induction n with
  | zero => exact ⟨![.univ], by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]⟩
  | succ n IH =>
    obtain ⟨U, h₁, h₂, h₃, h₄⟩ := IH
    obtain ⟨i, hi⟩ : ∃ i, ¬ IsConnected (U i) := by
      simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)
    obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U
    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: n
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x} = connectedComponent x
have h : ∀ (y : α),
  Membership.mem (γ := Set α) (preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x})
      y ↔
    y ∈ connectedComponent x
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
⊢ Membership.mem (γ := Set α) (preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x})
      y ↔
    y ∈ connectedComponent x
have h : Membership.mem (γ := Set (ConnectedComponents α)) {ConnectedComponents.mk x} (ConnectedComponents.mk y) ↔
  y ∈ connectedComponent x
Tactic: rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
h :
  Membership.mem (γ := Set (ConnectedComponents α)) {ConnectedComponents.mk x} (ConnectedComponents.mk y) ↔
    y ∈ connectedComponent x
⊢ Membership.mem (γ := Set α) (preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x})
      y ↔
    y ∈ connectedComponent x
have h₁ : Eq (α := ConnectedComponents α) (ConnectedComponents.mk y) (ConnectedComponents.mk x) ↔ y ∈ connectedComponent x
Tactic: rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
h :
  Membership.mem (γ := Set (ConnectedComponents α)) {ConnectedComponents.mk x} (ConnectedComponents.mk y) ↔
    y ∈ connectedComponent x
h₁ : Eq (α := ConnectedComponents α) (ConnectedComponents.mk y) (ConnectedComponents.mk x) ↔ y ∈ connectedComponent x
⊢ Membership.mem (γ := Set α) (preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x})
      y ↔
    y ∈ connectedComponent x
have h₂ : y ∈ connectedComponent x ↔ y ∈ connectedComponent x
Tactic: rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ DiscreteTopology.{u} (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst] (connectedComponent x)
have simp_rw : (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
  ∀ (x : α), IsOpen[inst] (connectedComponent x)
Tactic: simp_rw [discreteTopology_iff_isOpen_singleton, ← connectedComponents_preimage_singleton,
    isQuotientMap_coe.isOpen_preimage, surjective_coe.forall]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
simp_rw :
  (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
    ∀ (x : α), IsOpen[inst] (connectedComponent x)
⊢ DiscreteTopology.{u} (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst] (connectedComponent x)
have simp_rw₁ : (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
  ∀ (x : α), IsOpen[inst] (preimage (β := ConnectedComponents α) mk {mk x})
Tactic: simp_rw [discreteTopology_iff_isOpen_singleton, ← connectedComponents_preimage_singleton,
    isQuotientMap_coe.isOpen_preimage, surjective_coe.forall]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
simp_rw :
  (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
    ∀ (x : α), IsOpen[inst] (connectedComponent x)
simp_rw₁ :
  (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
    ∀ (x : α), IsOpen[inst] (preimage (β := ConnectedComponents α) mk {mk x})
⊢ DiscreteTopology.{u} (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst] (connectedComponent x)
have simp_rw₂ : (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
  ∀ (x : α), IsOpen (X := ConnectedComponents α) {mk x}
Tactic: simp_rw [discreteTopology_iff_isOpen_singleton, ← connectedComponents_preimage_singleton,
    isQuotientMap_coe.isOpen_preimage, surjective_coe.forall]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
⊢ ∀ (u v : Set α),
    IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
have by_contra! : ∀ (u v : Set α) (u_op : IsOpen[inst] u) (v_op : IsOpen[inst] v) (hsuv : s ⊆ u ∪ v) (x : α) (x_in_s : x ∈ s)
  (x_in_u : x ∈ u) (H : s ∩ (u ∩ v) = ∅) (y : α) (y_in_s : y ∈ s) (y_in_v : y ∈ v), False
Tactic: by_contra! ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
⊢ False
have hy : y ∉ u
Tactic: have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_notMem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ ContinuousOn u.boolIndicator s
have apply : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
apply : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ ContinuousOn u.boolIndicator s
have apply₁ : IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
have rw : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
Tactic: rw [preimage_subtype_coe_eq_compl hsuv H]