simp only [lowerSemicontinuousOn_iff_restrict, restrict_eq,
  lowerSemicontinuous_iff_isOpen_preimage, preimage_comp, isOpen_induced_iff,
  Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ u, IsOpen u ∧ s ∩ f ⁻¹' Ioi b = s ∩ u
no goals