-- Mathlib/Topology/Order/ExtrClosure.lean
theorem IsLocalMaxOn.closure (h : IsLocalMaxOn f s a) (hc : ContinuousOn f (closure s)) :
    IsLocalMaxOn f (closure s) a

Proof state:
case intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ ContinuousWithinAt f (U ∩ s) x

Tactic:
exact (hc _ hxs).mono (inter_subset_right.trans subset_closure)

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
⊢ IsLocalMaxOn f (closure s) a

Tactic:
refine mem_nhdsWithin.2 ⟨U, Uo, aU, ?_⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
⊢ U ∩ closure s ⊆ {x | (fun x => f x ≤ f a) x}

Proof state:
case intro.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ x ∈ closure (U ∩ s)

Tactic:
rwa [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_inter_of_mem, ←
  mem_closure_iff_nhdsWithin_neBot]

Result:
case intro.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ U ∈ 𝓝[s] x

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
⊢ IsLocalMaxOn f (closure s) a

Tactic:
rcases mem_nhdsWithin.1 h with ⟨U, Uo, aU, hU⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
⊢ IsLocalMaxOn f (closure s) a

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ x ∈ {x | (fun x => f x ≤ f a) x}

Tactic:
refine ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU

Result:
case intro.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ x ∈ closure (U ∩ s)

case intro.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ ContinuousWithinAt f (U ∩ s) x

Proof state:
case intro.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ U ∈ 𝓝[s] x

Tactic:
exact nhdsWithin_le_nhds (Uo.mem_nhds hxU)

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
⊢ U ∩ closure s ⊆ {x | (fun x => f x ≤ f a) x}

Tactic:
rintro x ⟨hxU, hxs⟩

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ x ∈ {x | (fun x => f x ≤ f a) x}