-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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.{u_1, u_2} (σ := σ) fun (a : α) ↦ F a (c a)
have this : Computable G₁
Tactic: have : Computable G₁ := by
    refine option_bind (list_getElem?.comp (snd.comp fst) (snd.comp snd)) <| .mk ?_
    refine option_bind ((list_getElem?.comp (snd.comp fst)
      (fst.comp <| Computable.unpair.comp (snd.comp snd))).comp fst) <| .mk ?_
    refine option_map ((list_getElem?.comp (snd.comp fst)
      (snd.comp <| Computable.unpair.comp (snd.comp snd))).comp <| fst.comp fst) <| .mk ?_
    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₂)))