let m := max' _ hu
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
case refine_1
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)