diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean
index b634ba83b6634b..8a2ddd93dba407 100644
--- a/Mathlib/Topology/Connected/LocallyConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyConnected.lean
@@ -151,6 +151,22 @@ theorem IsOpen.locallyConnectedSpace [LocallyConnectedSpace α] {U : Set α} (hU
     LocallyConnectedSpace U :=
   hU.isOpenEmbedding_subtypeVal.locallyConnectedSpace
 
+/-- The image of a locally connected space under a quotient map (in particular, under an open
+continuous surjection) is locally connected. -/
+theorem Topology.IsQuotientMap.locallyConnectedSpace [LocallyConnectedSpace α]
+    [TopologicalSpace β] {f : α → β} (hf : IsQuotientMap f) : LocallyConnectedSpace β := by
+  rw [locallyConnectedSpace_iff_connectedComponentIn_open]
+  intro F hF y _
+  rw [← hf.isOpen_preimage, isOpen_iff_mem_nhds]
+  intro x hx
+  have hxF : x ∈ f ⁻¹' F := connectedComponentIn_subset F y hx
+  refine Filter.mem_of_superset
+    ((hF.preimage hf.continuous).connectedComponentIn.mem_nhds (mem_connectedComponentIn hxF))
+    fun z hz ↦ ?_
+  rw [mem_preimage, connectedComponentIn_eq hx]
+  exact connectedComponentIn_mono _ (image_preimage_subset f F)
+    (hf.continuous.mapsTo_connectedComponentIn hxF hz)
+
 /-- If a space is locally connected, the topology of its connected components is discrete. -/
 instance [LocallyConnectedSpace α] : DiscreteTopology <| ConnectedComponents α := by
   refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
@@ -162,4 +178,83 @@ instance [LocallyConnectedSpace α] : DiscreteTopology <| ConnectedComponents α
 instance [LocallyConnectedSpace α] [CompactSpace α] : Finite <| ConnectedComponents α :=
   finite_of_compact_of_discrete
 
+/-- The product of two locally connected spaces is locally connected. -/
+instance Prod.locallyConnectedSpace [TopologicalSpace β] [LocallyConnectedSpace α]
+    [LocallyConnectedSpace β] : LocallyConnectedSpace (α × β) := by
+  rw [locallyConnectedSpace_iff_connected_subsets]
+  rintro ⟨x, y⟩ U hU
+  obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
+  exact ⟨connectedComponentIn u x ×ˢ connectedComponentIn v y,
+    prod_mem_nhds (connectedComponentIn_mem_nhds hu) (connectedComponentIn_mem_nhds hv),
+    isPreconnected_connectedComponentIn.prod isPreconnected_connectedComponentIn,
+    (prod_mono (connectedComponentIn_subset _ _) (connectedComponentIn_subset _ _)).trans huv⟩
+
+/-- If each `X i` is locally connected and all but finitely many are preconnected, then
+`∀ i, X i` is locally connected. -/
+theorem Pi.locallyConnectedSpace_of_finite_nonpreconnected [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] (hfinite : {i | ¬PreconnectedSpace (X i)}.Finite) :
+    LocallyConnectedSpace (∀ i, X i) := by
+  rw [locallyConnectedSpace_iff_connected_subsets]
+  intro x U hU
+  rw [nhds_pi, Filter.mem_pi] at hU
+  obtain ⟨J, hJ, t, ht, htU⟩ := hU
+  classical
+  set K := J ∪ {i | ¬PreconnectedSpace (X i)} with hK
+  refine ⟨K.pi fun i ↦ connectedComponentIn (t i) (x i),
+    set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
+    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i (mem_union_left _ hiJ))⟩
+  rw [← univ_pi_piecewise_univ]
+  refine isPreconnected_univ_pi fun i ↦ ?_
+  by_cases hi : i ∈ K
+  · rw [piecewise_eq_of_mem _ _ _ hi]
+    exact isPreconnected_connectedComponentIn
+  · rw [piecewise_eq_of_notMem _ _ _ hi]
+    have : PreconnectedSpace (X i) := not_not.mp fun h ↦ hi (hK ▸ mem_union_right _ h)
+    exact isPreconnected_univ
+
+/-- A finite product of locally connected spaces is locally connected. -/
+instance Pi.locallyConnectedSpace_of_finite [Finite ι] [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] : LocallyConnectedSpace (∀ i, X i) :=
+  locallyConnectedSpace_of_finite_nonpreconnected (Set.toFinite _)
+
+/-- A product of preconnected, locally connected spaces is locally connected. Note that an
+arbitrary product of locally connected spaces need not be locally connected, so the
+preconnectedness assumption cannot be dropped entirely (though it can be dropped for finitely
+many factors, see `Pi.locallyConnectedSpace_of_finite_nonpreconnected`). -/
+instance Pi.locallyConnectedSpace [∀ i, TopologicalSpace (X i)]
+    [∀ i, LocallyConnectedSpace (X i)] [∀ i, PreconnectedSpace (X i)] :
+    LocallyConnectedSpace (∀ i, X i) :=
+  locallyConnectedSpace_of_finite_nonpreconnected
+    (Set.finite_empty.subset fun _ hi ↦ (hi inferInstance).elim)
+
+/-- A product of spaces is locally connected iff it is empty, or every factor is locally
+connected and all but finitely many factors are preconnected. -/
+theorem Pi.locallyConnectedSpace_iff [∀ i, TopologicalSpace (X i)] :
+    LocallyConnectedSpace (∀ i, X i) ↔
+      IsEmpty (∀ i, X i) ∨
+        (∀ i, LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · rcases isEmpty_or_nonempty (∀ i, X i) with he | hne
+    · exact .inl he
+    obtain ⟨x⟩ := hne
+    classical
+    haveI : ∀ i, Nonempty (X i) := Classical.nonempty_pi.mp ⟨x⟩
+    refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
+      (Function.surjective_eval i)).locallyConnectedSpace, ?_⟩
+    have hVn : connectedComponent x ∈ 𝓝 x :=
+      isOpen_connectedComponent.mem_nhds mem_connectedComponent
+    rw [nhds_pi, Filter.mem_pi] at hVn
+    obtain ⟨J, hJ, t, ht, htV⟩ := hVn
+    refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_
+    suffices himg : Function.eval i '' connectedComponent x = univ by
+      exact ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩
+    refine (subset_univ _).antisymm fun z _ ↦
+      ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩
+    rw [Function.update_of_ne (ne_of_mem_of_not_mem hj hiJ)]
+    exact mem_of_mem_nhds (ht j)
+  · rintro (he | ⟨hloc, hfin⟩)
+    · exact ⟨fun x ↦ he.elim x⟩
+    · haveI := hloc
+      exact Pi.locallyConnectedSpace_of_finite_nonpreconnected hfin
+
 end LocallyConnectedSpace
