-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem Convex.locPathConnectedSpace [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
    {S : Set E} (hS : Convex ℝ S) : LocPathConnectedSpace S

Proof state:
case refine_1
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ Subtype.val ⁻¹' t' ∈ 𝓝 x

Tactic:
exact continuousAt_subtype_val.preimage_mem_nhds ht'.1.1

Result:
no goals

Proof state:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
⊢ LocPathConnectedSpace ↑S

Tactic:
refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩

Result:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let ⟨t, ht⟩ := (mem_nhds_subtype S x s).mp hs

Result:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
case refine_2
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (S ∩ t')

Tactic:
exact (hS.inter ht'.1.2).isPathConnected ⟨x, x.2, mem_of_mem_nhds ht'.1.1⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let ⟨t', ht'⟩ := (LocallyConvexSpace.convex_basis (𝕜 := ℝ) x.1).mem_iff.mp ht.1

Result:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
case refine_2
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (Subtype.val ⁻¹' t')

Tactic:
refine Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left

Result:
case refine_2
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (S ∩ t')

Proof state:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩

Result:
case refine_1
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ Subtype.val ⁻¹' t' ∈ 𝓝 x

case refine_2
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (Subtype.val ⁻¹' t')