awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
x y : ℝ
⊢ ContinuousMap.toFun (X := (↑I : Type))
      { toFun := fun (t : (↑I : Type)) ↦ (1 - (↑t : ℝ)) * x + (↑t : ℝ) * y, continuous_toFun := ⋯ : C((↑I : Type), ℝ) }
      0 =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
x y : ℝ
⊢ ContinuousMap.toFun (X := (↑I : Type))
      { toFun := fun (t : (↑I : Type)) ↦ (1 - (↑t : ℝ)) * x + (↑t : ℝ) * y, continuous_toFun := ⋯ : C((↑I : Type), ℝ) }
      1 =
    y

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ PathConnectedSpace X ↔ ∃ (x : X), pathComponent x = univ

Tactic:
simp [pathConnectedSpace_iff_univ, isPathConnected_iff_eq]

Premises used: isPathConnected_iff_eq, pathConnectedSpace_iff_univ
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
rw : ∃ (x : X), connectedComponent x = univ
⊢ ConnectedSpace X

Tactic:
rw [connectedSpace_iff_connectedComponent]

Premises used: connectedSpace_iff_connectedComponent
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
rcases :
  ∀ (x : X) (_x_in : Membership.mem (γ := Set X) univ x) (hx : pathComponentIn univ x = univ),
    ∃ (x : X), connectedComponent x = univ
⊢ ∃ (x : X), connectedComponent x = univ

Tactic:
rcases isPathConnected_iff_eq.mp (pathConnectedSpace_iff_univ.mp ‹_›) with ⟨x, _x_in, hx⟩

Premises used: isPathConnected_iff_eq, pathConnectedSpace_iff_univ, Iff.mp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
x : X
_x_in : Membership.mem (γ := Set X) univ x
hx : pathComponentIn univ x = univ
h : connectedComponent x = univ
⊢ ∃ (x : X), connectedComponent x = univ

Tactic:
use x
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
x : X
_x_in : Membership.mem (γ := Set X) univ x
hx : pathComponentIn univ x = univ
h : univ ⊆ connectedComponent x
⊢ connectedComponent x = univ

Tactic:
rw [← univ_subset_iff]

Premises used: Set.univ_subset_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
x : X
_x_in : Membership.mem (γ := Set X) univ x
hx : pathComponentIn univ x = univ
⊢ pathComponent x = univ

Tactic:
simpa using hx
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
x : X
_x_in : Membership.mem (γ := Set X) univ x
hx : pathComponentIn univ x = univ
⊢ univ ⊆ connectedComponent x

Tactic:
exact (by simpa using hx : pathComponent x = univ) ▸ pathComponent_subset_component x
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
hF : IsPathConnected F
rw : ConnectedSpace.{u_1} (↑F : Type u_1)
⊢ IsConnected F

Tactic:
rw [isConnected_iff_connectedSpace]

Premises used: isConnected_iff_connectedSpace
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ PathConnectedSpace.{u_1} (↑F : Type u_1)

Tactic:
rw [isPathConnected_iff_pathConnectedSpace] at hF

Premises used: isPathConnected_iff_pathConnectedSpace
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
hF : PathConnectedSpace.{u_1} (↑F : Type u_1)
⊢ ConnectedSpace.{u_1} (↑F : Type u_1)

Tactic:
@PathConnectedSpace.connectedSpace _ _ hF

Premises used: PathConnectedSpace.connectedSpace
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
hF : PathConnectedSpace.{u_1} (↑F : Type u_1)
⊢ ConnectedSpace.{u_1} (↑F : Type u_1)

Tactic:
exact @PathConnectedSpace.connectedSpace _ _ hF

Premises used: PathConnectedSpace.connectedSpace
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ PathConnectedSpace X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ IsPathConnected.{u_1} (X := X) univ

Tactic:
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
rcases :
  ∀ (γ : Path (p 0) (p (last n)))
    (h :
      ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)),
    ∃ (γ : Path (p 0) (p (last n))),
      ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
⊢ ∃ (γ : Path (p 0) (p (last n))),
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)

Tactic:
rcases this.exists_path_through_family p fun _i => True.intro with ⟨γ, -, h⟩

