awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)

Tactic:
isOpenMap_inl _ <| (hu.preimage continuous_inl).pathComponentIn _

Premises used: continuous_inl, IsOpen.pathComponentIn, isOpenMap_inl, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)

Tactic:
exact isOpenMap_inl _ <| (hu.preimage continuous_inl).pathComponentIn _

Premises used: continuous_inl, IsOpen.pathComponentIn, isOpenMap_inl, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inr y), IsOpen[instTopologicalSpaceSum] t ∧ inr y ∈ t

Tactic:
⟨Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y, ?_, ?_, ?_⟩

Premises used: pathComponentIn, Set.preimage, Sum.inr, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : Sum.inr y ∈ u
inr : Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ pathComponentIn u (Sum.inr y)
inr₁ : IsOpen[instTopologicalSpaceSum] (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y)
inr₂ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y) (Sum.inr y)
⊢ ∃ t ⊆ pathComponentIn u (Sum.inr y), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inr y ∈ t

Tactic:
refine ⟨Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : Sum.inr y ∈ u
inr : IsPathConnected (X := X ⊕ Y) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y)
inr₁ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y) (Sum.inr y)
inr₂ : Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ u
⊢ Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ pathComponentIn u (Sum.inr y)

Tactic:
apply IsPathConnected.subset_pathComponentIn

Premises used: IsPathConnected.subset_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ y ∈ inr ⁻¹' u

Tactic:
hxu

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ y ∈ inr ⁻¹' u

Tactic:
exact hxu
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsPathConnected (X := X ⊕ Y) (inr '' pathComponentIn (inr ⁻¹' u) y)

Tactic:
exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inr

Premises used: continuous_inr, IsPathConnected.image, isPathConnected_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ Membership.mem (γ := Set (X ⊕ Y)) (inr '' pathComponentIn (inr ⁻¹' u) y) (inr y)

Tactic:
⟨y, mem_pathComponentIn_self hxu, rfl⟩

Premises used: Set.Mem, setOf, mem_pathComponentIn_self, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ Membership.mem (γ := Set (X ⊕ Y)) (inr '' pathComponentIn (inr ⁻¹' u) y) (inr y)

Tactic:
exact ⟨y, mem_pathComponentIn_self hxu, rfl⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ u

Tactic:
(image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Set.image_preimage_subset, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ u

Tactic:
exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Set.image_preimage_subset, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

Tactic:
isOpenMap_inr _ <| (hu.preimage continuous_inr).pathComponentIn _

Premises used: continuous_inr, IsOpen.pathComponentIn, IsOpen.preimage, isOpenMap_inr
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

Tactic:
exact isOpenMap_inr _ <| (hu.preimage continuous_inr).pathComponentIn _

Premises used: continuous_inr, IsOpen.pathComponentIn, IsOpen.preimage, isOpenMap_inr
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
rw :
  ∀ (x : (i : ι) × X i) (u : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
⊢ LocPathConnectedSpace ((i : ι) × X i)

Tactic:
rw [locPathConnectedSpace_iff_pathComponentIn_mem_nhds]

Premises used: locPathConnectedSpace_iff_pathComponentIn_mem_nhds
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
rw : ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t
⊢ pathComponentIn u x ∈ 𝓝 x

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t

Tactic:
⟨(Sigma.mk x.1) '' pathComponentIn ((Sigma.mk x.1) ⁻¹' u) x.2, ?_, ?_, ?_⟩

Premises used: Sigma.fst, pathComponentIn, Set.preimage, And.intro, Exists.intro, Set.image, Sigma.mk, Sigma.snd
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
refine_1 :
  mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x
refine_2 :
  IsOpen[instTopologicalSpaceSigma]
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
refine_3 :
  x ∈
    mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t

Tactic:
refine ⟨(Sigma.mk x.1) '' pathComponentIn ((Sigma.mk x.1) ⁻¹' u) x.2, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
refine_1 :
  IsPathConnected
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
refine_1₁ :
  x ∈
    mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))
refine_1₂ :
  mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    u
⊢ mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x

Tactic:
apply IsPathConnected.subset_pathComponentIn

Premises used: IsPathConnected.subset_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x.snd (β := fun (i : ι) ↦ X i) ∈ mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u

Tactic:
hxu

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x.snd (β := fun (i : ι) ↦ X i) ∈ mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u

Tactic:
exact hxu
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ IsPathConnected
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))

Tactic:
exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_sigmaMk

Premises used: continuous_sigmaMk, IsPathConnected.image, isPathConnected_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x ∈
    mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))

Tactic:
⟨x.2, mem_pathComponentIn_self hxu, rfl⟩

Premises used: Set.Mem, setOf, mem_pathComponentIn_self, And.intro, Exists.intro, Set.image, Sigma.snd, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x ∈
    mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))

Tactic:
exact ⟨x.2, mem_pathComponentIn_self hxu, rfl⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    u

Tactic:
(image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Set.image_preimage_subset, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    u

Tactic:
exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Set.image_preimage_subset, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ IsOpen[instTopologicalSpaceSigma]
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))

Tactic:
isOpenMap_sigmaMk _ <| (hu.preimage continuous_sigmaMk).pathComponentIn _

Premises used: continuous_sigmaMk, IsOpen.pathComponentIn, isOpenMap_sigmaMk, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ IsOpen[instTopologicalSpaceSigma]
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))

