split <;> split <;> simp
case swap
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ y✝ : α
l✝ : List α
⊢ (match f y✝ with
    | true => some y✝
    | false =>
      match f x✝ with
      | true => some x✝
      | false => find? f l✝) =
    match f x✝ with
    | true => some x✝
    | false =>
      match f y✝ with
      | true => some y✝
      | false => find? f l✝
case swap.h_1.h_1
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ y✝ = x✝²