Premises used: IsPathConnected.exists_path_through_family, True.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
γ : Path (p 0) (p (last n))
h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
⊢ ∃ (γ : Path (p 0) (p (last n))),
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)

Tactic:
⟨γ, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
γ : Path (p 0) (p (last n))
h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
⊢ ∃ (γ : Path (p 0) (p (last n))),
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)

Tactic:
exact ⟨γ, h⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
rcases :
  ∀ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type))
    (h : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i),
    ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
      ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩

Premises used: IsPathConnected.exists_path_through_family', True.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
γ : Path (p 0) (p (last n))
t : Fin (n + 1) → (↑I : Type)
h : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
⟨γ, t, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
γ : Path (p 0) (p (last n))
t : Fin (n + 1) → (↑I : Type)
h : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
exact ⟨γ, t, h⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
h : ∀ (y : X), Membership.mem (γ := Set X) (preimage (β := ZerothHomotopy X) mk {mk x}) y ↔ y ∈ pathComponent x
⊢ preimage (β := ZerothHomotopy X) mk {mk x} = pathComponent x

Tactic:
ext y
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : Eq (α := ZerothHomotopy X) (mk x) (mk y) ↔ Joined x y
⊢ Membership.mem (γ := Set X) (preimage (β := ZerothHomotopy X) mk {mk x}) y ↔ y ∈ pathComponent x

Tactic:
rw [mem_preimage, mem_singleton_iff, eq_comm, mem_pathComponent_iff]

Premises used: mem_pathComponent_iff, eq_comm, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Eq (α := ZerothHomotopy X) (mk x) (mk y) ↔ Joined x y

Tactic:
Quotient.eq

Premises used: ZerothHomotopy, ZerothHomotopy.mk, Quotient.eq
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Eq (α := ZerothHomotopy X) (mk x) (mk y) ↔ Joined x y

Tactic:
exact Quotient.eq

Premises used: Quotient.eq
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : CompactSpace X
⊢ CompactSpace.{u_1} (ZerothHomotopy X)

Tactic:
Quotient.compactSpace

Premises used: Quotient.compactSpace, ZerothHomotopy
-- Module: Mathlib.Topology.Connected.Separation
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TotallySeparatedSpace X
x y : X
h : x ≠ y
obtain :
  ∀ (u v : Set X) (h₁ : IsOpen u) (h₂ : IsOpen v) (h₃ : x ∈ u) (h₄ : y ∈ v),
    Set.univ ⊆ u ∪ v →
      ∀ (h₅ : Disjoint u v), ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨u, v, h₁, h₂, h₃, h₄, _, h₅⟩ := isTotallySeparated_univ trivial trivial h

Premises used: trivial, TotallySeparatedSpace.isTotallySeparated_univ
-- Module: Mathlib.Topology.Connected.Separation
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TotallySeparatedSpace X
x y : X
h : x ≠ y
u v : Set X
h₁ : IsOpen u
h₂ : IsOpen v
h₃ : x ∈ u
h₄ : y ∈ v
left : Set.univ ⊆ u ∪ v
h₅ : Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
⟨u, v, h₁, h₂, h₃, h₄, h₅⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Separation
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TotallySeparatedSpace X
x y : X
h : x ≠ y
u v : Set X
h₁ : IsOpen u
h₂ : IsOpen v
h₃ : x ∈ u
h₄ : y ∈ v
left : Set.univ ⊆ u ∪ v
h₅ : Disjoint u v
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
exact ⟨u, v, h₁, h₂, h₃, h₄, h₅⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ IsTotallyDisconnected.{u} (α := α) ∅

Tactic:
fun _ ht _ _ x_in _ _ =>
  (ht x_in).elim

Premises used: False.elim, Set.Subsingleton, IsTotallyDisconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsTotallyDisconnected (α := α) {x}

Tactic:
fun _ ht _ =>
  subsingleton_singleton.anti ht

Premises used: Set.subsingleton_singleton, Set.Subsingleton.anti, IsTotallyDisconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : TotallyDisconnectedSpace α
s : Set α
h : IsPreconnected s
⊢ s.Subsingleton

Tactic:
TotallyDisconnectedSpace.isTotallyDisconnected_univ s (subset_univ s) h

Premises used: Set.subset_univ, TotallyDisconnectedSpace.isTotallyDisconnected_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
inst_2 : TotallyDisconnectedSpace α
⊢ Subsingleton α