diff --git a/Mathlib/Topology/Connected/LocallyPathConnected.lean b/Mathlib/Topology/Connected/LocallyPathConnected.lean
index b5ff93d8531de0..2091add763f588 100644
--- a/Mathlib/Topology/Connected/LocallyPathConnected.lean
+++ b/Mathlib/Topology/Connected/LocallyPathConnected.lean
@@ -29,6 +29,12 @@ path-connected, in that each point has a basis of path-connected neighborhoods.
   path-connected spaces are locally path-connected.
 * `Sum.locallyPathConnectedSpace` / `Sigma.locallyPathConnectedSpace`: disjoint unions of locally
   path-connected spaces are locally path-connected.
+* `Prod.locallyPathConnectedSpace` / `Pi.locallyPathConnectedSpace`: binary products of locally
+  path-connected spaces are locally path-connected; likewise for pi types when the index type is
+  finite or all factors are path-connected.
+* `Pi.locallyPathConnectedSpace_iff`: a product of spaces is locally path-connected iff it is
+  empty, or every factor is locally path-connected and all but finitely many factors are
+  path-connected.
 
 Abstractly, this also shows that locally path-connected spaces form a coreflective subcategory of
 the category of topological spaces, although we do not prove that in this form here.
@@ -299,6 +305,86 @@ instance Sigma.locallyPathConnectedSpace {X : ι → Type*}
 @[deprecated (since := "2026-06-21")]
 alias Sigma.locPathConnectedSpace := Sigma.locallyPathConnectedSpace
 
