F : Type ?u.366451
α : Type u_2
β : Type u_1
γ : Type ?u.366460
ι : Type ?u.366463
κ : Type ?u.366466
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
⊢ f (min' s (_ : Finset.Nonempty s)) ≤ y
F : Type ?u.366451
α : Type u_2
β : Type u_1
γ : Type ?u.366460
ι : Type ?u.366463
κ : Type ?u.366466
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
⊢ min' (image f s) h = f (min' s (_ : Finset.Nonempty s))
refine'
  le_antisymm (min'_le _ _ (mem_image.mpr ⟨_, min'_mem _ _, rfl⟩)) (le_min' _ _ _ fun y hy => _)
case intro.intro
F : Type ?u.366451
α : Type u_2
β : Type u_1
γ : Type ?u.366460
ι : Type ?u.366463
κ : Type ?u.366466
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 (min' s (_ : Finset.Nonempty s)) ≤ f x
F : Type ?u.366451
α : Type u_2
β : Type u_1
γ : Type ?u.366460
ι : Type ?u.366463
κ : Type ?u.366466
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
⊢ f (min' s (_ : Finset.Nonempty s)) ≤ y
obtain ⟨x, hx, rfl⟩ := mem_image.mp hy
no goals
case intro.intro
F : Type ?u.366451
α : Type u_2
β : Type u_1
γ : Type ?u.366460
ι : Type ?u.366463
κ : Type ?u.366466
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 (min' s (_ : Finset.Nonempty s)) ≤ f x
exact hf (min'_le _ _ hx)