-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode c) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode c))))
          (k', c') n =
        evaln k' c' n
succ :
  ∀
    (hg :
      ∀ {k' : ℕ} {c' : Code} {n : ℕ},
        Nat.pair k' (encode c') < Nat.pair k (encode zero) →
          lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair k (encode zero))))
              (k', c') n =
            evaln k' c' n),
    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 (Nat.pair (k' + 1) (encode zero))))
                (k' + 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 (Nat.pair (k' + 1) (encode zero))))
                (k' + 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 (Nat.pair (k' + 1) (encode zero))))
                (k' + 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 (Nat.pair (k' + 1) (encode zero))))
              (k' + 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 (Nat.pair (k' + 1) (encode zero))))
              (k' + 1, cf) (unpair n).1)
            (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode zero))))
                    (k', zero) (Nat.pair (unpair n).1 n_1)
              lup
                  (List.map
                    (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair (k' + 1) (encode zero))))
                  (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 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 (Nat.pair (k' + 1) (encode zero))))
                (k' + 1, cf) n
          Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
              (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode zero))))
                  (k', zero) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
              x)
        zero =
      evaln (k' + 1) zero n
succ₁ :
  ∀
    (hg :
      ∀ {k' : ℕ} {c' : Code} {n : ℕ},
        Nat.pair k' (encode c') < Nat.pair k (encode Code.succ) →
          lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair k (encode Code.succ))))
              (k', c') n =
            evaln k' c' n),
    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 (Nat.pair (k' + 1) (encode Code.succ))))
                (k' + 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 (Nat.pair (k' + 1) (encode Code.succ))))
                (k' + 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 (Nat.pair (k' + 1) (encode Code.succ))))
                (k' + 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 (Nat.pair (k' + 1) (encode Code.succ))))
              (k' + 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 (Nat.pair (k' + 1) (encode Code.succ))))
              (k' + 1, cf) (unpair n).1)
            (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode Code.succ))))
                    (k', Code.succ) (Nat.pair (unpair n).1 n_1)
              lup
                  (List.map
                    (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair (k' + 1) (encode Code.succ))))
                  (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 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 (Nat.pair (k' + 1) (encode Code.succ))))
                (k' + 1, cf) n
          Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
              (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode Code.succ))))
                  (k', Code.succ) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
              x)
        Code.succ =
      evaln (k' + 1) Code.succ n
succ₂ :
  ∀
    (hg :
      ∀ {k' : ℕ} {c' : Code} {n : ℕ},
        Nat.pair k' (encode c') < Nat.pair k (encode left) →
          lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair k (encode left))))
              (k', c') n =
            evaln k' c' n),
    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 (Nat.pair (k' + 1) (encode left))))
                (k' + 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 (Nat.pair (k' + 1) (encode left))))
                (k' + 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 (Nat.pair (k' + 1) (encode left))))
                (k' + 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 (Nat.pair (k' + 1) (encode left))))
              (k' + 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 (Nat.pair (k' + 1) (encode left))))
              (k' + 1, cf) (unpair n).1)
            (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode left))))
                    (k', left) (Nat.pair (unpair n).1 n_1)
              lup
                  (List.map
                    (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                    (List.range (Nat.pair (k' + 1) (encode left))))
                  (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 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 (Nat.pair (k' + 1) (encode left))))
                (k' + 1, cf) n
          Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
              (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode left))))
                  (k', left) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
              x)
        left =
      evaln (k' + 1) left n
⊢ 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 (Nat.pair (k' + 1) (encode c))))
              (k' + 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 (Nat.pair (k' + 1) (encode c))))
              (k' + 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 (Nat.pair (k' + 1) (encode c))))
              (k' + 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 (Nat.pair (k' + 1) (encode c))))
            (k' + 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 (Nat.pair (k' + 1) (encode c))))
            (k' + 1, cf) (unpair n).1)
          (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode c))))
                  (k', c) (Nat.pair (unpair n).1 n_1)
            lup
                (List.map
                  (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair (k' + 1) (encode c))))
                (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 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 (Nat.pair (k' + 1) (encode c))))
              (k' + 1, cf) n
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
            (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode c))))
                (k', c) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
            x)
      c =
    evaln (k' + 1) c n
have succ₃ : ∀
  (hg :
    ∀ {k' : ℕ} {c' : Code} {n : ℕ},
      Nat.pair k' (encode c') < Nat.pair k (encode right) →
        lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair k (encode right))))
            (k', c') n =
          evaln k' c' n),
  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 (Nat.pair (k' + 1) (encode right))))
              (k' + 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 (Nat.pair (k' + 1) (encode right))))
              (k' + 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 (Nat.pair (k' + 1) (encode right))))
              (k' + 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 (Nat.pair (k' + 1) (encode right))))
            (k' + 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 (Nat.pair (k' + 1) (encode right))))
            (k' + 1, cf) (unpair n).1)
          (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode right))))
                  (k', right) (Nat.pair (unpair n).1 n_1)
            lup
                (List.map
                  (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair (k' + 1) (encode right))))
                (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 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 (Nat.pair (k' + 1) (encode right))))
              (k' + 1, cf) n
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
            (fun (n_1 : ℕ) (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 (Nat.pair (k' + 1) (encode right))))
                (k', right) (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
            x)
      right =
    evaln (k' + 1) right n
Tactic: obtain - | - | - | - | ⟨cf, cg⟩ | ⟨cf, cg⟩ | ⟨cf, cg⟩ | cf := c
Cleared hypotheses: c, hg