+/-- The product of two locally path-connected spaces is locally path-connected. -/
+instance Prod.locallyPathConnectedSpace [LocallyPathConnectedSpace Y] :
+    LocallyPathConnectedSpace (X × Y) where
+  path_connected_basis := fun (x, y) ↦ hasBasis_self.mpr fun U hU ↦ by
+    obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
+    exact ⟨pathComponentIn u x ×ˢ pathComponentIn v y,
+      prod_mem_nhds (pathComponentIn_mem_nhds hu) (pathComponentIn_mem_nhds hv),
+      (isPathConnected_pathComponentIn (mem_of_mem_nhds hu)).prod
+        (isPathConnected_pathComponentIn (mem_of_mem_nhds hv)),
+      (Set.prod_mono pathComponentIn_subset pathComponentIn_subset).trans huv⟩
+
+/-- If each `Z i` is locally path-connected and all but finitely many are path-connected, then
+`∀ i, Z i` is locally path-connected. -/
+theorem Pi.locallyPathConnectedSpace_of_finite_nonpathconnected {Z : ι → Type*}
+    [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)]
+    (hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite) :
+    LocallyPathConnectedSpace (∀ i, Z i) where
+  path_connected_basis x := hasBasis_self.mpr fun U hU ↦ by
+    rw [nhds_pi, Filter.mem_pi] at hU
+    obtain ⟨J, hJ, t, ht, htU⟩ := hU
+    classical
+    set K := J ∪ {i | ¬PathConnectedSpace (Z i)} with hK
+    refine ⟨K.pi fun i ↦ pathComponentIn (t i) (x i),
+      set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ pathComponentIn_mem_nhds (ht i), ?_,
+      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i (mem_union_left _ hiJ))⟩
+    rw [← univ_pi_piecewise_univ]
+    refine .pi fun i ↦ ?_
+    by_cases hi : i ∈ K
+    · rw [piecewise_eq_of_mem _ _ _ hi]
+      exact isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i))
+    · rw [piecewise_eq_of_notMem _ _ _ hi]
+      have : PathConnectedSpace (Z i) := not_not.mp fun h ↦ hi (hK ▸ mem_union_right _ h)
+      exact isPathConnected_univ
+
+/-- A finite product of locally path-connected spaces is locally path-connected. -/
+instance Pi.locallyPathConnectedSpace_of_finite [Finite ι] {Z : ι → Type*}
+    [∀ i, TopologicalSpace (Z i)] [∀ i, LocallyPathConnectedSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) :=
+  locallyPathConnectedSpace_of_finite_nonpathconnected (Set.toFinite _)
+
+/-- A product of path-connected, locally path-connected spaces is locally path-connected. Note
+that an arbitrary product of locally path-connected spaces need not be locally path-connected, so
+the path-connectedness assumption cannot be dropped entirely (though it can be dropped for
+finitely many factors, see `Pi.locallyPathConnectedSpace_of_finite_nonpathconnected`). -/
+instance Pi.locallyPathConnectedSpace {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)]
+    [∀ i, LocallyPathConnectedSpace (Z i)] [∀ i, PathConnectedSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) :=
+  locallyPathConnectedSpace_of_finite_nonpathconnected
+    (Set.finite_empty.subset fun _ hi ↦ (hi inferInstance).elim)
+
+/-- A product of spaces is locally path-connected iff it is empty, or every factor is locally
+path-connected and all but finitely many factors are path-connected. -/
+theorem Pi.locallyPathConnectedSpace_iff {Z : ι → Type*} [∀ i, TopologicalSpace (Z i)] :
+    LocallyPathConnectedSpace (∀ i, Z i) ↔
+      IsEmpty (∀ i, Z i) ∨
+        (∀ i, LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · rcases isEmpty_or_nonempty (∀ i, Z i) with he | hne
+    · exact .inl he
+    obtain ⟨x⟩ := hne
+    classical
+    haveI : ∀ i, Nonempty (Z i) := Classical.nonempty_pi.mp ⟨x⟩
+    refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
+      (surjective_eval i)).locallyPathConnectedSpace, ?_⟩
+    have hVn : pathComponent x ∈ 𝓝 x :=
+      (IsOpen.pathComponent x).mem_nhds (mem_pathComponent_self x)
+    rw [nhds_pi, Filter.mem_pi] at hVn
+    obtain ⟨J, hJ, t, ht, htV⟩ := hVn
+    refine hJ.subset fun i hi ↦ by_contra fun hiJ ↦ hi ?_
+    suffices himg : eval i '' pathComponent x = univ by
+      rw [pathConnectedSpace_iff_univ, ← himg]
+      exact isPathConnected_pathComponent.image (continuous_apply i)
+    refine (subset_univ _).antisymm fun z _ ↦ ⟨update x i z, htV fun j hj ↦ ?_, by simp⟩
+    rw [update_of_ne (ne_of_mem_of_not_mem hj hiJ)]
+    exact mem_of_mem_nhds (ht j)
+  · rintro (he | ⟨hloc, hfin⟩)
+    · exact ⟨fun x ↦ he.elim x⟩
+    · haveI := hloc
+      exact Pi.locallyPathConnectedSpace_of_finite_nonpathconnected hfin
+
 instance AlexandrovDiscrete.locallyPathConnectedSpace [AlexandrovDiscrete X] :
     LocallyPathConnectedSpace X := by
   apply LocallyPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton