rcases (decode e) <;> simp[this]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
⊢ Option.map (fun w => (↑w).depth) (decode e) =
    Option.map (elim' ℕ (fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1) s) (decode e)
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
this : ∀ (w : SubWType β s), (↑w).depth = elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s w
val✝ : SubWType β s
⊢ elim' ℕ (fun p => Finset.univ.sup p.snd + 1) s val✝ =
    elim' ℕ (fun x => (List.ofFn (fintypeArrowEquivFinArrow x.snd)).sup + 1) s val✝