awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ IsEmpty.{u + 1} (ConnectedComponents α) ↔ IsEmpty α
have rw : ¬IsEmpty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
Tactic: rw [← not_iff_not, not_isEmpty_iff, not_isEmpty_iff, nonempty_iff_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : ¬IsEmpty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
⊢ IsEmpty.{u + 1} (ConnectedComponents α) ↔ IsEmpty α
have rw₁ : Nonempty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
Tactic: rw [← not_iff_not, not_isEmpty_iff, not_isEmpty_iff, nonempty_iff_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : ¬IsEmpty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
rw₁ : Nonempty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
⊢ IsEmpty.{u + 1} (ConnectedComponents α) ↔ IsEmpty α
have rw₂ : Nonempty.{u + 1} (ConnectedComponents α) ↔ Nonempty α
Tactic: rw [← not_iff_not, not_isEmpty_iff, not_isEmpty_iff, nonempty_iff_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : ¬IsEmpty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
rw₁ : Nonempty.{u + 1} (ConnectedComponents α) ↔ ¬IsEmpty α
rw₂ : Nonempty.{u + 1} (ConnectedComponents α) ↔ Nonempty α
⊢ IsEmpty.{u + 1} (ConnectedComponents α) ↔ IsEmpty α
have rw₃ : Nonempty α ↔ Nonempty α
Tactic: rw [← not_iff_not, not_isEmpty_iff, not_isEmpty_iff, nonempty_iff_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
⊢ Subsingleton.{u + 1} (ConnectedComponents α)
have refine : ∀ (x y : ConnectedComponents α), x = y
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
x y : ConnectedComponents α
⊢ x = y
have obtain : ∀ (x : α), mk x = y
Tactic: obtain ⟨x, rfl⟩ := surjective_coe x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
y : ConnectedComponents α
x : α
⊢ mk x = y
have obtain : ∀ (y : α), Eq (α := ConnectedComponents α) (mk x) (mk y)
Tactic: obtain ⟨y, rfl⟩ := surjective_coe y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : PreconnectedSpace α
x y : α
⊢ Eq (α := ConnectedComponents α) (mk x) (mk y)
have simp_rw : connectedComponent x = connectedComponent y
Tactic: simp_rw [coe_eq_coe, PreconnectedSpace.connectedComponent_eq_univ, ]
-- 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)
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
have rw : connectedComponentIn (U i) x = connectedComponent x
Tactic: rw [← connectedComponentIn_eq_image hx, (hclopen i).connectedComponentIn_eq hx]
-- 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)
x : α
i : ι
hx : x ∈ U i
rw : connectedComponentIn (U i) x = connectedComponent x
⊢ Subtype.val (p := Membership.mem (U i)) '' connectedComponent (Subtype.mk (p := Membership.mem (U i)) x hx) =
    connectedComponent x
have rw₁ : connectedComponent x = connectedComponent x
Tactic: rw [← connectedComponentIn_eq_image hx, (hclopen i).connectedComponentIn_eq hx]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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)
⊢ ConnectedComponents α ≃ (i : ι) × ConnectedComponents (↑(U i) : Type u)
have 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
Tactic: haveI heq {x : α} {i} (hx : x ∈ U i) :
      Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x := by
    rw [← connectedComponentIn_eq_image hx, (hclopen i).connectedComponentIn_eq hx]
-- 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
⊢ ConnectedComponents α ≃ (i : ι) × ConnectedComponents (↑(U i) : Type u)
have refine_1 : ∀ (x x : (i : ι) × ConnectedComponents (↑(U i) : Type u)) (i : ι) (x : ConnectedComponents (↑(U i) : Type u)) (j : ι)
  (y : ConnectedComponents (↑(U j) : Type u)),
  Eq.{u + 1} (α := 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 α))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i x))
      ((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 α))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)) →
    Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)
Tactic: refine .symm <| .ofBijective
      (fun ⟨i, x⟩ ↦
        x.lift (ConnectedComponents.mk ∘ Subtype.val)
          (fun x y (hxy : connectedComponent x = connectedComponent y) ↦ by
            simp [← heq x.2, ← heq y.2, hxy]))
      ⟨fun ⟨i, x⟩ ⟨j, y⟩ ↦ ?_, fun 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
