F : Type ?u.348581
α : Type u_1
β : Type ?u.348587
γ : Type ?u.348590
ι : Type ?u.348593
κ : Type ?u.348596
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithTop.map (↑toDual) (Finset.min s) = sup s (WithBot.some ∘ ↑toDual)
F : Type ?u.348581
α : Type u_1
β : Type ?u.348587
γ : Type ?u.348590
ι : Type ?u.348593
κ : Type ?u.348596
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithTop.map (↑toDual) (Finset.min s) = Finset.max (image (↑toDual) s)
rw [max_eq_sup_withBot, sup_image]
no goals
F : Type ?u.348581
α : Type u_1
β : Type ?u.348587
γ : Type ?u.348590
ι : Type ?u.348593
κ : Type ?u.348596
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithTop.map (↑toDual) (Finset.min s) = sup s (WithBot.some ∘ ↑toDual)
exact congr_fun Option.map_id _