mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t

pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace 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:
·

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ ∀ i ∈ s, w i = 0

pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : ¬(i ∈ s ∧ w i ≠ 0)
⊢ ∀ i ∈ s, w i = 0

Tactic:
·

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ ∀ i ∈ s, w i = 0
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case inl
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
hs' : s ∩ Iio a = ∅
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

pp: case inr
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
hs' : s ∩ Iio a = ∅
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ pathComponentIn u (inl x)

pp: case inl.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)

pp: case inl.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x

Tactic:
·

Goal state after:
case inl.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ pathComponentIn u (inl x)
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl.refine_1.hs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsPathConnected (inl '' pathComponentIn (inl ⁻¹' u) x)

pp: case hxs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x

pp: case inl.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ u

Tactic:
·

Goal state after:
case inl.refine_1.hs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsPathConnected (inl '' pathComponentIn (inl ⁻¹' u) x)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
⊢ Convex R {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

pp: case refine_3
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
⊢ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x} ⊆ (convexHull R) (Set.range v)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
⊢ Convex R {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case hxs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x

pp: case inl.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ u

Tactic:
·

Goal state after:
case hxs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
⊢ Ioo b a ∈ 𝓝[s ∩ Iio a] a

pp: 𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
x : 𝕜
hx : x ∈ Ioo b a
⊢ s \ {a} ∈ 𝓝 x

Tactic:
·

Goal state after:
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
⊢ Ioo b a ∈ 𝓝[s ∩ Iio a] a
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ u

Tactic:
·

Goal state after:
case inl.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ u
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
x : 𝕜
hx : x ∈ Ioo b a
⊢ s \ {a} ∈ 𝓝 x

Tactic:
·

Goal state after:
𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
x : 𝕜
hx : x ∈ Ioo b a
⊢ s \ {a} ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)

pp: case inl.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x

Tactic:
·

Goal state after:
case inl.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x

Tactic:
·

Goal state after:
case inl.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace 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:
·

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace 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
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ pathComponentIn u (inr y)

pp: case inr.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

pp: case inr.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

Tactic:
·

Goal state after:
case inr.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ pathComponentIn u (inr y)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x

pp: case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : (𝓝[s \ {a}] a).NeBot
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_1.hs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsPathConnected (inr '' pathComponentIn (inr ⁻¹' u) y)

pp: case hxs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

pp: case inr.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ u

Tactic:
·

Goal state after:
case inr.refine_1.hs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsPathConnected (inr '' pathComponentIn (inr ⁻¹' u) y)
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case hxs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

pp: case inr.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ u

Tactic:
·

Goal state after:
case hxs
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ u

Tactic:
·

Goal state after:
case inr.refine_1.hsF
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ u
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

pp: case inr.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

Tactic:
·

Goal state after:
case inr.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

Tactic:
·

Goal state after:
case inr.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_1
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd ⊆ pathComponentIn u x

pp: case refine_2
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ IsOpen[instTopologicalSpaceSigma] (mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd)

pp: case refine_3
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ x ∈ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd

Tactic:
·

Goal state after:
case refine_1
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd ⊆ pathComponentIn u x