F : Type ?u.349735
α : Type u_1
β : Type ?u.349741
γ : Type ?u.349744
ι : Type ?u.349747
κ : Type ?u.349750
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithBot.map (↑toDual) (Finset.max s) = inf s (WithTop.some ∘ ↑toDual)
F : Type ?u.349735
α : Type u_1
β : Type ?u.349741
γ : Type ?u.349744
ι : Type ?u.349747
κ : Type ?u.349750
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithBot.map (↑toDual) (Finset.max s) = Finset.min (image (↑toDual) s)
rw [min_eq_inf_withTop, inf_image]
no goals
F : Type ?u.349735
α : Type u_1
β : Type ?u.349741
γ : Type ?u.349744
ι : Type ?u.349747
κ : Type ?u.349750
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithBot.map (↑toDual) (Finset.max s) = inf s (WithTop.some ∘ ↑toDual)
exact congr_fun Option.map_id _