-- Mathlib/Topology/Order/Compact.lean
theorem IsCompact.continuous_sSup {f : γ → β → α} {K : Set β} (hK : IsCompact K)
    (hf : Continuous ↿f) : Continuous fun x => sSup (f x '' K)

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'

Tactic:
have := tendsto_order.mp ((show Continuous fun x => f x y
  from hf.comp <| continuous_id.prod_mk continuous_const).tendsto x)

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'

Proof state:
case inr.intro.intro.intro.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Tactic:
obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ :=
  generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h

Result:
case inr.intro.intro.intro.refine_2.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen u
left✝ : IsOpen v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Proof state:
case inr.intro.intro.intro.refine_2.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen u
left✝ : IsOpen v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ x ∈ K, f x' x < z

Tactic:
exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))

Result:
no goals

Proof state:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
⊢ ∀ (x : γ), ContinuousAt (fun x => sSup (f x '' K)) x

Tactic:
intro x

Result:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
⊢ ContinuousAt (fun x => sSup (f x '' K)) x

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ ContinuousAt (fun x => sSup (f x '' K)) x

Tactic:
rw [ContinuousAt, h2y, tendsto_order]

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'

Proof state:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
⊢ ContinuousAt (fun x => sSup (f x '' K)) x

Tactic:
obtain ⟨y, hyK, h2y, hy⟩ :=
  hK.exists_sSup_image_eq_and_ge h0K
    (show Continuous fun y => f x y from hf.comp <| Continuous.Prod.mk x).continuousOn

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ ContinuousAt (fun x => sSup (f x '' K)) x