awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
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)
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)) ⋯ x :
              ConnectedComponents α))
          a =
        x
⊢ ConnectedComponents α ≃ (i : ι) × ConnectedComponents (↑(U i) : Type u)

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 ↦ ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
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))
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)) ⋯ 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)
⊢ 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:
obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.Clopen
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))
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)) ⋯ 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))
⊢ 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 ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.Clopen
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 (α := ConnectedComponents α) (mk (↑x : α)) (mk (↑y : α))

Tactic:
replace hxy : ConnectedComponents.mk x.val = ConnectedComponents.mk y.val := hxy
-- Module: Mathlib.Topology.Connected.Clopen
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 : α))
⊢ connectedComponent (↑x : α) = connectedComponent (↑y : α)

Tactic:
rw [ConnectedComponents.coe_eq_coe] at hxy

Premises used: ConnectedComponents.coe_eq_coe
-- Module: Mathlib.Topology.Connected.Clopen
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 : α)
apply : ¬(Disjoint on U) i j
⊢ i = j

Tactic:
apply hdisj.eq

Premises used: Pairwise.eq
-- Module: Mathlib.Topology.Connected.Clopen
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 : α)
rw : ∃ x ∈ U i, x ∈ U j
⊢ ¬(Disjoint on U) i j

Tactic:
rw [Set.not_disjoint_iff]

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.Topology.Connected.Clopen
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 : α)
⊢ ∃ x ∈ U i, x ∈ U j

Tactic:
⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩

Premises used: mem_connectedComponent, Eq.rec, IsClopen.connectedComponent_subset, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Connected.Clopen
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 : α)
⊢ ∃ x ∈ U i, x ∈ U j

Tactic:
exact ⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩
-- Module: Mathlib.Topology.Connected.Clopen
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 : α)
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))
⊢ 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 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)⟩

Premises used: rfl
-- Module: Mathlib.Topology.Connected.Clopen
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 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:
simp [← Set.image_val_inj, heq, hxy]

Premises used: Set.image_val_inj
-- Module: Mathlib.Topology.Connected.Clopen
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 α
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)) ⋯ x :
              ConnectedComponents α))
          a)
        (mk x)
⊢ ∃ (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

Tactic:
obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.Clopen
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 : α
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)) ⋯ x :
              ConnectedComponents α))
          a)
        (mk 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)

Tactic:
obtain ⟨i, hi⟩ := Set.iUnion_eq_univ_iff.mp hunion x

Premises used: Set.iUnion_eq_univ_iff, Iff.mp
-- Module: Mathlib.Topology.Connected.Clopen
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
refine_2 :
  ∃ (a : ι) (b : ConnectedComponents (↑(U a) : Type u)),
    Eq (α := ConnectedComponents α) (Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U a)) ⋯ b) (mk 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)

Tactic:
simp only [Sigma.exists]

Premises used: Sigma.exists
-- Module: Mathlib.Topology.Connected.Clopen
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
h :
  Eq (α := ConnectedComponents α)
    (Quotient.lift (s := connectedComponentSetoid (↑(U i) : Type u)) (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) ⋯
      (mk (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)))
    (mk x)
⊢ ∃ (a : ι) (b : ConnectedComponents (↑(U a) : Type u)),
    Eq (α := ConnectedComponents α) (Quotient.lift (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U a)) ⋯ b) (mk x)

Tactic:
use i, .mk ⟨x, hi⟩
-- Module: Mathlib.Topology.Connected.Clopen
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
⊢ Eq (α := ConnectedComponents α)
    (Quotient.lift (s := connectedComponentSetoid (↑(U i) : Type u)) (mk ∘ Subtype.val (p := fun (x : α) ↦ x ∈ U i)) ⋯
      (mk (Subtype.mk (p := fun (x : α) ↦ x ∈ U i) x hi)))
    (mk x)

Tactic:
rfl
-- 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 : (↑(U i) : Type u)
⊢ Eq.{u + 1} (α := 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 x)) :
      ConnectedComponents α)
    (mk (↑x : α) : ConnectedComponents α)

Tactic:
rfl

Premises used: ConnectedComponents.mk, rfl