awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ

Tactic:
exact (v_op.preimage continuous_subtype_val).isClosed_compl

Premises used: continuous_subtype_val, IsOpen.isClosed_compl, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
u_op.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
exact u_op.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ ContinuousOn u.boolIndicator s

Tactic:
have : ContinuousOn u.boolIndicator s := by
    apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
    · rw [preimage_subtype_coe_eq_compl hsuv H]
      exact (v_op.preimage continuous_subtype_val).isClosed_compl
    · exact u_op.preimage continuous_subtype_val
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
this : ContinuousOn u.boolIndicator s
⊢ False

Tactic:
simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.notMem_iff_boolIndicator _).mp hy] using
    hs _ this x x_in_s y y_in_s

Premises used: Set.mem_iff_boolIndicator, Set.notMem_iff_boolIndicator, Iff.mp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
hs : ∀ (f : α → Bool), Continuous[inst, _] f → ∀ (x y : α), f x = f y
⊢ PreconnectedSpace α

Tactic:
⟨isPreconnected_of_forall_constant fun f hf x _ y _ =>
      hs f (continuousOn_univ.mp hf) x y⟩

Premises used: PreconnectedSpace.mk, isPreconnected_of_forall_constant, Iff.mp, continuousOn_univ
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
⊢ PreconnectedSpace α ↔ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
⟨fun _ _ => isClopen_iff.mp, fun h ↦ ?_⟩

Premises used: isClopen_iff, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
refine : ∀ (h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ), PreconnectedSpace α
⊢ PreconnectedSpace α ↔ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
refine ⟨fun _ _ => isClopen_iff.mp, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ PreconnectedSpace α

Tactic:
preconnectedSpace_of_forall_constant fun f hf x y ↦ ?_

Premises used: preconnectedSpace_of_forall_constant
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
refine : ∀ (f : α → Bool) (hf : Continuous[inst, _] f) (x y : α), f x = f y
⊢ PreconnectedSpace α

Tactic:
refine preconnectedSpace_of_forall_constant fun f hf x y ↦ ?_

Premises used: preconnectedSpace_of_forall_constant
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
rw : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
rw₁ : f ⁻¹' {false} = f ⁻¹' {!true}
rw₂ rw₃ : f ⁻¹' {false} = f ⁻¹' {false}
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ

Tactic:
rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]

Premises used: Bool.compl_singleton, Set.preimage_compl, Bool.not_true
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ

Tactic:
have : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ := by
    rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
