-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ 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)
⊢ Computable (σ := σ) fun (p : (((Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) × σ) × σ) × σ) ↦
    bif p.1.1.1.2.1.bodd then
      bif p.1.1.1.2.1.div2.bodd then rf p.1.1.1.1.1 (ofNat Code p.1.1.1.2.2, p.1.1.2)
      else pc p.1.1.1.1.1 (ofNat Code (unpair p.1.1.1.2.2).1, ofNat Code (unpair p.1.1.1.2.2).2, p.1.2, p.2)
    else
      bif p.1.1.1.2.1.div2.bodd then
        co p.1.1.1.1.1 (ofNat Code (unpair p.1.1.1.2.2).1, ofNat Code (unpair p.1.1.1.2.2).2, p.1.2, p.2)
      else pr p.1.1.1.1.1 (ofNat Code (unpair p.1.1.1.2.2).1, ofNat Code (unpair p.1.1.1.2.2).2, p.1.2, p.2)

Tactic:
exact
      have a := fst.comp (fst.comp <| fst.comp <| fst.comp fst)
      have n := fst.comp (snd.comp <| fst.comp <| fst.comp fst)
      have m := snd.comp (snd.comp <| fst.comp <| fst.comp fst)
      have m₁ := fst.comp (Computable.unpair.comp m)
      have m₂ := snd.comp (Computable.unpair.comp m)
      have s := snd.comp (fst.comp fst)
      have s₁ := snd.comp fst
      have s₂ := snd
      (nat_bodd.comp n).cond
        ((nat_bodd.comp <| nat_div2.comp n).cond
          (hrf.comp a (((Computable.ofNat Code).comp m).pair s))
          (hpc.comp a (((Computable.ofNat Code).comp m₁).pair <|
            ((Computable.ofNat Code).comp m₂).pair <| s₁.pair s₂)))
        (Computable.cond (nat_bodd.comp <| nat_div2.comp n)
          (hco.comp a (((Computable.ofNat Code).comp m₁).pair <|
            ((Computable.ofNat Code).comp m₂).pair <| s₁.pair s₂))
          (hpr.comp a (((Computable.ofNat Code).comp m₁).pair <|
            ((Computable.ofNat Code).comp m₂).pair <| s₁.pair s₂)))

Premises used: Computable.ofNat, Nat.Partrec.Code, Computable.snd, Computable₂.comp, Computable.unpair, Computable.comp, Computable.pair, Computable.fst, Computable.cond, Computable.nat_div2, Computable.nat_bodd