awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯) : α) ∈ s

Tactic:
exact hxs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
⊢ Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)

Tactic:
have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
    rw [mem_preimage]
    exact hxs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)

Tactic:
have := this.subset_connectedComponent h2xs
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
rw : s ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ s ⊆ connectedComponentIn F x

Tactic:
rw [connectedComponentIn_eq_image (hsF hxs)]

Premises used: connectedComponentIn_eq_image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
⊢ s ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)

Tactic:
Subset.trans ?_ (image_mono this)

Premises used: Set.Subset.trans, Set.image_mono
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
refine :
  s ⊆
    image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
⊢ s ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)

Tactic:
refine Subset.trans ?_ (image_mono this)

Premises used: Set.Subset.trans, Set.image_mono
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this_1 : IsPreconnected (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
h2xs :
  Membership.mem (γ := Set { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
this : Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s ⊆ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x ⋯)
rw : s ⊆ F ∩ s
rw₁ rw₂ : s ⊆ s
⊢ s ⊆
    image (α := { x : α // x ∈ F }) (Subtype.val (p := fun (x : α) ↦ x ∈ F))
      (Subtype.val (p := fun (x : α) ↦ x ∈ F) ⁻¹' s)

Tactic:
rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]

Premises used: Iff.mpr, Subtype.image_preimage_coe, Set.inter_eq_right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
s : Set α
H1 : IsConnected s
H2 : x ∈ s
⊢ s ⊆ connectedComponent x

Tactic:
H1.2.subset_connectedComponent H2

Premises used: And.right, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
h : IsPreconnected F
hx : x ∈ F
⊢ _root_.connectedComponentIn F x = F

Tactic:
(connectedComponentIn_subset F x).antisymm (h.subset_connectedComponentIn hx subset_rfl)

Premises used: connectedComponentIn_subset, HasSubset.Subset.antisymm, IsPreconnected.subset_connectedComponentIn, subset_rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
h : y ∈ connectedComponent x
⊢ connectedComponent x = connectedComponent y

Tactic:
eq_of_subset_of_subset (isConnected_connectedComponent.subset_connectedComponent h)
    (isConnected_connectedComponent.subset_connectedComponent
      (Set.mem_of_mem_of_subset mem_connectedComponent
        (isConnected_connectedComponent.subset_connectedComponent h)))

Premises used: isConnected_connectedComponent, mem_connectedComponent, Set.mem_of_mem_of_subset, Set.eq_of_subset_of_subset, IsConnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
⊢ connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y

Tactic:
⟨fun h => h ▸ mem_connectedComponent, fun h => (connectedComponent_eq h).symm⟩

Premises used: mem_connectedComponent, Eq.rec, connectedComponent_eq, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
⊢ x ∈ F

Tactic:
have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
simp_rw :
  ∀ (h : y ∈ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)),
    Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
      connectedComponentIn F y
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
simp_rw [connectedComponentIn_eq_image hx] at h ⊢

Premises used: connectedComponentIn_eq_image
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
F : Set α
hx : x ∈ F
h : y ∈ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)
obtain :
  ∀ (y : α) (hy : y ∈ F)
    (h2y :
      Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy ∈ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)),
    Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
      connectedComponentIn F (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy) : α)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F y

Tactic:
obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy ∈ connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx)
simp_rw simp_rw₁ :
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F y
simp_rw₂ :
  Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ F) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) =
    connectedComponentIn F (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ F) y hy) : α)

Tactic:
simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]

Premises used: connectedComponentIn_eq_image, connectedComponent_eq
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ connectedComponentIn univ x = connectedComponent x

Tactic:
subset_antisymm
    (isPreconnected_connectedComponentIn.subset_connectedComponent <|
      mem_connectedComponentIn trivial)
    (isPreconnected_connectedComponent.subset_connectedComponentIn mem_connectedComponent <|
      subset_univ _)

Premises used: trivial, Set.subset_univ, mem_connectedComponent, mem_connectedComponentIn, isPreconnected_connectedComponentIn, subset_antisymm, isPreconnected_connectedComponent, IsPreconnected.subset_connectedComponentIn, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x y : α
h : connectedComponent x ≠ connectedComponent y
⊢ Disjoint (connectedComponent x) (connectedComponent y)

Tactic:
Set.disjoint_left.2 fun _ h1 h2 =>
    h ((connectedComponent_eq h1).trans (connectedComponent_eq h2).symm)

Premises used: Iff.mpr, Set.disjoint_left, connectedComponent_eq, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsClosed[inst] (connectedComponent x)

Tactic:
closure_subset_iff_isClosed.1 <|
    isConnected_connectedComponent.closure.subset_connectedComponent <|
      subset_closure mem_connectedComponent