inl : ∀ (h : f ⁻¹' {true} = ∅), f x = f y
inr : ∀ (h : f ⁻¹' {true} = univ), f x = f y
⊢ f x = f y

Tactic:
obtain (h | h) := h _ ((isClopen_discrete {true}).preimage hf)

Premises used: isClopen_discrete, Bool.true, Singleton.singleton, IsClopen.preimage
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h_1 : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = ∅
⊢ f x = f y

Tactic:
simp_all
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
h_1 : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = univ
⊢ f x = f y

Tactic:
simp_all
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
rw : IsConnected.{u} (α := α) univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₁ :
  Set.Nonempty.{u} (α := α) univ ∧ IsPreconnected.{u} (α := α) univ ↔
    Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₂ : Set.Nonempty.{u} (α := α) univ ∧ PreconnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₃ :
  (Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ) ↔
    Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₄ rw₅ :
  (Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ) ↔
    Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]

Premises used: IsConnected, Set.nonempty_iff_univ_nonempty, preconnectedSpace_iff_univ, connectedSpace_iff_univ, preconnectedSpace_iff_clopen
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : CompactSpace α
⊢ CompactSpace.{u} (ConnectedComponents α)

Tactic:
Quotient.compactSpace

Premises used: Quotient.compactSpace, ConnectedComponents
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
rw : ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
rw [hasBasis_self]

Premises used: Filter.hasBasis_self
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
rcases : ∀ (i : ι) (hpi : p x i) (hi : s x i ⊆ t), ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
rcases (h x).mem_iff.mp ht with ⟨i, hpi, hi⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

Premises used: And.intro, Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : IsOpen[inst] F
x : X
rw : ∀ x_1 ∈ pathComponentIn F x, pathComponentIn F x ∈ 𝓝 x_1
⊢ IsOpen[inst] (pathComponentIn F x)

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : IsOpen[inst] F
x y : X
hy : y ∈ pathComponentIn F x
let : ∀ (s : Set X) (hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F), pathComponentIn F x ∈ 𝓝 y
⊢ pathComponentIn F x ∈ 𝓝 y

Tactic:
let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : IsOpen[inst] F
x y : X
hy : y ∈ pathComponentIn F x
s : Set X
hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F
⊢ pathComponentIn F x ∈ 𝓝 y

Tactic:
mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸
    hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

Premises used: Eq.rec, mem_of_mem_nhds, And.right, IsPathConnected.subset_pathComponentIn, And.left, pathComponentIn_congr, Filter.mem_of_superset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : IsOpen[inst] F
x y : X
hy : y ∈ pathComponentIn F x
s : Set X
hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F
⊢ pathComponentIn F x ∈ 𝓝 y

Tactic:
exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸
    hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

Premises used: And.left, Filter.mem_of_superset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
rw : IsOpen[inst] (pathComponentIn univ x)
⊢ IsOpen[inst] (pathComponent x)

Tactic:
rw [← pathComponentIn_univ]

Premises used: pathComponentIn_univ
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ IsOpen[inst] (pathComponentIn univ x)

Tactic:
isOpen_univ.pathComponentIn _

Premises used: IsOpen.pathComponentIn, isOpen_univ
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ IsOpen[inst] (pathComponentIn univ x)

Tactic:
exact isOpen_univ.pathComponentIn _

Premises used: IsOpen.pathComponentIn, isOpen_univ
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
rw : ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1
⊢ IsClosed[inst] (pathComponent x)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds, isOpen_compl_iff
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
rcases : ∀ (V : Set X) (hVy : V ∈ 𝓝 y) (hVc : IsPathConnected V), (pathComponent x)ᶜ ∈ 𝓝 y
⊢ (pathComponent x)ᶜ ∈ 𝓝 y

Tactic:
rcases (path_connected_basis y).ex_mem with ⟨V, hVy, hVc⟩

Premises used: Filter.HasBasis.ex_mem, LocPathConnectedSpace.path_connected_basis
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
h : ∀ (z : X) (hz : z ∈ V) (hxz : z ∈ pathComponent x), False
⊢ (pathComponent x)ᶜ ∈ 𝓝 y

Tactic:
filter_upwards [hVy] with z hz hxz
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
hz : z ∈ V
hxz : z ∈ pathComponent x
⊢ False

Tactic:
hxy <| hxz.trans (hVc.joinedIn _ hz _ (mem_of_mem_nhds hVy)).joined

Premises used: Joined.trans, JoinedIn.joined, mem_of_mem_nhds, IsPathConnected.joinedIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
hz : z ∈ V
hxz : z ∈ pathComponent x
⊢ False

Tactic:
exact hxy <| hxz.trans (hVc.joinedIn _ hz _ (mem_of_mem_nhds hVy)).joined

Premises used: Joined.trans, JoinedIn.joined, mem_of_mem_nhds, IsPathConnected.joinedIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ IsClopen (pathComponent x)

Tactic:
⟨.pathComponent x, .pathComponent x⟩

Premises used: And.intro, IsClosed.pathComponent, IsClopen, IsOpen.pathComponent
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
let : ∀ (u : Set X) (huF : u ⊆ F) (hu : IsOpen[inst] u) (hxu : x ∈ u), pathComponentIn F x ∈ 𝓝 x
⊢ pathComponentIn F x ∈ 𝓝 x

Tactic:
let ⟨u, huF, hu, hxu⟩ := mem_nhds_iff.mp hF
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
u : Set X
huF : u ⊆ F
hu : IsOpen[inst] u
hxu : x ∈ u
⊢ pathComponentIn F x ∈ 𝓝 x

Tactic:
mem_nhds_iff.mpr ⟨pathComponentIn u x, pathComponentIn_mono huF,
    hu.pathComponentIn x, mem_pathComponentIn_self hxu⟩

Premises used: Iff.mpr, mem_nhds_iff, mem_pathComponentIn_self, IsOpen.pathComponentIn, pathComponentIn, And.intro, Exists.intro, pathComponentIn_mono
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
u : Set X
huF : u ⊆ F
hu : IsOpen[inst] u
hxu : x ∈ u
⊢ pathComponentIn F x ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.mpr ⟨pathComponentIn u x, pathComponentIn_mono huF,
    hu.pathComponentIn x, mem_pathComponentIn_self hxu⟩

Premises used: Iff.mpr, mem_nhds_iff, mem_pathComponentIn_self, IsOpen.pathComponentIn, pathComponentIn, And.intro, Exists.intro, pathComponentIn_mono
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
inst_2 : ConnectedSpace X
⊢ ∀ (x y : X), Joined x y

Tactic:
simp [← mem_pathComponent_iff, IsClopen.pathComponent _ |>.eq_univ]

Premises used: IsClopen.pathComponent, mem_pathComponent_iff, IsClopen.eq_univ
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
⊢ PathConnectedSpace X ↔ ConnectedSpace X

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ .of_locPathConnectedSpace⟩

Premises used: inferInstance, PathConnectedSpace.of_locPathConnectedSpace, Iff.intro
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ pathComponent x = connectedComponent x

Tactic:
(pathComponent_subset_component x).antisymm <|
    (IsClopen.pathComponent x).connectedComponent_subset (mem_pathComponent_self _)

Premises used: IsClopen.pathComponent, IsClopen.connectedComponent_subset, mem_pathComponent_self, HasSubset.Subset.antisymm, pathComponent_subset_component
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
rw : connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x
⊢ connectedComponent x = connectedComponent y ↔ Joined x y

Tactic:
rw [← mem_pathComponent_iff, pathComponent_eq_connectedComponent, eq_comm]

Premises used: mem_pathComponent_iff, eq_comm, pathComponent_eq_connectedComponent
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
⊢ connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x

Tactic:
connectedComponent_eq_iff_mem

Premises used: connectedComponent_eq_iff_mem
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
⊢ connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x

Tactic:
exact connectedComponent_eq_iff_mem

Premises used: connectedComponent_eq_iff_mem
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
⊢ connectedComponentSetoid X = pathSetoid X

Tactic:
Setoid.ext connectedComponent_eq_iff_joined

Premises used: connectedComponent_eq_iff_joined, Setoid.ext
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ Eq (α := ZerothHomotopy X)
    ((connectedComponentsEquivZerothHomotopy : (a : ConnectedComponents X) → ZerothHomotopy X) ⟦x⟧ : ZerothHomotopy X)
    (ZerothHomotopy.mk x : ZerothHomotopy X)

Tactic:
rfl

Premises used: Quotient.map, Quot.map, ZerothHomotopy.mk, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
⊢ Eq.{u_1 + 1} (α := (a : ZerothHomotopy X) → ConnectedComponents X)
    (⇑(Equiv.symm connectedComponentsEquivZerothHomotopy) : (a : ZerothHomotopy X) → ConnectedComponents X)
    ZerothHomotopy.toConnectedComponents

Tactic:
rfl

Premises used: Quotient.map, ZerothHomotopy.toConnectedComponents, Quot.map, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ (Equiv.symm connectedComponentsEquivZerothHomotopy : (a : ZerothHomotopy X) → ConnectedComponents X)
      (ZerothHomotopy.mk x) =
    ⟦x⟧

Tactic:
rfl

Premises used: Quotient.map, ZerothHomotopy.toConnectedComponents, Quot.map, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
inst_1 : LocPathConnectedSpace X
U : Set X
h : IsOpen[inst] U
hx : x ∈ U
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsPathConnected s ∧ s ⊆ U) id

