rcases this with (rfl | ⟨hne, hmem⟩) <;> simp[lookup]
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
this : a = a' ∨ a ≠ a' ∧ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
case cons.inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
hne : a ≠ a'
hmem : a ∈ as
⊢ (match a == a' with
    | true => some (f a')
    | false => lookup a (map (fun x => (x, f x)) as)) =
    some (f a)