Theorem: Primrec.list_take (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₂ List.take
Tactic:
have : Primrec₂ (fun s a => s.rec [] (fun n as => as ++ (a.get? n).toList) : ℕ → List α → List α) :=
  to₂ (nat_rec' fst (const [])
    (list_append.comp₂ (snd.comp₂ Primrec₂.right)
      (option_toList.comp₂ $ list_get?.comp₂ (snd.comp₂ Primrec₂.left) (fst.comp₂ Primrec₂.right))))
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 s a => Nat.rec [] (fun n as => as ++ (a.get? n).toList) s
⊢ Primrec₂ List.take

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 s a => Nat.rec [] (fun n as => as ++ (a.get? n).toList) s
⊢ Primrec₂ List.take
Tactic:
exact this.of_eq (fun n as => by induction' n with n ih <;> simp[List.take_succ, *])
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 s a => Nat.rec [] (fun n as => as ++ (a.get? n).toList) s
n : ℕ
as : List α
⊢ Nat.rec [] (fun n as_1 => as_1 ++ (as.get? n).toList) n = List.take n as
Tactic:
induction' n with n ih <;> simp[List.take_succ, *]
State after:
no goals