awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
i : ι
x : α
hx : x ∈ U i
a :
  Eq.{u + 1} (α := ConnectedComponents α)
    (((equivOfIsClopen (U := U) hclopen hdisj hunion).symm :
          (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)) → ConnectedComponents α)
        ((equivOfIsClopen (U := U) hclopen hdisj hunion :
            (a : ConnectedComponents α) → (i : ι) × ConnectedComponents (↑(U i) : Type u))
          (mk x)) :
      ConnectedComponents α)
    (((equivOfIsClopen (U := U) hclopen hdisj hunion).symm :
          (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)) → ConnectedComponents α)
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i
          (mk (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hx))) :
      ConnectedComponents α)
⊢ Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    ((equivOfIsClopen (U := U) hclopen hdisj hunion :
          (a : ConnectedComponents α) → (i : ι) × ConnectedComponents (↑(U i) : Type u))
        (mk x) :
      (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i
        (mk (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hx)) :
      (i : ι) × ConnectedComponents (↑(U i) : Type u))

Tactic:
apply (equivOfIsClopen hclopen hdisj hunion).symm.injective

Premises used: ConnectedComponents.equivOfIsClopen, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
i : ι
x : α
hx : x ∈ U i
⊢ Eq.{u + 1} (α := ConnectedComponents α)
    (((equivOfIsClopen (U := U) hclopen hdisj hunion).symm :
          (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)) → ConnectedComponents α)
        ((equivOfIsClopen (U := U) hclopen hdisj hunion :
            (a : ConnectedComponents α) → (i : ι) × ConnectedComponents (↑(U i) : Type u))
          (mk x)) :
      ConnectedComponents α)
    (((equivOfIsClopen (U := U) hclopen hdisj hunion).symm :
          (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)) → ConnectedComponents α)
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i
          (mk (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hx))) :
      ConnectedComponents α)

Tactic:
simp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
hconn : ∀ (i : ι), IsConnected (U i)
i : ι
x : α
hx : x ∈ U i
⊢ (equivOfIsClopenOfIsConnected (U := U) hclopen hdisj hunion hconn : (a : ConnectedComponents α) → ι) (mk x) = i

Tactic:
simp [equivOfIsClopenOfIsConnected, equivOfIsClopen_mk _ _ _ _ hx]

Premises used: ConnectedComponents.equivOfIsClopen_mk, ConnectedComponents.equivOfIsClopenOfIsConnected
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
n : ℕ
hn : 0 < n
inl :
  IsEmpty α →
    ∃ (U : Fin n → Set α),
      (∀ (i : Fin n), IsClopen (U i)) ∧
        (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin n), U i) univ
inr :
  Nonempty α →
    ∃ (U : Fin n → Set α),
      (∀ (i : Fin n), IsClopen (U i)) ∧
        (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin n), U i) univ
⊢ ∃ (U : Fin n → Set α),
    (∀ (i : Fin n), IsClopen (U i)) ∧
      (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin n), U i) univ

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
n : ℕ
hn : 0 < n
h : IsEmpty α
⊢ ∃ (U : Fin n → Set α),
    (∀ (i : Fin n), IsClopen (U i)) ∧
      (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin n), U i) univ

Tactic:
(not_finite (ConnectedComponents α)).elim

Premises used: False.elim, ConnectedComponents, not_finite
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
n : ℕ
hn : 0 < n
h : IsEmpty α
⊢ ∃ (U : Fin n → Set α),
    (∀ (i : Fin n), IsClopen (U i)) ∧
      (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin n), U i) univ

Tactic:
exact (not_finite (ConnectedComponents α)).elim

Premises used: False.elim, ConnectedComponents, not_finite
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
n : ℕ
hn : 0 < n
h : Nonempty α
inr :
  ∀ (hn : LT.lt (α := ℕ) 0 0),
    ∃ (U : Fin 0 → Set α),
      (∀ (i : Fin 0), IsClopen (U i)) ∧
        (∀ (i : Fin 0), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin 0), U i) univ
inr₁ :
  ∀ (n : ℕ) (hn : 0 < n + 1),
    ∃ (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 → Set α),
    (∀ (i : Fin n), IsClopen (U i)) ∧
      (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin n), U i) univ

Tactic:
obtain (_ | n) := n
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
hn : LT.lt (α := ℕ) 0 0
⊢ ∃ (U : Fin 0 → Set α),
    (∀ (i : Fin 0), IsClopen (U i)) ∧
      (∀ (i : Fin 0), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ Eq.{u + 1} (α := Set α) (⋃ (i : Fin 0), U i) univ

Tactic:
simp at hn
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
⊢ (∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), IsClopen.{u} (X := α) (![univ] i)) ∧
    (∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), Set.Nonempty.{u} (α := α) (![univ] i)) ∧
      Pairwise (onFun.{1, u + 1, 1} (β := Set α) Disjoint ![univ]) ∧
        Eq.{u + 1} (α := Set α) (⋃ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), ![univ] i) univ

Tactic:
simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]

Premises used: Set.iUnion_fin_add_one_eq_iUnion_succ, isClopen_univ
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
⊢ ∃ (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:
exact ⟨![.univ], by simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
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
inr :
  ∀ (U : Fin (n + 1) → Set α) (h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)) (h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty)
    (h₃ : Pairwise (Disjoint on U)) (h₄ : 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 + 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 ⟨U, h₁, h₂, h₃, h₄⟩ := IH
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
simp_rw : ¬∀ (x : Fin (n + 1)), ConnectedSpace.{u} (↑(U x) : Type u)
⊢ ∃ (i : Fin (n + 1)), ¬IsConnected (U i)

Tactic:
simp_rw [isConnected_iff_connectedSpace, ← not_forall]

Premises used: Classical.not_forall, isConnected_iff_connectedSpace
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
⊢ ¬∀ (x : Fin (n + 1)), ConnectedSpace.{u} (↑(U x) : Type u)

Tactic:
fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)

Premises used: Iff.mpr, Finite.of_equiv, not_finite_iff_infinite, ConnectedComponents.equivOfIsClopen, Set.Elem, Equiv.symm, ConnectedComponents, Not, Sigma
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
⊢ ¬∀ (x : Fin (n + 1)), ConnectedSpace.{u} (↑(U x) : Type u)

Tactic:
exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
inr :
  ∀ (i : Fin (n + 1)) (hi : ¬IsConnected (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:
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)
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
h : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : Eq.{u + 1} (α := Set α) (⋃ (i : Fin (n + 1)), U i) univ
i : Fin (n + 1)
hi : ¬IsConnected (U i)
inr :
  ∀ (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
⊢ ∃ (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 ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U

Premises used: Equiv.swap, Equiv.piCongrLeft, Equiv.surjective, Equiv.symm, OfNat.ofNat, rfl, Set
-- 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₁ :
  ∀ (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)
⊢ ∀ (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))

Tactic:
simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *

Premises used: Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero
-- 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₁ :
  ∀ (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)
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))
⊢ ∀ (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))

Tactic:
simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *

Premises used: Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero
-- 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₁ :
  ∀ (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)
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))
⊢ 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

Tactic:
simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *

Premises used: Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero
-- 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₁ :
  ∀ (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)
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
⊢ ¬IsConnected s

Tactic:
simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *

Premises used: Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero
-- 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
⊢ IsClopen s

Tactic:
simpa using h₁ i