rw [preimage_comp, ← inducing_subtype_val.isPreconnected_image, image_preimage_eq_inter_range,
  Subtype.range_coe, inter_comm]
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconvexOn ℝ s f
⊢ IsPreconnected ((f ∘ fun x => ↑x) ⁻¹' Iic t)
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconvexOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Iic t)