Theorem: QuasiconvexOn.isPreconnected_preimage (Sion/Concavexity.lean)

State before:
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)
Tactic:
rw [preimage_comp, ← inducing_subtype_val.isPreconnected_image, image_preimage_eq_inter_range,
  Subtype.range_coe, inter_comm]
State after:
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)

State before:
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)
Tactic:
exact (hfc t).isPreconnected
State after:
no goals