-- Mathlib/Computability/Partrec.lean
theorem nat_casesOn_right {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ} (hf : Computable f)
    (hg : Computable g) (hh : Partrec₂ h) : Partrec fun a => (f a).casesOn (some (g a)) (h a) :=
  (nat_rec hf hg (hh.comp fst (pred.comp <| hf.comp fst)).to₂).of_eq fun a => by
    simp only [PFun.coe_val, Nat.pred_eq_sub_one]; rcases f a with - | n <;> simp
    refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩
    · rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩
      exact h₂
    · have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
          (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom

Proof state:
case succ.refine_1
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n
⊢ b ∈ h a n

Tactic:
rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩

Result:
case succ.refine_1.intro.intro
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n
c : σ
left✝ : c ∈ Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n
h₂ : b ∈ h a n
⊢ b ∈ h a n

Proof state:
case succ.refine_2
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n

Tactic:
have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
    (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
  intro m
  induction m <;> simp [*, H.fst]

Result:
case succ.refine_2
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
this : ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
⊢ b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a (f a - 1)) (f a) =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (f a)

Tactic:
rcases f a with - | n <;> simp

Result:
case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ ((Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n) = h a n

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH => IH.bind fun i => h (a, y, i).1 (f (a, y, i).1).pred) (f a) =
    Nat.casesOn (f a) (Part.some (g a)) (h a)

Tactic:
simp only [PFun.coe_val, Nat.pred_eq_sub_one]

Result:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a (f a - 1)) (f a) =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (f a)

Proof state:
case succ.refine_2
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
this : ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
⊢ b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n

Tactic:
exact ⟨⟨this n, H.fst⟩, H.snd⟩

Result:
no goals

Proof state:
case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ ((Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n) = h a n

Tactic:
refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩

Result:
case succ.refine_1
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n
⊢ b ∈ h a n

case succ.refine_2
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n

Proof state:
case succ.refine_1.intro.intro
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ (Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n).bind fun i => h a n
c : σ
left✝ : c ∈ Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => h a n) n
h₂ : b ∈ h a n
⊢ b ∈ h a n

Tactic:
exact h₂

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom

Tactic:
intro m

Result:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
m : ℕ
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
m : ℕ
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom

Tactic:
induction m <;> simp [*, H.fst]

Result:
no goals