case intro
F : Type ?u.314269
α : Type u_1
β : Type ?u.314275
γ : Type ?u.314278
ι : Type ?u.314281
κ : Type ?u.314284
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
a : α
ha : Finset.max s = ↑a
⊢ s = ∅
F : Type ?u.314269
α : Type u_1
β : Type ?u.314275
γ : Type ?u.314278
ι : Type ?u.314281
κ : Type ?u.314284
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
⊢ s = ∅
obtain ⟨a, ha⟩ := max_of_nonempty H
case intro
F : Type ?u.314269
α : Type u_1
β : Type ?u.314275
γ : Type ?u.314278
ι : Type ?u.314281
κ : Type ?u.314284
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
a : α
ha : ⊥ = ↑a
⊢ s = ∅
case intro
F : Type ?u.314269
α : Type u_1
β : Type ?u.314275
γ : Type ?u.314278
ι : Type ?u.314281
κ : Type ?u.314284
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
a : α
ha : Finset.max s = ↑a
⊢ s = ∅
rw [h] at ha
no goals
case intro
F : Type ?u.314269
α : Type u_1
β : Type ?u.314275
γ : Type ?u.314278
ι : Type ?u.314281
κ : Type ?u.314284
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
a : α
ha : ⊥ = ↑a
⊢ s = ∅
cases ha