Theorem: Primrec.option_toList (Logic/Vorspiel/OmegaRec.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ Primrec Option.toList
Tactic:
have : Primrec (fun a => [a] : α → List α) := list_cons.comp Primrec.id (const [])
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
⊢ Primrec Option.toList

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
⊢ Primrec Option.toList
Tactic:
exact (option_casesOn Primrec.id (const []) (this.comp₂ Primrec₂.right)).of_eq
  (fun o => by rcases o <;> simp)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
o : Option α
⊢ (Option.casesOn (id o) [] fun b => [b]) = o.toList
Tactic:
rcases o <;> simp
State after:
no goals