no goals
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
this : Primrec₂ fun a n => List.map (f a) (List.range n)
a : α
n : ℕ
⊢ List.get? (List.map (f (a, n).fst) (List.range (Nat.succ (a, n).snd))) (a, n).snd = some (f a n)
simp [List.get?_range (Nat.lt_succ_self n)]
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) n =
    some (List.map (f a) (List.range n))
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some [])
      (fun n IH =>
        Option.bind (a, n, IH).snd.snd fun b =>
          Option.map (fun b_1 => (((a, n, IH), b), b_1).fst.snd ++ [(((a, n, IH), b), b_1).snd])
            (g ((a, n, IH), b).fst.fst ((a, n, IH), b).snd))
      n =
    some (List.map (f a) (List.range n))
simp
case zero
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) Nat.zero =
    some (List.map (f a) (List.range Nat.zero))

case succ
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
IH :
  Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) n =
    some (List.map (f a) (List.range n))
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) (Nat.succ n) =
    some (List.map (f a) (List.range (Nat.succ n)))
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) n =
    some (List.map (f a) (List.range n))
induction' n with n IH
no goals
case succ
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
IH :
  Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) n =
    some (List.map (f a) (List.range n))
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) (Nat.succ n) =
    some (List.map (f a) (List.range (Nat.succ n)))
simp [IH, H, List.range_succ]
no goals
case zero
α : Type u_2
β : Type ?u.320238
γ : Type ?u.320241
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) Nat.zero =
    some (List.map (f a) (List.range Nat.zero))
rfl