F : Type ?u.352825
α : Type u_1
β : Type ?u.352831
γ : Type ?u.352834
ι : Type ?u.352837
κ : Type ?u.352840
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑(↑ofDual (max' s hs)) = ↑(min' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s)))
F : Type ?u.352825
α : Type u_1
β : Type ?u.352831
γ : Type ?u.352834
ι : Type ?u.352837
κ : Type ?u.352840
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑ofDual (max' s hs) = min' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s))
rw [← WithTop.coe_eq_coe]
F : Type ?u.352825
α : Type u_1
β : Type ?u.352831
γ : Type ?u.352834
ι : Type ?u.352837
κ : Type ?u.352840
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ inf s (WithTop.some ∘ fun x => ↑ofDual x) = inf s ((WithTop.some ∘ fun x => x) ∘ ↑ofDual)
F : Type ?u.352825
α : Type u_1
β : Type ?u.352831
γ : Type ?u.352834
ι : Type ?u.352837
κ : Type ?u.352840
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑(↑ofDual (max' s hs)) = ↑(min' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s)))
simp only [max'_eq_sup', id_eq, ofDual_sup', Function.comp_apply, coe_inf', min'_eq_inf',
  inf_image]
no goals
F : Type ?u.352825
α : Type u_1
β : Type ?u.352831
γ : Type ?u.352834
ι : Type ?u.352837
κ : Type ?u.352840
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ inf s (WithTop.some ∘ fun x => ↑ofDual x) = inf s ((WithTop.some ∘ fun x => x) ∘ ↑ofDual)
rfl