-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p : ℕ
refine :
  ∀ n ∈ List.range (unpair p).1,
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) Option.none
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          rec (motive := fun (x : Code) ↦ Option ℕ) (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ←
                lup
                    (List.map
                      (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range p))
                    ((unpair p).1, cf) n
              let y ←
                lup
                    (List.map
                      (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range p))
                    ((unpair p).1, cg) n
              some (Nat.pair x y))
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ←
                lup
                    (List.map
                      (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range p))
                    ((unpair p).1, cg) n
              lup
                  (List.map
                    (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range p))
                  ((unpair p).1, cf) x)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ)
                (lup
                  (List.map
                    (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range p))
                  ((unpair p).1, cf) (unpair n).1)
                (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦ do
                  let i ←
                    lup
                        (List.map
                          (fun (n : ℕ) ↦
                            List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                          (List.range p))
                        (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 n_2)
                  lup
                      (List.map
                        (fun (n : ℕ) ↦
                          List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range p))
                      ((unpair p).1, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
                (unpair n).2)
            (fun (cf : Code) (x : Option ℕ) ↦ do
              let x ←
                lup
                    (List.map
                      (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range p))
                    ((unpair p).1, cf) n
              Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
                  (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
                    lup
                      (List.map
                        (fun (n : ℕ) ↦
                          List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range p))
                      (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                  x)
            (ofNat Code (unpair p).2))
        (unpair p).1 =
      evaln (unpair p).1 (ofNat Code (unpair p).2) n
⊢ List.map
      (fun (n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) Option.none
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            rec (motive := fun (x : Code) ↦ Option ℕ) (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ←
                  lup
                      (List.map
                        (fun (n : ℕ) ↦
                          List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range p))
                      ((unpair p).1, cf) n
                let y ←
                  lup
                      (List.map
                        (fun (n : ℕ) ↦
                          List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range p))
                      ((unpair p).1, cg) n
                some (Nat.pair x y))
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ←
                  lup
                      (List.map
                        (fun (n : ℕ) ↦
                          List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range p))
                      ((unpair p).1, cg) n
                lup
                    (List.map
                      (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range p))
                    ((unpair p).1, cf) x)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ)
                  (lup
                    (List.map
                      (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                      (List.range p))
                    ((unpair p).1, cf) (unpair n).1)
                  (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦ do
                    let i ←
                      lup
                          (List.map
                            (fun (n : ℕ) ↦
                              List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                            (List.range p))
                          (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 n_2)
                    lup
                        (List.map
                          (fun (n : ℕ) ↦
                            List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                          (List.range p))
                        ((unpair p).1, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
                  (unpair n).2)
              (fun (cf : Code) (x : Option ℕ) ↦ do
                let x ←
                  lup
                      (List.map
                        (fun (n : ℕ) ↦
                          List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                        (List.range p))
                      ((unpair p).1, cf) n
                Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
                    (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
                      lup
                        (List.map
                          (fun (n : ℕ) ↦
                            List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                          (List.range p))
                        (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
                    x)
              (ofNat Code (unpair p).2))
          (unpair p).1)
      (List.range (unpair p).1) =
    List.map (evaln (unpair p).1 (ofNat Code (unpair p).2)) (List.range (unpair p).1)

Tactic:
refine List.map_congr_left fun n => ?_

Premises used: List.map_congr_left