case pos
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : Finset.Nonempty (erase s x)
⊢ Finset.max (erase s x) ≠ ↑x

case neg
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : ¬Finset.Nonempty (erase s x)
⊢ Finset.max (erase s x) ≠ ↑x
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ Finset.max (erase s x) ≠ ↑x
by_cases s0 : (s.erase x).Nonempty
case pos
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : Finset.Nonempty (erase s x)
⊢ ↑(max' (erase s x) s0) ≠ ↑x
case pos
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : Finset.Nonempty (erase s x)
⊢ Finset.max (erase s x) ≠ ↑x
refine' ne_of_eq_of_ne (coe_max' s0).symm _
no goals
case pos
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : Finset.Nonempty (erase s x)
⊢ ↑(max' (erase s x) s0) ≠ ↑x
exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
case neg
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : ¬Finset.Nonempty (erase s x)
⊢ ⊥ ≠ ↑x
case neg
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : ¬Finset.Nonempty (erase s x)
⊢ Finset.max (erase s x) ≠ ↑x
rw [not_nonempty_iff_eq_empty.mp s0, max_empty]
no goals
case neg
F : Type ?u.372851
α : Type u_1
β : Type ?u.372857
γ : Type ?u.372860
ι : Type ?u.372863
κ : Type ?u.372866
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : ¬Finset.Nonempty (erase s x)
⊢ ⊥ ≠ ↑x
exact WithBot.bot_ne_coe