Premises used: closure_subset_iff_isClosed, subset_closure, isConnected_connectedComponent, mem_connectedComponent, IsConnected.closure, Iff.mp, IsConnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : Continuous[inst, inst_1] f
a : α
⊢ f '' connectedComponent a ⊆ connectedComponent (f a)

Tactic:
(isConnected_connectedComponent.image f h.continuousOn).subset_connectedComponent
    ((mem_image f (connectedComponent a) (f a)).2 ⟨a, mem_connectedComponent, rfl⟩)

Premises used: Iff.mpr, Continuous.continuousOn, IsConnected.image, isConnected_connectedComponent, mem_connectedComponent, Set.mem_image, connectedComponent, And.intro, Exists.intro, rfl, IsConnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
a : α
hf : Continuous[inst, inst_1] f
hx : a ∈ s
⊢ f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)

Tactic:
(isPreconnected_connectedComponentIn.image _ hf.continuousOn).subset_connectedComponentIn
    (mem_image_of_mem _ <| mem_connectedComponentIn hx)
    (image_mono <| connectedComponentIn_subset _ _)

Premises used: connectedComponentIn_subset, Continuous.continuousOn, Set.image_mono, mem_connectedComponentIn, IsPreconnected.image, isPreconnected_connectedComponentIn, Set.mem_image_of_mem, IsPreconnected.subset_connectedComponentIn
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : Continuous[inst, inst_1] f
a : α
⊢ MapsTo f (connectedComponent a) (connectedComponent (f a))

Tactic:
mapsTo_iff_image_subset.2 <| h.image_connectedComponent_subset a

Premises used: Iff.mpr, Continuous.image_connectedComponent_subset, Set.mapsTo_iff_image_subset
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : Continuous[inst, inst_1] f
a : α
hx : a ∈ s
⊢ MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a))

Tactic:
mapsTo_iff_image_subset.2 <| image_connectedComponentIn_subset h hx

Premises used: Iff.mpr, Continuous.image_connectedComponentIn_subset, Set.mapsTo_iff_image_subset
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ irreducibleComponent x ⊆ connectedComponent x

Tactic:
isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent

Premises used: mem_irreducibleComponent, isIrreducible_irreducibleComponent, IsIrreducible.isConnected, IsConnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
pos : ∀ (hx : x ∈ F), connectedComponentIn F x ⊆ connectedComponentIn G x
neg : ∀ (hx : x ∉ F), connectedComponentIn F x ⊆ connectedComponentIn G x
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
by_cases hx : x ∈ F
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
pos :
  Subtype.val (p := fun (x : α) ↦ x ∈ G) ''
      inclusion (s := F) (t := G) h '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) ⊆
    Subtype.val (p := fun (x : α) ↦ x ∈ G) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ G) x ⋯)
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
rw [connectedComponentIn_eq_image hx, connectedComponentIn_eq_image (h hx), ←
      show ((↑) : G → α) ∘ inclusion h = (↑) from rfl, image_comp]

Premises used: connectedComponentIn_eq_image, Set.image_comp, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ G) ''
      inclusion (s := F) (t := G) h '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) ⊆
    Subtype.val (p := fun (x : α) ↦ x ∈ G) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ G) x ⋯)

Tactic:
image_mono ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩)

Premises used: Set.image_mono, Continuous.image_connectedComponent_subset, Subtype.mk, continuous_inclusion
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ G) ''
      inclusion (s := F) (t := G) h '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ F) x hx) ⊆
    Subtype.val (p := fun (x : α) ↦ x ∈ G) '' connectedComponent (Subtype.mk (p := fun (x : α) ↦ x ∈ G) x ⋯)

Tactic:
exact image_mono ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩)

Premises used: Set.image_mono, Continuous.image_connectedComponent_subset, Subtype.mk, continuous_inclusion
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
neg : ∅ ⊆ connectedComponentIn G x
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
rw [connectedComponentIn_eq_empty hx]

Premises used: connectedComponentIn_eq_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ ∅ ⊆ connectedComponentIn G x

Tactic:
Set.empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ ∅ ⊆ connectedComponentIn G x

Tactic:
exact Set.empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
⊢ IsConnected.{u} (α := α) univ

Tactic:
⟨univ_nonempty, isPreconnected_univ⟩

Premises used: IsConnected, Set.univ_nonempty, And.intro, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
⊢ PreconnectedSpace α ↔ IsPreconnected.{u} (α := α) univ

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

Premises used: PreconnectedSpace.mk, Iff.intro, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
⊢ ConnectedSpace α ↔ IsConnected.{u} (α := α) univ

Tactic:
⟨fun h ↦ ⟨univ_nonempty, h.1.1⟩,
   fun h ↦ ConnectedSpace.mk (toPreconnectedSpace := ⟨h.2⟩) ⟨h.1.some⟩⟩

