Theorem: lowerSemicontinuousOn_iff_preimage_Iic (Sion/Semicontinuous.lean)

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ v, IsClosed v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
Tactic:
simp only [lowerSemicontinuousOn_iff_restrict, restrict_eq,
  lowerSemicontinuous_iff_isClosed_preimage, preimage_comp, isClosed_induced_iff,
  Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
State after:
no goals