F : Type ?u.354773
α : Type u_1
β : Type ?u.354779
γ : Type ?u.354782
ι : Type ?u.354785
κ : Type ?u.354788
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(↑toDual (min' s hs)) = ↑(max' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s)))
F : Type ?u.354773
α : Type u_1
β : Type ?u.354779
γ : Type ?u.354782
ι : Type ?u.354785
κ : Type ?u.354788
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑toDual (min' s hs) = max' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s))
rw [← WithBot.coe_eq_coe]
F : Type ?u.354773
α : Type u_1
β : Type ?u.354779
γ : Type ?u.354782
ι : Type ?u.354785
κ : Type ?u.354788
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ sup s (WithBot.some ∘ fun x => ↑toDual x) = sup s ((WithBot.some ∘ fun x => x) ∘ ↑toDual)
F : Type ?u.354773
α : Type u_1
β : Type ?u.354779
γ : Type ?u.354782
ι : Type ?u.354785
κ : Type ?u.354788
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(↑toDual (min' s hs)) = ↑(max' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s)))
simp only [min'_eq_inf', id_eq, toDual_inf', Function.comp_apply, coe_sup', max'_eq_sup',
  sup_image]
no goals
F : Type ?u.354773
α : Type u_1
β : Type ?u.354779
γ : Type ?u.354782
ι : Type ?u.354785
κ : Type ?u.354788
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ sup s (WithBot.some ∘ fun x => ↑toDual x) = sup s ((WithBot.some ∘ fun x => x) ∘ ↑toDual)
rfl