Tactic:
(path_connected_basis x).hasBasis_self_subset (IsOpen.mem_nhds h hx)

Premises used: IsOpen.mem_nhds, LocPathConnectedSpace.path_connected_basis, Filter.HasBasis.hasBasis_self_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsPathConnected s) id

Tactic:
⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩

Premises used: Iff.mpr, mem_nhds_iff, Membership.mem, _private.0.isOpen_isPathConnected_basis.match_1, nhds, And.right, And.left, Filter.HasBasis.mk, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
refine : ∀ (s : Set X) (hs : s ∈ 𝓝 x), ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsPathConnected s) id

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
have :
  ∀ (u : Set X) (hus : u ⊆ s) (hu : IsOpen[inst] u) (hxu : x ∈ u),
    ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
have ⟨u, hus, hu, hxu⟩ := mem_nhds_iff.mp hs
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hus : u ⊆ s
hu : IsOpen[inst] u
hxu : x ∈ u
⊢ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
⟨pathComponentIn u x, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu,
    isPathConnected_pathComponentIn hxu⟩⟩, pathComponentIn_subset.trans hus⟩

Premises used: HasSubset.Subset.trans, mem_pathComponentIn_self, IsOpen.pathComponentIn, pathComponentIn, isPathConnected_pathComponentIn, And.intro, Exists.intro, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hus : u ⊆ s
hu : IsOpen[inst] u
hxu : x ∈ u
⊢ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
exact ⟨pathComponentIn u x, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu,
    isPathConnected_pathComponentIn hxu⟩⟩, pathComponentIn_subset.trans hus⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocPathConnectedSpace X
e : Y → X
he : IsOpenEmbedding e
this :
  ∀ (y : Y), (𝓝 y).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) fun (x : Set X) ↦ e ⁻¹' x
x : Y
s : Set X
h : s ∈ 𝓝 (e x) ∧ IsPathConnected s ∧ s ⊆ range e
left : s ∈ 𝓝 (e x)
hs : IsPathConnected s
hse : s ⊆ range e
rwa : IsPathConnected (e '' e ⁻¹' s)
rwa₁ rwa₂ rwa₃ rwa₄ : IsPathConnected s
⊢ IsPathConnected (e ⁻¹' s)

Tactic:
rwa [he.isPathConnected_iff, image_preimage_eq_of_subset hse]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Set.image_preimage_eq_of_subset, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.isPathConnected_iff
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
h : IsOpen[inst] U
⊢ LocPathConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
h.isOpenEmbedding_subtypeVal.locPathConnectedSpace

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.locPathConnectedSpace
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
U_op : IsOpen[inst] U
rw : ConnectedSpace.{u_1} (↑U : Type u_1) ↔ PathConnectedSpace.{u_1} (↑U : Type u_1)
⊢ IsConnected U ↔ IsPathConnected U

Tactic:
rw [isConnected_iff_connectedSpace, isPathConnected_iff_pathConnectedSpace]

Premises used: isPathConnected_iff_pathConnectedSpace, isConnected_iff_connectedSpace
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
U_op : IsOpen[inst] U
⊢ LocPathConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
haveI := U_op.locPathConnectedSpace