Tactic:
Set.subsingleton_of_univ_subsingleton isPreconnected_univ.subsingleton

Premises used: Set.subsingleton_of_univ_subsingleton, IsPreconnected.subsingleton, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α_1 : Type u
β_1 : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u_3
β : α → Type u_4
inst_1 : (a : α) → TopologicalSpace (β a)
inst_2 : ∀ (a : α), TotallyDisconnectedSpace.{u_4} (β a)
⊢ TotallyDisconnectedSpace ((a : α) → β a)

Tactic:
⟨fun t _ h2 =>
    have this : ∀ a, IsPreconnected ((fun x : ∀ a, β a => x a) '' t) := fun a =>
      h2.image (fun x => x a) (continuous_apply a).continuousOn
    fun x x_in y y_in => funext fun a => (this a).subsingleton ⟨x, x_in, rfl⟩ ⟨y, y_in, rfl⟩⟩

Premises used: TotallyDisconnectedSpace.mk, Continuous.continuousOn, IsPreconnected.image, IsPreconnected.subsingleton, funext, And.intro, Exists.intro, continuous_apply, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
⊢ TotallyDisconnectedSpace (α × β)

Tactic:
⟨fun t _ h2 =>
    have H1 : IsPreconnected (Prod.fst '' t) := h2.image Prod.fst continuous_fst.continuousOn
    have H2 : IsPreconnected (Prod.snd '' t) := h2.image Prod.snd continuous_snd.continuousOn
    fun x hx y hy =>
    Prod.ext (H1.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩)
      (H2.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩)⟩

Premises used: TotallyDisconnectedSpace.mk, Continuous.continuousOn, IsPreconnected.image, continuous_snd, continuous_fst, IsPreconnected.subsingleton, Prod.fst, Prod.ext, And.intro, Exists.intro, Prod.snd, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
⊢ TotallyDisconnectedSpace (α ⊕ β)

Tactic:
⟨fun s _ hs => ?_⟩

Premises used: TotallyDisconnectedSpace.mk
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
refine : ∀ s ⊆ univ, ∀ (hs : IsPreconnected s), s.Subsingleton
⊢ TotallyDisconnectedSpace (α ⊕ β)

Tactic:
refine ⟨fun s _ hs => ?_⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
s : Set (α ⊕ β)
h : s ⊆ univ
hs : IsPreconnected s
inl :
  ∀ (t : Set α) (ht : IsPreconnected t),
    Subset (α := Set (α ⊕ β)) (Sum.inl '' t) univ →
      ∀ (hs : IsPreconnected (α := α ⊕ β) (Sum.inl '' t)), Set.Subsingleton (α := α ⊕ β) (Sum.inl '' t)
inr :
  ∀ (t : Set β) (ht : IsPreconnected t),
    Subset (α := Set (α ⊕ β)) (Sum.inr '' t) univ →
      ∀ (hs : IsPreconnected (α := α ⊕ β) (Sum.inr '' t)), Set.Subsingleton (α := α ⊕ β) (Sum.inr '' t)
⊢ s.Subsingleton

Tactic:
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isPreconnected_iff.1 hs

Premises used: Iff.mp, Sum.isPreconnected_iff, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t_1 u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
t : Set α
ht : IsPreconnected t
h : Subset (α := Set (α ⊕ β)) (Sum.inl '' t) univ
hs : IsPreconnected (α := α ⊕ β) (Sum.inl '' t)
⊢ Set.Subsingleton (α := α ⊕ β) (Sum.inl '' t)

Tactic:
ht.subsingleton.image _

Premises used: Set.Subsingleton.image, IsPreconnected.subsingleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t_1 u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
t : Set α
ht : IsPreconnected t
h : Subset (α := Set (α ⊕ β)) (Sum.inl '' t) univ
hs : IsPreconnected (α := α ⊕ β) (Sum.inl '' t)
⊢ Set.Subsingleton (α := α ⊕ β) (Sum.inl '' t)

Tactic:
exact ht.subsingleton.image _

