F : Type ?u.350869
α : Type u_1
β : Type ?u.350875
γ : Type ?u.350878
ι : Type ?u.350881
κ : Type ?u.350884
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑(↑ofDual (min' s hs)) = ↑(max' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s)))
F : Type ?u.350869
α : Type u_1
β : Type ?u.350875
γ : Type ?u.350878
ι : Type ?u.350881
κ : Type ?u.350884
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑ofDual (min' s hs) = max' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s))
rw [← WithBot.coe_eq_coe]
F : Type ?u.350869
α : Type u_1
β : Type ?u.350875
γ : Type ?u.350878
ι : Type ?u.350881
κ : Type ?u.350884
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ sup s (WithBot.some ∘ fun x => ↑ofDual x) = sup s ((WithBot.some ∘ fun x => x) ∘ ↑ofDual)
F : Type ?u.350869
α : Type u_1
β : Type ?u.350875
γ : Type ?u.350878
ι : Type ?u.350881
κ : Type ?u.350884
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑(↑ofDual (min' s hs)) = ↑(max' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s)))
simp only [min'_eq_inf', id_eq, ofDual_inf', Function.comp_apply, coe_sup', max'_eq_sup',
  sup_image]
no goals
F : Type ?u.350869
α : Type u_1
β : Type ?u.350875
γ : Type ?u.350878
ι : Type ?u.350881
κ : Type ?u.350884
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ sup s (WithBot.some ∘ fun x => ↑ofDual x) = sup s ((WithBot.some ∘ fun x => x) ∘ ↑ofDual)
rfl