Tactic:
exact isOpenMap_sigmaMk _ <| (hu.preimage continuous_sigmaMk).pathComponentIn _

Premises used: continuous_sigmaMk, IsOpen.pathComponentIn, isOpenMap_sigmaMk, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
apply : ∀ (x : X) (i : Unit), True → IsPathConnected (X := X) (nhdsKer {x})
⊢ LocPathConnectedSpace X

Tactic:
apply LocPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton

Premises used: nhds_basis_nhdsKer_singleton, LocPathConnectedSpace.of_bases
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
simp : ∀ (x : X), ∃ (x_1 : X), x_1 ⤳ x ∧ ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x_1 y
⊢ ∀ (x : X) (i : Unit), True → IsPathConnected (X := X) (nhdsKer {x})

Tactic:
simp only [forall_const, IsPathConnected, mem_nhdsKer_singleton]

Premises used: IsPathConnected, forall_const, mem_nhdsKer_singleton
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x : X
exists : ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x y
⊢ ∃ (x_2 : X), x_2 ⤳ x ∧ ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x_2 y

Tactic:
exists x, specializes_rfl

Premises used: specializes_rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
symm : JoinedIn (nhdsKer {x}) y x
⊢ JoinedIn (nhdsKer {x}) x y

Tactic:
symm
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₁ : Membership.mem (γ := Set X) (nhdsKer {x}) x
⊢ JoinedIn (nhdsKer {x}) y x

Tactic:
apply hy.joinedIn

Premises used: Specializes.joinedIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy hx : y ⤳ x
⊢ Membership.mem (γ := Set X) (nhdsKer {x}) y

Tactic:
rewrite [mem_nhdsKer_singleton]

Premises used: mem_nhdsKer_singleton
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
hy₁ : x ⤳ x
⊢ Membership.mem (γ := Set X) (nhdsKer {x}) x

Tactic:
rewrite [mem_nhdsKer_singleton]

Premises used: mem_nhdsKer_singleton
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ y ⤳ x

Tactic:
assumption
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ x ⤳ x

Tactic:
rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₁ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₁ : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₂ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₂ : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₃ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₃ : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₄ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₄ : y ⤳ x
hy₅ : x ⤳ x
hx₅ : y ⤳ x
hy₆ : x ⤳ x
⊢ JoinedIn (nhdsKer {x}) y x

Tactic:
apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]

Premises used: Specializes.joinedIn, mem_nhdsKer_singleton
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
⊢ DiscreteTopology.{u_1} (ZerothHomotopy X)

Tactic:
discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 : LocPathConnectedSpace X
refine : ∀ (c : ZerothHomotopy X), IsOpen (X := ZerothHomotopy X) {c}
⊢ DiscreteTopology.{u_1} (ZerothHomotopy X)

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton