awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
refine : ∀ b ∈ f '' K, b ≤ f x
⊢ sSup (f '' K) < y

Tactic:
refine (csSup_le (h0K.image f) ?_).trans_lt (h x hx)

Premises used: Set.Nonempty.image, LE.le.trans_lt, csSup_le
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
x' : β
hx' : x' ∈ K
⊢ f x' ≤ f x

Tactic:
h2x hx'

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
x' : β
hx' : x' ∈ K
⊢ f x' ≤ f x

Tactic:
exact h2x hx'
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
⊢ y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x

Tactic:
IsCompact.sSup_lt_iff_of_continuous (α := αᵒᵈ) hK h0K hf y

Premises used: IsCompact.sSup_lt_iff_of_continuous, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ sInf s ∈ s

Tactic:
let ⟨_a, ha⟩ := hs.exists_isLeast ne_s
  ha.csInf_mem

Premises used: IsCompact.exists_isLeast, IsLeast.csInf_mem, Membership.mem, _private.0.IsCompact.sInf_mem.match_1, InfSet.sInf
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ sSup s ∈ s

Tactic:
IsCompact.sInf_mem (α := αᵒᵈ) hs ne_s

Premises used: Set.Mem, IsCompact.sInf_mem
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ IsGLB s (sInf s)

Tactic:
isGLB_csInf ne_s hs.bddBelow

Premises used: IsCompact.bddBelow, isGLB_csInf
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
IsCompact.isGLB_sInf (α := αᵒᵈ) hs ne_s

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsLeast, IsCompact.isGLB_sInf, IsLUB, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ IsLeast s (sInf s)

Tactic:
⟨hs.sInf_mem ne_s, (hs.isGLB_sInf ne_s).1⟩

Premises used: IsCompact.sInf_mem, IsLeast, IsCompact.isGLB_sInf, And.left, And.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ IsGreatest s (sSup s)

Tactic:
IsCompact.isLeast_sInf (α := αᵒᵈ) hs ne_s

Premises used: IsCompact.isLeast_sInf, Set.Mem, setOf, upperBounds, IsGreatest, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
⊢ ∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y

Tactic:
let ⟨x, hxs, hx⟩ := (hs.image_of_continuousOn hf).sInf_mem (ne_s.image f)
  ⟨x, hxs, hx.symm, fun _y hy =>
    hx.trans_le <| csInf_le (hs.image_of_continuousOn hf).bddBelow <| mem_image_of_mem f hy⟩

Premises used: IsCompact.bddBelow, IsCompact.sInf_mem, Membership.mem, Exists, Eq.trans_le, And, Set.mem_image_of_mem, Set.Nonempty.image, IsCompact.image_of_continuousOn, And.intro, Exists.intro, Set.image, _private.0.IsCompact.exists_sInf_image_eq_and_le.match_1, Eq.symm, csInf_le, Eq, InfSet.sInf
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
⊢ ∃ x ∈ s, sSup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x

Tactic:
IsCompact.exists_sInf_image_eq_and_le (α := αᵒᵈ) hs ne_s hf

Premises used: OrderDual, IsCompact.exists_sInf_image_eq_and_le
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
⊢ ∃ x ∈ s, sInf (f '' s) = f x

Tactic:
let ⟨x, hxs, hx, _⟩ := hs.exists_sInf_image_eq_and_le ne_s hf
  ⟨x, hxs, hx⟩

Premises used: Membership.mem, Exists, And, And.intro, Exists.intro, Set.image, Eq, InfSet.sInf, _private.0.IsCompact.exists_sInf_image_eq.match_1, IsCompact.exists_sInf_image_eq_and_le
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
⊢ ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x

Tactic:
IsCompact.exists_sInf_image_eq (α := αᵒᵈ) hs ne_s

Premises used: OrderDual, IsCompact.exists_sInf_image_eq
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
f : β → α
s t : Set β
z : β
ht : IsCompact t
hf : ContinuousOn f t
hz : z ∈ t
hfz : ∀ z' ∈ t \ s, f z < f z'
⊢ ∃ x ∈ s, IsMinOn f t x

