awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
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
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
⊢ ∃ (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)

Premises used: mt, IsClopen.not_isPreconnected_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Connected.Clopen
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

Tactic:
⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩

Premises used: Fin.cons, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
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)))
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
⊢ ∃ (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:
refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
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)
⊢ ∀ (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:
simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))

Premises used: Fin.succ, Equiv.swap, Fin.forall_iff_succ, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.Connected.Clopen
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)
⊢ ∀ (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:
simpa [Fin.forall_iff_succ, *] using fun x ↦ h₂ (Equiv.swap 0 i (.succ x))

Premises used: Fin.succ, Equiv.swap, Fin.forall_iff_succ, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.Connected.Clopen
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)
j : Fin n
⊢ Disjoint (U j) a ∧ Disjoint (U j) b

Tactic:
simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))

Premises used: Function.onFun, Equiv.swap, Function.Injective.ne, Fin.succ_ne_zero, Equiv.injective, OfNat.ofNat
-- Module: Mathlib.Topology.Connected.Clopen
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)
⊢ ∀ (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))
-- Module: Mathlib.Topology.Connected.Clopen
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)
h₃' : ∀ (j : Fin n), Disjoint (U j) a ∧ Disjoint (U j) 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)))

Tactic:
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 _))

Premises used: Function.onFun, Equiv.swap, Fin.succ_injective, Pairwise.comp_of_injective, disjoint_comm, Fin.forall_iff_succ, Function.Injective.comp, Pairwise, Equiv.injective, OfNat.ofNat
-- Module: Mathlib.Topology.Connected.Clopen
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)
⊢ 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:
simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

Premises used: Function.Surjective.iUnion_comp, Equiv.surjective, Set.union_assoc
-- Module: Mathlib.Topology.Connected.Clopen
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
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
⊢ ∃ (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

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₄

Premises used: Function.onFun, Equiv.piCongrLeft_symm_apply, Fin.forall_iff_succ, Pairwise, Function.Surjective.iUnion_comp, Equiv.surjective, Set.union_assoc, Equiv.swap_apply_right, rfl, Fin.cons_zero
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h :
  ∀ (y : α),
    Membership.mem (γ := Set α)
        (preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x}) y ↔
      y ∈ connectedComponent x
⊢ preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x} = connectedComponent x

Tactic:
ext y
-- Module: Mathlib.Topology.Connected.Clopen
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
h₂ h₃ : y ∈ connectedComponent x ↔ y ∈ connectedComponent x
⊢ Membership.mem (γ := Set α) (preimage (β := ConnectedComponents α) ConnectedComponents.mk {ConnectedComponents.mk x})
      y ↔
    y ∈ connectedComponent x

Tactic:
rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe']

Premises used: ConnectedComponents.coe_eq_coe', Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
U : Set α
⊢ preimage (β := ConnectedComponents α) ConnectedComponents.mk (ConnectedComponents.mk '' U) =
    ⋃ x ∈ U, connectedComponent x

Tactic:
simp only [connectedComponents_preimage_singleton, preimage_iUnion₂, image_eq_iUnion]

Premises used: Set.image_eq_iUnion, connectedComponents_preimage_singleton, Set.preimage_iUnion₂
-- Module: Mathlib.Topology.Connected.Clopen
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})
simp_rw₂ :
  (∀ (a : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {a}) ↔
    ∀ (x : α), IsOpen (X := ConnectedComponents α) {mk x}
⊢ DiscreteTopology.{u} (ConnectedComponents α) ↔ ∀ (x : α), IsOpen[inst] (connectedComponent x)

Tactic:
simp_rw [discreteTopology_iff_isOpen_singleton, ← connectedComponents_preimage_singleton,
    isQuotientMap_coe.isOpen_preimage, surjective_coe.forall]

Premises used: Function.Surjective.forall, connectedComponents_preimage_singleton, ConnectedComponents.surjective_coe, Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, ConnectedComponents.isQuotientMap_coe, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
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
⊢ ∀ (u v : Set α),
    IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

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⟩
-- Module: Mathlib.Topology.Connected.Clopen
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
⊢ 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⟩⟩
-- Module: Mathlib.Topology.Connected.Clopen
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)
apply₁ : IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ ContinuousOn u.boolIndicator s

Tactic:
apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩

Premises used: Iff.mpr, continuousOn_boolIndicator_iff_isClopen, And.intro
-- Module: Mathlib.Topology.Connected.Clopen
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
rw : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
rw [preimage_subtype_coe_eq_compl hsuv H]

Premises used: Set.preimage_subtype_coe_eq_compl
-- Module: Mathlib.Topology.Connected.Clopen
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) ⁻¹' v)ᶜ

Tactic:
(v_op.preimage continuous_subtype_val).isClosed_compl

Premises used: continuous_subtype_val, IsOpen.isClosed_compl, IsOpen.preimage