case inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : Set.Finite ∅
⊢ ∃ a, ∀ (b : α), b ∈ ∅ → f a ≤ f b

case inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
hs : Set.Nonempty s
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
rcases s.eq_empty_or_nonempty with rfl | hs
no goals
case inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : Set.Finite ∅
⊢ ∃ a, ∀ (b : α), b ∈ ∅ → f a ≤ f b
exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩
case inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
hs : Set.Nonempty s
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ (b : α), b ∈ s → f x₀ ≤ f b
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
case inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
hs : Set.Nonempty s
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
no goals
case inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
hs : Set.Nonempty s
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ (b : α), b ∈ s → f x₀ ≤ f b
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
exact ⟨x₀, fun x hx => hx₀ x hx⟩