Tactic:
let ⟨x, hxt, hfx⟩ := ht.exists_isMinOn ⟨z, hz⟩ hf
  ⟨x, by_contra fun hxs => (hfz x ⟨hxt, hxs⟩).not_ge (hfx hz), hfx⟩

Premises used: _private.0.IsCompact.exists_isMinOn_mem_subset.match_1, Membership.mem, Exists, IsMinOn, And, IsCompact.exists_isMinOn, And.intro, Exists.intro, by_contra, LT.lt.not_ge
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
s t : Set β
z : β
ht : IsCompact t
hf : ContinuousOn f t
hz : z ∈ t
hfz : ∀ z' ∈ t \ s, f z' < f z
⊢ ∃ x ∈ s, IsMaxOn f t x

Tactic:
let ⟨x, hxt, hfx⟩ := ht.exists_isMaxOn ⟨z, hz⟩ hf
  ⟨x, by_contra fun hxs => (hfz x ⟨hxt, hxs⟩).not_ge (hfx hz), hfx⟩

Premises used: IsMaxOn, Membership.mem, Exists, _private.0.IsCompact.exists_isMaxOn_mem_subset.match_1, And, And.intro, Exists.intro, by_contra, LT.lt.not_ge, IsCompact.exists_isMaxOn
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
f : β → α
s t : Set β
z : β
ht : IsCompact t
hst : s ⊆ t
hf : ContinuousOn f t
hz : z ∈ t
hfz : ∀ z' ∈ t \ s, f z < f z'
hs : IsOpen[inst_2] s
⊢ ∃ x ∈ s, IsLocalMin f x

Tactic:
let ⟨x, hxs, h⟩ := ht.exists_isMinOn_mem_subset hf hz hfz
  ⟨x, hxs, h.isLocalMin <| mem_nhds_iff.2 ⟨s, hst, hs, hxs⟩⟩

Premises used: Iff.mpr, mem_nhds_iff, IsCompact.exists_isMinOn_mem_subset, Membership.mem, Exists, _private.0.IsCompact.exists_isLocalMin_mem_open.match_1, IsMinOn.isLocalMin, IsLocalMin, And, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
s t : Set β
z : β
ht : IsCompact t
hst : s ⊆ t
hf : ContinuousOn f t
hz : z ∈ t
hfz : ∀ z' ∈ t \ s, f z' < f z
hs : IsOpen[inst_2] s
⊢ ∃ x ∈ s, IsLocalMax f x

Tactic:
let ⟨x, hxs, h⟩ := ht.exists_isMaxOn_mem_subset hf hz hfz
  ⟨x, hxs, h.isLocalMax <| mem_nhds_iff.2 ⟨s, hst, hs, hxs⟩⟩

Premises used: Iff.mpr, IsLocalMax, mem_nhds_iff, Membership.mem, Exists, IsMaxOn.isLocalMax, And, And.intro, Exists.intro, IsCompact.exists_isMaxOn_mem_subset, _private.0.IsCompact.exists_isLocalMax_mem_open.match_1
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
h₁ : IsConnected s
h₂ : IsCompact s
⊢ s = Icc (sInf s) (sSup s)

Tactic:
eq_Icc_csInf_csSup_of_connected_bdd_closed h₁ h₂.bddBelow h₂.bddAbove h₂.isClosed

Premises used: IsCompact.bddBelow, IsCompact.bddAbove, eq_Icc_csInf_csSup_of_connected_bdd_closed, IsCompact.isClosed
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
inl : ∀ (hK : IsCompact.{u_3} (X := β) ∅), Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' ∅)
inr : ∀ (h0K : K.Nonempty), Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)

Tactic:
rcases eq_empty_or_nonempty K with (rfl | h0K)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
hK : IsCompact.{u_3} (X := β) ∅
inl : Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup ∅
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' ∅)

Tactic:
simp_rw [image_empty]

Premises used: Set.image_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
hK : IsCompact.{u_3} (X := β) ∅
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup ∅

