F : Type ?u.364381
α : Type u_2
β : Type u_1
γ : Type ?u.364390
ι : Type ?u.364393
κ : Type ?u.364396
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
y : β
hy : y ∈ image f s
⊢ y ≤ f (max' s (_ : Finset.Nonempty s))
F : Type ?u.364381
α : Type u_2
β : Type u_1
γ : Type ?u.364390
ι : Type ?u.364393
κ : Type ?u.364396
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
⊢ max' (image f s) h = f (max' s (_ : Finset.Nonempty s))
refine'
  le_antisymm (max'_le _ _ _ fun y hy => _) (le_max' _ _ (mem_image.mpr ⟨_, max'_mem _ _, rfl⟩))
case intro.intro
F : Type ?u.364381
α : Type u_2
β : Type u_1
γ : Type ?u.364390
ι : Type ?u.364393
κ : Type ?u.364396
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
x : α
hx : x ∈ s
hy : f x ∈ image f s
⊢ f x ≤ f (max' s (_ : Finset.Nonempty s))
F : Type ?u.364381
α : Type u_2
β : Type u_1
γ : Type ?u.364390
ι : Type ?u.364393
κ : Type ?u.364396
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
y : β
hy : y ∈ image f s
⊢ y ≤ f (max' s (_ : Finset.Nonempty s))
obtain ⟨x, hx, rfl⟩ := mem_image.mp hy
no goals
case intro.intro
F : Type ?u.364381
α : Type u_2
β : Type u_1
γ : Type ?u.364390
ι : Type ?u.364393
κ : Type ?u.364396
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
x : α
hx : x ∈ s
hy : f x ∈ image f s
⊢ f x ≤ f (max' s (_ : Finset.Nonempty s))
exact hf (le_max' _ _ hx)