case intro
F : Type ?u.403056
α : Type u_2
β : Type u_1
γ : Type ?u.403065
ι : Type ?u.403068
κ : Type ?u.403071
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
y : α
hy : Finset.max (image f s) = ↑y
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
F : Type ?u.403056
α : Type u_2
β : Type u_1
γ : Type ?u.403065
ι : Type ?u.403068
κ : Type ?u.403071
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
cases' max_of_nonempty (h.image f) with y hy
case intro.intro.intro
F : Type ?u.403056
α : Type u_2
β : Type u_1
γ : Type ?u.403065
ι : Type ?u.403068
κ : Type ?u.403071
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
x : β
hx : x ∈ s
hy : Finset.max (image f s) = ↑(f x)
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
case intro
F : Type ?u.403056
α : Type u_2
β : Type u_1
γ : Type ?u.403065
ι : Type ?u.403068
κ : Type ?u.403071
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
y : α
hy : Finset.max (image f s) = ↑y
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩
no goals
case intro.intro.intro
F : Type ?u.403056
α : Type u_2
β : Type u_1
γ : Type ?u.403065
ι : Type ?u.403068
κ : Type ?u.403071
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
x : β
hx : x ∈ s
hy : Finset.max (image f s) = ↑(f x)
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