case h.e'_2.h
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ Finset.min (erase s x) = Finset.max (erase (map (Equiv.toEmbedding toDual) s) (↑toDual x))
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ Finset.min (erase s x) ≠ ↑x
convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding) using 1
case h.e'_2.h.h
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ erase s x = erase (map (Equiv.toEmbedding toDual) s) (↑toDual x)
case h.e'_2.h
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ Finset.min (erase s x) = Finset.max (erase (map (Equiv.toEmbedding toDual) s) (↑toDual x))
apply congr_arg
case h.e'_2.h.h.h.e'_3.h
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ s = map (Equiv.toEmbedding toDual) s
case h.e'_2.h.h
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ erase s x = erase (map (Equiv.toEmbedding toDual) s) (↑toDual x)
congr!
case h.e'_2.h.h.h.e'_3.h.a
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ map (Equiv.toEmbedding toDual) s
case h.e'_2.h.h.h.e'_3.h
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ s = map (Equiv.toEmbedding toDual) s
ext
case h.e'_2.h.h.h.e'_3.h.a
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ ↑toDual.symm a✝ ∈ s
case h.e'_2.h.h.h.e'_3.h.a
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ map (Equiv.toEmbedding toDual) s
simp only [mem_map_equiv]
no goals
case h.e'_2.h.h.h.e'_3.h.a
F : Type ?u.373369
α : Type u_1
β : Type ?u.373375
γ : Type ?u.373378
ι : Type ?u.373381
κ : Type ?u.373384
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ ↑toDual.symm a✝ ∈ s
exact Iff.rfl