Tactic:
continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
hK : IsCompact.{u_3} (X := β) ∅
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup ∅

Tactic:
exact continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
inr : ∀ (x : γ), ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x
⊢ Continuous[inst_4, inst_1] fun (x : γ) ↦ sSup (f x '' K)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
inr :
  ∀ (y : β) (hyK : y ∈ K) (h2y : sSup (f x '' K) = f x y) (hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y),
    ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x
⊢ ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x

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

Premises used: Continuous.continuousOn, Continuous.comp, Continuous.prodMk_right, IsCompact.exists_sSup_image_eq_and_ge
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
inr : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
⊢ ContinuousAt.{u_4, u_2} (Y := α) (fun (x : γ) ↦ sSup (f x '' K)) x

Tactic:
rw [ContinuousAt, h2y, tendsto_order]

Premises used: ContinuousAt, tendsto_order
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'

Tactic:
have := tendsto_order.mp ((show Continuous fun x => f x y
    from hf.comp <| .prodMk_left _).tendsto x)
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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'

Tactic:
⟨fun z hz => ?_, fun z hz => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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'
inr : ∀ (z : α) (hz : z < f x y), ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)
inr₁ : ∀ (z : α) (hz : z > f x y), ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
⊢ (∀ 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:
refine ⟨fun z hz => ?_, fun z hz => ?_⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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
⊢ ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)

Tactic:
(this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK

Premises used: Filter.Eventually.mono, And.left, Set.mem_image_of_mem, LT.lt.trans_le, le_csSup
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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
inr : ∀ (x' : γ) (hx' : z < f x' y), BddAbove (f x' '' K)
⊢ ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)

Tactic:
refine (this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK

Premises used: Filter.Eventually.mono, And.left, Set.mem_image_of_mem, LT.lt.trans_le, le_csSup
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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
x' : γ
hx' : z < f x' y
⊢ BddAbove (f x' '' K)

Tactic:
hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn

Premises used: Continuous.continuousOn, Continuous.comp, Continuous.prodMk_right, IsCompact.bddAbove_image
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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
x' : γ
hx' : z < f x' y
⊢ BddAbove (f x' '' K)

Tactic:
exact hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn

Premises used: Continuous.continuousOn, Continuous.comp, Continuous.prodMk_right, IsCompact.bddAbove_image
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
y : β
hyK : y ∈ K
z : α
x' : γ
y' : β
hy' : (x', y').2 ∈ K
h2y : sSup (f x' '' 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'
hz : z > f x' y
⊢ (x', y') ∈ ↿f ⁻¹' Iio z

Tactic:
(hy y' hy').trans_lt hz

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
y : β
hyK : y ∈ K
z : α
x' : γ
y' : β
hy' : (x', y').2 ∈ K
h2y : sSup (f x' '' 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'
hz : z > f x' y
⊢ (x', y') ∈ ↿f ⁻¹' Iio z

Tactic:
exact (hy y' hy').trans_lt hz

Premises used: LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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
⊢ SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z

Tactic:
have h : ({x} : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z := by
      rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
      exact (hy y' hy').trans_lt hz
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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 : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
inr :
  ∀ (u : Set γ) (v : Set β) (hu : IsOpen[inst_4] u),
    IsOpen[inst_3] v →
      ∀ (hxu : {x} ⊆ u) (hKv : K ⊆ v) (huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z), ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < 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

Premises used: isOpen_Iio, isCompact_singleton, generalized_tube_lemma, IsOpen.preimage
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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 : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Tactic:
eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => ?_

Premises used: Set.singleton_subset_iff, Filter.eventually_of_mem, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst_1] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' 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 : SProd.sprod (α := Set γ) {x} K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst_4] u
left : IsOpen[inst_3] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
inr : ∀ (x' : γ) (hx' : x' ∈ u), sSup (f x' '' K) < z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Tactic:
refine eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => ?_

Premises used: Set.singleton_subset_iff, Filter.eventually_of_mem, IsOpen.mem_nhds, Iff.mp