Premises used: Set.Subsingleton.image, IsPreconnected.subsingleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t_1 u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
t : Set β
ht : IsPreconnected t
h : Subset (α := Set (α ⊕ β)) (Sum.inr '' t) univ
hs : IsPreconnected (α := α ⊕ β) (Sum.inr '' t)
⊢ Set.Subsingleton (α := α ⊕ β) (Sum.inr '' t)

Tactic:
ht.subsingleton.image _

Premises used: Set.Subsingleton.image, IsPreconnected.subsingleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t_1 u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
t : Set β
ht : IsPreconnected t
h : Subset (α := Set (α ⊕ β)) (Sum.inr '' t) univ
hs : IsPreconnected (α := α ⊕ β) (Sum.inr '' t)
⊢ Set.Subsingleton (α := α ⊕ β) (Sum.inr '' t)

Tactic:
exact ht.subsingleton.image _

Premises used: Set.Subsingleton.image, IsPreconnected.subsingleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
⊢ TotallyDisconnectedSpace ((i : ι) × X i)

Tactic:
⟨fun s _ hs => ?_⟩

Premises used: TotallyDisconnectedSpace.mk
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
refine : ∀ s ⊆ univ, ∀ (hs : IsPreconnected s), s.Subsingleton
⊢ TotallyDisconnectedSpace ((i : ι) × X i)

Tactic:
refine ⟨fun s _ hs => ?_⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
s : Set ((i : ι) × X i)
h : s ⊆ univ
hs : IsPreconnected s
inl :
  Subset (α := Set ((i : ι) × X i)) ∅ univ →
    ∀ (hs : IsPreconnected (α := (i : ι) × X i) ∅), Set.Subsingleton (α := (i : ι) × X i) ∅
inr : ∀ (h : s.Nonempty), s.Subsingleton
⊢ s.Subsingleton

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
h : Subset (α := Set ((i : ι) × X i)) ∅ univ
hs : IsPreconnected (α := (i : ι) × X i) ∅
⊢ Set.Subsingleton (α := (i : ι) × X i) ∅

Tactic:
subsingleton_empty

Premises used: Set.subsingleton_empty
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
h : Subset (α := Set ((i : ι) × X i)) ∅ univ
hs : IsPreconnected (α := (i : ι) × X i) ∅
⊢ Set.Subsingleton (α := (i : ι) × X i) ∅

Tactic:
exact subsingleton_empty

Premises used: Set.subsingleton_empty
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
s : Set ((i : ι) × X i)
h_1 : s ⊆ univ
hs : IsPreconnected s
h : s.Nonempty
inr :
  ∀ (a : ι) (t : Set (X a)) (ht : IsConnected t),
    Sigma.mk (β := fun (i : ι) ↦ X i) a '' t ⊆ univ →
      ∀ (hs : IsPreconnected (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t))
        (h : (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty),
        (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Subsingleton
⊢ s.Subsingleton

Tactic:
obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩

Premises used: And.intro, Iff.mp, Sigma.isConnected_iff, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t_1 u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
a : ι
t : Set (X a)
ht : IsConnected t
h_1 : Sigma.mk (β := fun (i : ι) ↦ X i) a '' t ⊆ univ
hs : IsPreconnected (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t)
h : (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty
⊢ (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Subsingleton

Tactic:
ht.isPreconnected.subsingleton.image _

Premises used: Set.Subsingleton.image, IsPreconnected.subsingleton, IsConnected.isPreconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t_1 u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
a : ι
t : Set (X a)
ht : IsConnected t
h_1 : Sigma.mk (β := fun (i : ι) ↦ X i) a '' t ⊆ univ
hs : IsPreconnected (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t)
h : (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Nonempty
⊢ (Sigma.mk (β := fun (i : ι) ↦ X i) a '' t).Subsingleton

Tactic:
exact ht.isPreconnected.subsingleton.image _

Premises used: Set.Subsingleton.image, IsPreconnected.subsingleton, IsConnected.isPreconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
mp : TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton
mpr : (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
mp : connectedComponent x ⊆ univ
mp₁ : IsPreconnected (connectedComponent x)
⊢ (connectedComponent x).Subsingleton

Tactic:
apply h.1

Premises used: TotallyDisconnectedSpace.isTotallyDisconnected_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ

Tactic:
subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Tactic:
isPreconnected_connectedComponent

Premises used: isPreconnected_connectedComponent