-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : 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 : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) 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₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Primrec G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Primrec₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
m1 : (unpair m).1 < n + 4
m2 : (unpair m).2 < n + 4
⊢ (bif n.bodd then
      bif n.div2.bodd then rf a (ofNat Code n.div2.div2, F a (ofNat Code n.div2.div2))
      else
        pc a
          (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2,
            F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2))
    else
      bif n.div2.bodd then
        co a
          (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2,
            F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2))
      else
        pr a
          (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2,
            F a (ofNat Code (unpair n.div2.div2).1), F a (ofNat Code (unpair n.div2.div2).2))) =
    F a (ofNat Code (n + 4))
have succ : (bif n.bodd then
    bif n.div2.bodd then rf a (ofNat Code n.div2.div2, F a (ofNat Code n.div2.div2))
    else
      pc a
        (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1),
          F a (ofNat Code (unpair n.div2.div2).2))
  else
    bif n.div2.bodd then
      co a
        (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1),
          F a (ofNat Code (unpair n.div2.div2).2))
    else
      pr a
        (ofNat Code (unpair n.div2.div2).1, ofNat Code (unpair n.div2.div2).2, F a (ofNat Code (unpair n.div2.div2).1),
          F a (ofNat Code (unpair n.div2.div2).2))) =
  F a (ofNatCode (n + 4))
Tactic: rw [show ofNat Code (n + 4) = ofNatCode (n + 4) from rfl]