refine ⟨fun h ↦ ?_, ?_⟩
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ 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
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

case refine_2
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
⊢ (∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)) → ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a