Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.succ.succ.succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p ↦
    p.1.2[p.2.2]?.bind fun s ↦
      p.1.2[(unpair p.2.2).1]?.bind fun s₁ ↦
        Option.map
          (fun s₂ ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          p.1.2[(unpair p.2.2).2]?
this✝ : Primrec G₁
G : α → List σ → Option σ :=
  fun a IH ↦
    Nat.casesOn IH.length (some (z a)) fun n ↦
      Nat.casesOn n (some (s a)) fun n ↦
        Nat.casesOn n (some (l a)) fun n ↦ Nat.casesOn n (some (r a)) fun n ↦ G₁ ((a, IH), n, n.div2.div2)
this : Primrec₂ G
a : α
n : ℕ
⊢ Nat.rec (some (z a))
      (fun n_1 n_ih ↦
        Nat.rec (some (s a))
          (fun n_2 n_ih ↦
            Nat.rec (some (l a))
              (fun n_3 n_ih ↦
                Nat.rec (some (r a))
                  (fun n_4 n_ih ↦
                    G₁
                      ((a, List.map (fun n ↦ F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))), n_4, n_4.div2.div2))
                  n_3)
              n_2)
          n_1)
      (List.map (fun n ↦ F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))).length =
    some (F a (ofNat Code (n + 1 + 1 + 1 + 1)))

Tactic:
rw [List.length_map, List.length_range]

Goal state after:
case succ.succ.succ.succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p ↦
    p.1.2[p.2.2]?.bind fun s ↦
      p.1.2[(unpair p.2.2).1]?.bind fun s₁ ↦
        Option.map
          (fun s₂ ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          p.1.2[(unpair p.2.2).2]?
this✝ : Primrec G₁
G : α → List σ → Option σ :=
  fun a IH ↦
    Nat.casesOn IH.length (some (z a)) fun n ↦
      Nat.casesOn n (some (s a)) fun n ↦
        Nat.casesOn n (some (l a)) fun n ↦ Nat.casesOn n (some (r a)) fun n ↦ G₁ ((a, IH), n, n.div2.div2)
this : Primrec₂ G
a : α
n : ℕ
⊢ Nat.rec (some (z a))
      (fun n_1 n_ih ↦
        Nat.rec (some (s a))
          (fun n_2 n_ih ↦
            Nat.rec (some (l a))
              (fun n_3 n_ih ↦
                Nat.rec (some (r a))
                  (fun n_4 n_ih ↦
                    G₁
                      ((a, List.map (fun n ↦ F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))), n_4, n_4.div2.div2))
                  n_3)
              n_2)
          n_1)
      (n + 1 + 1 + 1 + 1) =
    some (F a (ofNat Code (n + 1 + 1 + 1 + 1)))