Premises used: Set.univ_nonempty, ConnectedSpace.mk, Nonempty.intro, And.left, And.intro, Iff.intro, PreconnectedSpace.isPreconnected_univ, Set.Nonempty.some
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PreconnectedSpace α
f : α → β
h : Continuous[inst, inst_1] f
⊢ IsPreconnected (range f)

Tactic:
@image_univ _ _ f ▸ isPreconnected_univ.image _ h.continuousOn

Premises used: Set.image_univ, Continuous.continuousOn, IsPreconnected.image, Eq.rec, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : ConnectedSpace α
f : α → β
h : Continuous[inst, inst_1] f
⊢ IsConnected (range f)

Tactic:
⟨range_nonempty f, isPreconnected_range h⟩

Premises used: IsConnected, isPreconnected_range, Set.range_nonempty, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst, inst_2] f
rw : IsConnected (range f)
⊢ ConnectedSpace β

Tactic:
rw [connectedSpace_iff_univ, ← hf.range_eq]

Premises used: Function.Surjective.range_eq, connectedSpace_iff_univ
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst, inst_2] f
⊢ IsConnected (range f)

Tactic:
isConnected_range hf'

Premises used: isConnected_range
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst, inst_2] f
⊢ IsConnected (range f)

Tactic:
exact isConnected_range hf'

Premises used: isConnected_range
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α ≃ₜ β
⊢ ConnectedSpace α ↔ ConnectedSpace β

Tactic:
⟨fun _ ↦ e.surjective.connectedSpace e.continuous,
    fun _ ↦ e.symm.surjective.connectedSpace e.symm.continuous⟩

Premises used: Homeomorph.continuous, Function.Surjective.connectedSpace, Homeomorph.symm, Iff.intro, Homeomorph.surjective
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
s : Setoid α
inst_1 : ConnectedSpace α
⊢ ConnectedSpace.{u} (Quotient s)

Tactic:
Quotient.mk'_surjective.connectedSpace continuous_coinduced_rng

Premises used: Quotient.mk'_surjective, Function.Surjective.connectedSpace, continuous_coinduced_rng
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PreconnectedSpace α
f : α → β
hf : DenseRange f
hc : Continuous[inst, inst_1] f
⊢ PreconnectedSpace β

Tactic:
⟨hf.closure_eq ▸ (isPreconnected_range hc).closure⟩

Premises used: isPreconnected_range, PreconnectedSpace.mk, Eq.rec, IsPreconnected.closure, Dense.closure_eq
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
mp : ConnectedSpace α → ∃ (x : α), connectedComponent x = univ
mpr : (∃ (x : α), connectedComponent x = univ) → ConnectedSpace α
⊢ ConnectedSpace α ↔ ∃ (x : α), connectedComponent x = univ

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
toPreconnectedSpace : PreconnectedSpace α
x : α
⊢ ∃ (x : α), connectedComponent x = univ

Tactic:
⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩

Premises used: Set.eq_univ_of_univ_subset, Exists.intro, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
toPreconnectedSpace : PreconnectedSpace α
x : α
⊢ ∃ (x : α), connectedComponent x = univ

Tactic:
exact
      ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
rw : IsPreconnected (connectedComponent x)
⊢ IsPreconnected.{u} (α := α) univ

Tactic:
rw [← h]
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)

Tactic:
isPreconnected_connectedComponent

Premises used: isPreconnected_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)

Tactic:
exact isPreconnected_connectedComponent

Premises used: isPreconnected_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ PreconnectedSpace α

Tactic:
haveI : PreconnectedSpace α :=
      ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α

Tactic:
⟨⟨x⟩⟩

Premises used: ConnectedSpace.mk, Nonempty.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α

Tactic:
exact ⟨⟨x⟩⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
mp : PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ
mpr : (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α
⊢ PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = univ

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ

Tactic:
eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)

Premises used: Set.eq_univ_of_univ_subset, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ

Tactic:
exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)

Premises used: Set.eq_univ_of_univ_subset, Set.mem_univ, PreconnectedSpace.isPreconnected_univ, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
mpr : ∀ (hα : IsEmpty α), PreconnectedSpace α
mpr₁ : ∀ (hα : Nonempty α), PreconnectedSpace α
⊢ PreconnectedSpace α

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
rw : IsPreconnected.{u} (α := α) ∅
⊢ IsPreconnected.{u} (α := α) univ

Tactic:
rw [univ_eq_empty_iff.mpr hα]

Premises used: Iff.mpr, Set.univ_eq_empty_iff
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected.{u} (α := α) ∅

Tactic:
isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected.{u} (α := α) ∅

Tactic:
exact isPreconnected_empty

Premises used: isPreconnected_empty