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

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