Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : 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✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p ↦
    p.1.2[p.2.2]?.bind fun s ↦
      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₂))
          p.1.2[(unpair p.2.2).2]?
⊢ Computable fun p ↦
    Option.map
      (fun s₂ ↦
        bif p.1.1.2.1.bodd then
          bif p.1.1.2.1.div2.bodd then rf p.1.1.1.1 (ofNat Code p.1.1.2.2, p.1.2)
          else pc p.1.1.1.1 (ofNat Code (unpair p.1.1.2.2).1, ofNat Code (unpair p.1.1.2.2).2, p.2, s₂)
        else
          bif p.1.1.2.1.div2.bodd then
            co p.1.1.1.1 (ofNat Code (unpair p.1.1.2.2).1, ofNat Code (unpair p.1.1.2.2).2, p.2, s₂)
          else pr p.1.1.1.1 (ofNat Code (unpair p.1.1.2.2).1, ofNat Code (unpair p.1.1.2.2).2, p.2, s₂))
      p.1.1.1.2[(unpair p.1.1.2.2).2]?

Tactic:
refine option_map ((list_getElem?.comp (snd.comp fst)
      (snd.comp <| Computable.unpair.comp (snd.comp snd))).comp <| fst.comp fst) <| .mk ?_

Goal state after:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : 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✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p ↦
    p.1.2[p.2.2]?.bind fun s ↦
      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₂))
          p.1.2[(unpair p.2.2).2]?
⊢ Computable fun p ↦
    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)