awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι_1 : Type u_1
X : ι_1 → Type u_2
inst : TopologicalSpace α
s t u v : Set α
ι : 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 : ι), IsPreconnected (U i)
heq :
  ∀ {x : α} {i : ι} (hx : x ∈ U i),
    Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
      connectedComponent x
x : α
⊢ ∃ (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)),
    Eq (α := ConnectedComponents α)
      ((fun (x : (i : ι) × ConnectedComponents (↑(U i) : Type u)) ↦
          (match (motive := (i : ι) × ConnectedComponents (↑(U i) : Type u) → ConnectedComponents α) x with
            | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) ⋯ x :
            ConnectedComponents α))
        a)
      (mk x)
have refine_2 : ∀ (i : ι) (hi : x ∈ U i),
  ∃ (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)),
    Eq (α := ConnectedComponents α)
      ((fun (x : (i : ι) × ConnectedComponents (↑(U i) : Type u)) ↦
          (match (motive := (i : ι) × ConnectedComponents (↑(U i) : Type u) → ConnectedComponents α) x with
            | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) sorry x :
            ConnectedComponents α))
        a)
      (mk x)
Tactic: obtain ⟨i, hi⟩ := Set.iUnion_eq_univ_iff.mp hunion x
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι_1 : Type u_1
X : ι_1 → Type u_2
inst : TopologicalSpace α
s t u v : Set α
ι : 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 : ι), IsPreconnected (U i)
heq :
  ∀ {x : α} {i : ι} (hx : x ∈ U i),
    Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
      connectedComponent x
x : α
i : ι
hi : x ∈ U i
⊢ ∃ (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)),
    Eq (α := ConnectedComponents α)
      ((fun (x : (i : ι) × ConnectedComponents (↑(U i) : Type u)) ↦
          (match (motive := (i : ι) × ConnectedComponents (↑(U i) : Type u) → ConnectedComponents α) x with
            | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) ⋯ x :
            ConnectedComponents α))
        a)
      (mk x)
have refine_2 : ∃ (a : ι) (b : ConnectedComponents (↑(U a) : Type u)),
  Eq (α := ConnectedComponents α) (Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U a)) sorry b) (mk x)
Tactic: simp only [Sigma.exists]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι_1 : Type u_1
X : ι_1 → Type u_2
inst : TopologicalSpace α
s t u v : Set α
ι : 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 : ι), IsPreconnected (U i)
heq :
  ∀ {x : α} {i : ι} (hx : x ∈ U i),
    Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
      connectedComponent x
x : α
i : ι
hi : x ∈ U i
⊢ ∃ (a : ι) (b : ConnectedComponents (↑(U a) : Type u)),
    Eq (α := ConnectedComponents α) (Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U a)) ⋯ b) (mk x)
have h : Eq (α := ConnectedComponents α)
  (Quotient.lift (s := connectedComponentSetoid (↑(U i) : Type u)) (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) sorry
    (mk (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)))
  (mk x)
Tactic: use i, .mk ⟨x, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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 (α := (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))
have 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 α)
Tactic: apply (equivOfIsClopen hclopen hdisj hunion).symm.injective
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
n : ℕ
hn : 0 < n
⊢ ∃ (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
have 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
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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
⊢ ∃ (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
have 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
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Infinite.{u + 1} (ConnectedComponents α)
n : ℕ
hn : 0 < n
h : 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
have 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
Tactic: obtain (_ | n) := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain (_ | n) := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
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
⊢ ∃ (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 : ∀ (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
Tactic: obtain ⟨U, h₁, h₂, h₃, h₄⟩ := IH
Cleared hypotheses: IH
-- 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 α
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)), ¬IsConnected (U i)
have simp_rw : ¬∀ (x : Fin (n + 1)), ConnectedSpace.{u} (↑(U x) : Type u)
Tactic: simp_rw [isConnected_iff_connectedSpace, ← not_forall]
-- 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 α
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
have 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
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)
-- 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 α
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)
⊢ ∃ (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 : ∀ (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
Tactic: obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U
Cleared hypotheses: U, h₁, h₂, h₃, h₄, hi
-- 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)
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
have 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))
Tactic: simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
Cleared hypotheses: h₁, h₂, h₄, hi
-- 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)
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))
⊢ ∃ (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 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))
Tactic: simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
Cleared hypotheses: h₁, h₂, h₄, hi
-- 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)
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))
⊢ ∃ (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 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
Tactic: simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
Cleared hypotheses: h₁, h₂, h₄, hi
-- 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)
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
⊢ ∃ (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 hi₁ : ¬IsConnected s
Tactic: simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
Cleared hypotheses: h₁, h₂, h₄, hi