refine_1 :
  ∀ (x x : (i : ι) × ConnectedComponents (↑(U i) : Type u)) (i : ι) (x : ConnectedComponents (↑(U i) : Type u)) (j : ι)
    (y : ConnectedComponents (↑(U j) : Type u)),
    Eq.{u + 1} (α := 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 α))
          (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i x))
        ((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 α))
          (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)) →
      Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i x)
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)
⊢ ConnectedComponents α ≃ (i : ι) × ConnectedComponents (↑(U i) : Type u)
have refine_2 : ∀ (x : ConnectedComponents α),
  ∃ (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)),
    (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 =
      x
Tactic: refine .symm <| .ofBijective
      (fun ⟨i, x⟩ ↦
        x.lift (ConnectedComponents.mk ∘ Subtype.val)
          (fun x y (hxy : connectedComponent x = connectedComponent y) ↦ by
            simp [← heq x.2, ← heq y.2, hxy]))
      ⟨fun ⟨i, x⟩ ⟨j, y⟩ ↦ ?_, fun 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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i : ι
x : ConnectedComponents (↑(U i) : Type u)
j : ι
y : ConnectedComponents (↑(U j) : Type u)
hxy :
  Eq.{u + 1} (α := 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 α))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i x))
    ((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 α))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y))
⊢ Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i x)
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)
have refine_1 : ∀ (x : (↑(U i) : Type u))
  (hxy :
    Eq.{u + 1} (α := 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 α))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x)))
      ((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 α))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y))),
  Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)
Tactic: obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
Cleared hypotheses: x, hxy
-- 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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i j : ι
y : ConnectedComponents (↑(U j) : Type u)
x : (↑(U i) : Type u)
hxy :
  Eq.{u + 1} (α := 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 α))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x)))
    ((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 α))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y))
⊢ Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j y)
have refine_1 : ∀ (y : (↑(U j) : Type u))
  (hxy :
    Eq.{u + 1} (α := 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 α))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x)))
      ((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 α))
        (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j (mk y)))),
  Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j (mk y))
Tactic: obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i j : ι
x : (↑(U i) : Type u)
y : (↑(U j) : Type u)
hxy :
  Eq.{u + 1} (α := 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 α))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x)))
    ((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 α))
      (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j (mk y)))
⊢ Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j (mk y))
have hxy₁ : Eq (α := ConnectedComponents α) (mk (↑x : α)) (mk (↑y : α))
Tactic: replace hxy : ConnectedComponents.mk x.val = ConnectedComponents.mk y.val := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i j : ι
x : (↑(U i) : Type u)
y : (↑(U j) : Type u)
hxy : Eq (α := ConnectedComponents α) (mk (↑x : α)) (mk (↑y : α))
⊢ Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j (mk y))
have hxy₁ : connectedComponent (↑x : α) = connectedComponent (↑y : α)
Tactic: rw [ConnectedComponents.coe_eq_coe] at hxy
Cleared hypotheses: hxy
-- 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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i j : ι
x : (↑(U i) : Type u)
y : (↑(U j) : Type u)
hxy : connectedComponent (↑x : α) = connectedComponent (↑y : α)
⊢ i = j
have apply : ¬(Disjoint on U) i j
Tactic: apply hdisj.eq
-- 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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i j : ι
x : (↑(U i) : Type u)
y : (↑(U j) : Type u)
hxy : connectedComponent (↑x : α) = connectedComponent (↑y : α)
⊢ ¬(Disjoint on U) i j
have rw : ∃ x ∈ U i, x ∈ U j
Tactic: rw [Set.not_disjoint_iff]
-- 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_1 x_2 : (i : ι) × ConnectedComponents (↑(U i) : Type u)
i j : ι
x : (↑(U i) : Type u)
y : (↑(U j) : Type u)
hxy : connectedComponent (↑x : α) = connectedComponent (↑y : α)
⊢ Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) j (mk y))
have refine_1 : ∀ (y : (↑(U i) : Type u)) (hxy : connectedComponent (↑x : α) = connectedComponent (↑y : α)),
  Eq (α := (i : ι) × ConnectedComponents (↑(U i) : Type u))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk x))
    (Sigma.mk (β := fun (i : ι) ↦ ConnectedComponents (↑(U i) : Type u)) i (mk y))
Tactic: obtain rfl : i = j := by
      apply hdisj.eq
      rw [Set.not_disjoint_iff]
      exact ⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩
Cleared hypotheses: j, y, hxy
-- 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 : ConnectedComponents α
⊢ ∃ (a : (i : ι) × ConnectedComponents (↑(U i) : Type u)),
    (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 =
      x
have refine_2 : ∀ (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)) sorry x :
            ConnectedComponents α))
        a)
      (mk x)
Tactic: obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
Cleared hypotheses: x