-- Mathlib/Order/Filter/Cofinite.lean
theorem Filter.Tendsto.exists_within_forall_le {α β : Type*} [LinearOrder β] {s : Set α}
    (hs : s.Nonempty) {f : α → β} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) :
    ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Proof state:
case inr.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
exact ⟨a₀, ha₀s, fun a ha => not_all_top a ha (f a₀)⟩

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
rcases em (∃ y ∈ s, ∃ x, f y < x) with (⟨y, hys, x, hx⟩ | not_all_top)

Result:
case inl.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

case inr
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ¬∃ y ∈ s, ∃ x, f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Proof state:
case inl.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ :=
  exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩

Result:
case inl.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Proof state:
case inl.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
refine ⟨a₀, ha₀s, fun a has => (lt_or_le (f a) x).elim ?_ (le_trans ha₀.le)⟩

Result:
case inl.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a

Proof state:
case inr
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ha₀s⟩ := hs

Result:
case inr.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Proof state:
case inr
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ¬∃ y ∈ s, ∃ x, f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
push_neg at not_all_top

Result:
case inr
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Proof state:
case inl.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
have : { y | ¬x ≤ f y }.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)

Result:
case inl.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | ¬x ≤ f y}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Proof state:
case inl.intro.intro.intro.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a

Tactic:
exact fun h => others_bigger a ⟨h, has⟩

Result:
no goals

Proof state:
case inl.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | ¬x ≤ f y}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
simp only [not_le] at this

Result:
case inl.intro.intro.intro
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a