-- Mathlib/Computability/Partrec.lean
theorem bind_decode_iff {f : α → β → Option σ} :
    (Computable₂ fun a n => (decode (α := β) n).bind (f a)) ↔ Computable₂ f :=
  ⟨fun hf =>
    Nat.Partrec.of_eq
      (((Partrec.nat_iff.2
        (Nat.Partrec.ppred.comp <| Nat.Partrec.of_primrec <| Primcodable.prim (α := β))).comp
            snd).bind
        (Computable.comp hf fst).to₂.partrec₂)
      fun n => by
        simp only [decode_prod_val, decode_nat, Option.map_some', PFun.coe_val, bind_eq_bind,
          bind_some, Part.map_bind, map_some]
        cases decode (α := α) n.unpair.1 <;> simp
        cases decode (α := β) n.unpair.2 <;> simp,
    fun hf => by
    have :
      Partrec fun a : α × ℕ =>
        (encode (decode (α := β) a.2)).casesOn (some Option.none)
          fun n => Part.map (f a.1) (decode (α := β) n) :=
      Partrec.nat_casesOn_right
        (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
        (Primrec.encdec.to_comp.comp snd) (const Option.none)
        ((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)
    refine this.of_eq fun a => ?_
    simp; cases decode (α := β) a.2 <;> simp [encodek]⟩

Proof state:
case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑(encode (decode (Nat.unpair n).2)).ppred).bind fun y =>
      Part.some (encode ((decode (Nat.unpair n).2).bind fun a => f val✝ a))) =
    (↑(Option.map (Prod.mk val✝) (decode (Nat.unpair n).2))).bind fun a => Part.some (encode (f a.1 a.2))

Tactic:
cases decode (α := β) n.unpair.2 <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => (decode n).bind (f a)
n : ℕ
⊢ ((↑((decode (Nat.unpair n).1).bind fun a => Option.some (a, (Nat.unpair n).2))).bind fun a =>
      (↑(encode (decode a.2)).ppred).bind fun y => Part.some (encode ((decode a.2).bind fun a_1 => f a.1 a_1))) =
    (↑((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a =>
      Part.some (encode (f a.1 a.2))

Tactic:
cases decode (α := α) n.unpair.1 <;> simp

Result:
case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑(encode (decode (Nat.unpair n).2)).ppred).bind fun y =>
      Part.some (encode ((decode (Nat.unpair n).2).bind fun a => f val✝ a))) =
    (↑(Option.map (Prod.mk val✝) (decode (Nat.unpair n).2))).bind fun a => Part.some (encode (f a.1 a.2))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)
a : α × ℕ
⊢ (Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)) =
    (↑fun p => (fun a n => (decode n).bind (f a)) p.1 p.2) a

Tactic:
simp

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)
a : α × ℕ
⊢ Nat.rec (Part.some Option.none) (fun n n_ih => map (f a.1) ↑(decode n)) (encode (decode a.2)) =
    Part.some ((decode a.2).bind (f a.1))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)
a : α × ℕ
⊢ Nat.rec (Part.some Option.none) (fun n n_ih => map (f a.1) ↑(decode n)) (encode (decode a.2)) =
    Part.some ((decode a.2).bind (f a.1))

Tactic:
cases decode (α := β) a.2 <;> simp [encodek]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => (decode n).bind (f a)
n : ℕ
⊢ ((↑(decode n)).bind fun a =>
      map encode
        ((fun a =>
            (do
                  let n ← (↑fun n => encode (decode n)) a.2
                  ↑n.ppred).bind
              ↑fun b => (fun a n => (decode n).bind (f a)) (a, b).1.1 (a, b).1.2)
          a)) =
    (↑(decode n)).bind fun a => map encode ((↑fun p => f p.1 p.2) a)

Tactic:
simp only [decode_prod_val, decode_nat, Option.map_some', PFun.coe_val, bind_eq_bind,
  bind_some, Part.map_bind, map_some]

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n => (decode n).bind (f a)
n : ℕ
⊢ ((↑((decode (Nat.unpair n).1).bind fun a => Option.some (a, (Nat.unpair n).2))).bind fun a =>
      (↑(encode (decode a.2)).ppred).bind fun y => Part.some (encode ((decode a.2).bind fun a_1 => f a.1 a_1))) =
    (↑((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a =>
      Part.some (encode (f a.1 a.2))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)
⊢ Computable₂ fun a n => (decode n).bind (f a)

Tactic:
refine this.of_eq fun a => ?_

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)
a : α × ℕ
⊢ (Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)) =
    (↑fun p => (fun a n => (decode n).bind (f a)) p.1 p.2) a

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ Computable₂ fun a n => (decode n).bind (f a)

Tactic:
have :
  Partrec fun a : α × ℕ =>
    (encode (decode (α := β) a.2)).casesOn (some Option.none)
      fun n => Part.map (f a.1) (decode (α := β) n) :=
  Partrec.nat_casesOn_right
    (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
    (Primrec.encdec.to_comp.comp snd) (const Option.none)
    ((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)
⊢ Computable₂ fun a n => (decode n).bind (f a)