case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
⊢ BddAbove (Set.range f)
obtain ⟨M, hM⟩ := Fintype.exists_le f
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)
refine' ⟨M, fun a ha => _⟩
case intro.intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M
obtain ⟨b, rfl⟩ := ha
no goals
case intro.intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M
exact hM b