refine' forall₂_congr fun a ha => forall₂_congr fun b _ => _
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x) ↔
    ∀ (x : α) (h : x ∈ s), LowerSemicontinuousAt (restrict s f) { val := x, property := h }
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : b < f a
⊢ (∀ᶠ (x' : α) in 𝓝[s] a, b < f x') ↔ ∀ᶠ (x' : ↑s) in 𝓝 { val := a, property := ha }, b < restrict s f x'