awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
⟨x, hxs, forall_mem_image.1 (fun _ hb => hx <| mem_image_of_mem f ?_)⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro, Iff.mp, Set.forall_mem_image
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
refine : ∀ (x : β) (hb : Membership.mem (γ := Set β) ((fun (a : β) ↦ a) '' s) x), x ∈ s
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
refine ⟨x, hxs, forall_mem_image.1 (fun _ hb => hx <| mem_image_of_mem f ?_)⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
x_1 : β
hb rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set β) ((fun (x : β) ↦ x) '' s) x_1
⊢ x_1 ∈ s

Tactic:
rwa [(image_id' s).symm]

Premises used: Set.image_id', Eq.symm
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
inl :
  ∀ (hs : IsCompact.{u_3} (X := β) ∅) (hf : ContinuousOn f ∅)
    (hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b),
    ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b
inr : ∀ (hs' : s.Nonempty), ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs')

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
a : α
hs : IsCompact.{u_3} (X := β) ∅
hf : ContinuousOn f ∅
hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b
inl : ∀ (a' : α) (ha' : a < a'), ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b
⊢ ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b

Tactic:
obtain ⟨a', ha'⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
a : α
hs : IsCompact.{u_3} (X := β) ∅
hf : ContinuousOn f ∅
hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b
a' : α
ha' : a < a'
⊢ ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b

Tactic:
⟨a', ha', fun _ a ↦ a.elim⟩

Premises used: False.elim, 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 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
a : α
hs : IsCompact.{u_3} (X := β) ∅
hf : ContinuousOn f ∅
hf' : ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a < f b
a' : α
ha' : a < a'
⊢ ∃ (a' : α), a < a' ∧ ∀ (b : β), Membership.mem (γ := Set β) ∅ b → a' ≤ f b

Tactic:
exact ⟨a', ha', fun _ a ↦ a.elim⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
inr : ∀ (x : β) (hx : x ∈ s) (hx' : IsMinOn f s x), ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf

Premises used: IsCompact.exists_isMinOn
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
x : β
hx : x ∈ s
hx' : IsMinOn f s x
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
⟨f x, hf' x hx, hx'⟩

Premises used: 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 : ClosedIicTopology α
inst_4 : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
x : β
hx : x ∈ s
hx' : IsMinOn f s x
⊢ ∃ (a' : α), a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
exact ⟨f x, hf' x hx, hx'⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
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, IsMaxOn f s x

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

Premises used: IsMaxOn, IsCompact.exists_isMinOn, IsMaxFilter
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
rcases : ∀ (K : Set β) (hK : IsCompact K) (hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x), ∃ x ∈ s, IsMinOn f s x
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩

Premises used: Iff.mp, Filter.HasBasis.eventually_iff, Filter.hasBasis_cocompact, Filter.HasBasis.inf_principal
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
⊢ insert x₀ (K ∩ s) ⊆ s

Tactic:
have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
⊢ ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y

Tactic:
((hK.inter_right hsc).insert x₀).exists_isMinOn (insert_nonempty _ _) (hf.mono hsub)

Premises used: Set.insert_nonempty, Set.Mem, Filter.Eventually, setOf, IsMinFilter, IsMinOn, Set.Subset, IsCompact.exists_isMinOn, IsCompact.insert, ContinuousOn.mono, IsCompact.inter_right
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
obtain : ∀ (x : β) (hx : x ∈ insert x₀ (K ∩ s)) (hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y), ∃ x ∈ s, IsMinOn f s x
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y :=
    ((hK.inter_right hsc).insert x₀).exists_isMinOn (insert_nonempty _ _) (hf.mono hsub)

Premises used: Set.insert_nonempty, Insert.insert, Inter.inter, IsCompact.exists_isMinOn, IsCompact.insert, ContinuousOn.mono, IsCompact.inter_right
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
⟨x, hsub hx, fun y hy => ?_⟩

Premises used: 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 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
refine : ∀ (y : β) (hy : y ∈ s), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
refine ⟨x, hsub hx, fun y hy => ?_⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
pos : ∀ (hyK : y ∈ K), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
neg : ∀ (hyK : y ∉ K), Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y
⊢ Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y

Tactic:
by_cases hyK : y ∈ K
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
hyK : y ∈ K
⊢ Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y

Tactic:
hxf _ (Or.inr ⟨hyK, hy⟩)

Premises used: Set.Mem, setOf, And.intro, Or.inr
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
hyK : y ∉ K
⊢ Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y

Tactic:
(hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)

Premises used: Set.Mem, setOf, And.intro, Or.inl, LE.le.trans, rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
hyK : y ∈ K
⊢ Membership.mem (γ := Set β) {x_1 : β | (fun (x_2 : β) ↦ f x ≤ f x_2) x_1} y

Tactic:
exacts [hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)]

Premises used: And.intro, Or.inl, LE.le.trans, Or.inr, rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst_2] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x ≤ f x₀
⊢ ∃ x ∈ s, IsMaxOn f s x

Tactic:
ContinuousOn.exists_isMinOn' (α := αᵒᵈ) hf hsc h₀ hc

Premises used: IsMaxOn, ContinuousOn.exists_isMinOn', IsMaxFilter
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
f : β → α
hf : Continuous[inst_2, inst_1] f
x₀ : β
h : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
rwa : ∀ᶠ (x : β) in cocompact β ⊓ ⊤, f x₀ ≤ f x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
⊢ ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 univ, f x₀ ≤ f x

Tactic:
rwa [principal_univ, inf_top_eq]

Premises used: inf_top_eq, Filter.principal_univ
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
f : β → α
hf : Continuous[inst_2, inst_1] f
x₀ : β
h : ∀ᶠ (x : β) in cocompact β, f x ≤ f x₀
⊢ ∃ (x : β), ∀ (y : β), f y ≤ f x

Tactic:
Continuous.exists_forall_le' (α := αᵒᵈ) hf x₀ h

Premises used: Continuous.exists_forall_le'
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
f : β → α
hf : Continuous[inst_2, inst_1] f
hlim : Tendsto f (cocompact β) atTop
inhabit : ∀ (inhabited_h : Inhabited β), ∃ (x : β), ∀ (y : β), f x ≤ f y
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
inhabit β
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
f : β → α
hf : Continuous[inst_2, inst_1] f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)

Premises used: Inhabited.default, Continuous.exists_forall_le', Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
f : β → α
hf : Continuous[inst_2, inst_1] f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)

Premises used: Inhabited.default, Continuous.exists_forall_le', Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
inst_4 : Nonempty β
f : β → α
hf : Continuous[inst_2, inst_1] f
hlim : Tendsto f (cocompact β) atBot
⊢ ∃ (x : β), ∀ (y : β), f y ≤ f x

Tactic:
Continuous.exists_forall_le (α := αᵒᵈ) hf hlim

Premises used: Continuous.exists_forall_le
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
obtain : ∀ (x : β) (hx : f x ∈ lowerBounds (range f)), ∃ (x : β), ∀ (y : β), f x ≤ f y
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)

Premises used: IsCompact.exists_isLeast, HasCompactMulSupport.isCompact_range, Set.range_nonempty, rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∀ (i : β), f x ≤ f i

Tactic:
rw [mem_lowerBounds, forall_mem_range] at hx

Premises used: Set.forall_mem_range, mem_lowerBounds
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
x : β
hx : ∀ (i : β), f x ≤ f i
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
⟨x, hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
x : β
hx : ∀ (i : β), f x ≤ f i
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
exact ⟨x, hx⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
inst_4 : Nonempty β
inst_5 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
⊢ ∃ (x : β), ∀ (y : β), f y ≤ f x

Tactic:
Continuous.exists_forall_le_of_hasCompactMulSupport (α := αᵒᵈ) hf h

Premises used: Continuous.exists_forall_le_of_hasCompactMulSupport
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
inl : ∀ (hs : IsCompact.{u_2} (X := α) ∅), BddBelow.{u_2} (α := α) ∅
inr : ∀ (hne : s.Nonempty), BddBelow s
⊢ BddBelow s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
hs : IsCompact.{u_2} (X := α) ∅
⊢ BddBelow.{u_2} (α := α) ∅

Tactic:
bddBelow_empty

Premises used: bddBelow_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
hs : IsCompact.{u_2} (X := α) ∅
⊢ BddBelow.{u_2} (α := α) ∅

Tactic:
exact bddBelow_empty

Premises used: bddBelow_empty
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
inr : ∀ (a : α) (has : a ∈ lowerBounds s), BddBelow s
⊢ BddBelow s

Tactic:
obtain ⟨a, -, has⟩ := hs.exists_isLeast hne

Premises used: IsCompact.exists_isLeast
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
a : α
has : a ∈ lowerBounds s
⊢ BddBelow s

Tactic:
⟨a, has⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
a : α
has : a ∈ lowerBounds s
⊢ BddBelow s

Tactic:
exact ⟨a, has⟩
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
inst_3 : Nonempty α
s : Set α
hs : IsCompact s
⊢ BddAbove s

Tactic:
IsCompact.bddBelow (α := αᵒᵈ) hs

Premises used: IsCompact.bddBelow, Set.Mem, setOf, upperBounds, BddAbove, OrderDual
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : Nonempty α
f : β → α
K : Set β
hK : IsCompact K
hf : ContinuousOn f K
⊢ BddBelow (f '' K)

Tactic:
(hK.image_of_continuousOn hf).bddBelow

Premises used: IsCompact.bddBelow, IsCompact.image_of_continuousOn
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
inst_4 : Nonempty α
f : β → α
K : Set β
hK : IsCompact K
hf : ContinuousOn f K
⊢ BddAbove (f '' K)

Tactic:
IsCompact.bddBelow_image (α := αᵒᵈ) hK hf

Premises used: Set.Mem, setOf, upperBounds, BddAbove, OrderDual, IsCompact.bddBelow_image
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIicTopology α
inst_4 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
⊢ BddBelow (range f)

Tactic:
(h.isCompact_range hf).bddBelow

Premises used: IsCompact.bddBelow, HasCompactMulSupport.isCompact_range
-- Module: Mathlib.Topology.Order.Compact
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : TopologicalSpace β
inst_3 : ClosedIciTopology α
inst_4 : One α
f : β → α
hf : Continuous[inst_2, inst_1] f
h : HasCompactMulSupport f
⊢ BddAbove (range f)

Tactic:
Continuous.bddBelow_range_of_hasCompactMulSupport (α := αᵒᵈ) hf h

Premises used: Set.Mem, setOf, upperBounds, BddAbove, OrderDual, Continuous.bddBelow_range_of_hasCompactMulSupport
-- 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 : α
⊢ sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y

Tactic:
⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h,
    fun h => ?_⟩

Premises used: IsCompact.bddAbove_image, Set.mem_image_of_mem, Iff.intro, le_csSup, LE.le.trans_lt
-- 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 : α
refine : ∀ (h : ∀ x ∈ K, f x < y), sSup (f '' K) < y
⊢ sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y

Tactic:
refine ⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h,
    fun h => ?_⟩
-- 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
obtain : ∀ (x : β) (hx : x ∈ K) (h2x : IsMaxOn f K x), sSup (f '' K) < y
⊢ sSup (f '' K) < y

Tactic:
obtain ⟨x, hx, h2x⟩ := hK.exists_isMaxOn h0K hf

Premises used: IsCompact.exists_isMaxOn
-- 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
⊢ sSup (f '' K) < y

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

Premises used: Set.Nonempty.image, LE.le.trans_lt, csSup_le