-- Mathlib/Topology/Connected/LocPathConnected.lean
/-- Any topology coinduced by a locally path-connected topology is locally path-connected. -/
lemma LocPathConnectedSpace.coinduced {Y : Type*} (f : X → Y) :
    @LocPathConnectedSpace Y (.coinduced f ‹_›)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
hx' : x ∈ f ⁻¹' u
⊢ f ⁻¹' pathComponentIn y u ∈ 𝓝 x

Tactic:
refine mem_nhds_iff.mpr ⟨pathComponentIn x (f ⁻¹' u), ?_,
  (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
hx' : x ∈ f ⁻¹' u
⊢ pathComponentIn x (f ⁻¹' u) ⊆ f ⁻¹' pathComponentIn y u

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
⊢ LocPathConnectedSpace Y

Tactic:
have hf : Continuous f := continuous_coinduced_rng

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
⊢ LocPathConnectedSpace Y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
hx' : x ∈ f ⁻¹' u
⊢ f '' pathComponentIn x (f ⁻¹' u) ⊆ pathComponentIn (f x) u

Tactic:
exact ((isPathConnected_pathComponentIn hx').image hf).subset_pathComponentIn
  ⟨x, mem_pathComponentIn_self hx', rfl⟩ <|
  (image_mono pathComponentIn_subset).trans <| u.image_preimage_subset f

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
⊢ LocPathConnectedSpace Y

Tactic:
refine locPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
  isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
⊢ f ⁻¹' pathComponentIn y u ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
hx' : x ∈ f ⁻¹' u
⊢ pathComponentIn x (f ⁻¹' u) ⊆ f ⁻¹' pathComponentIn y u

Tactic:
rw [← image_subset_iff, ← pathComponentIn_congr hx]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
hx' : x ∈ f ⁻¹' u
⊢ f '' pathComponentIn x (f ⁻¹' u) ⊆ pathComponentIn (f x) u

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
⊢ f ⁻¹' pathComponentIn y u ∈ 𝓝 x

Tactic:
have hx' := preimage_mono pathComponentIn_subset hx

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous f
y : Y
u : Set Y
hu : IsOpen u
x : X
hx : x ∈ f ⁻¹' pathComponentIn y u
hx' : x ∈ f ⁻¹' u
⊢ f ⁻¹' pathComponentIn y u ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
⊢ LocPathConnectedSpace Y

Tactic:
let _ := TopologicalSpace.coinduced f ‹_›

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
⊢ LocPathConnectedSpace Y