-- Mathlib/Computability/Partrec.lean
theorem rfind {p : α → ℕ →. Bool} (hp : Partrec₂ p) : Partrec fun a => Nat.rfind (p a) :=
  (Nat.Partrec.rfind <|
        hp.map ((Primrec.dom_bool fun b => cond b 0 1).comp Primrec.snd).to₂.to_comp).of_eq
    fun n => by
    rcases e : decode (α := α) n with - | a <;> simp [e, Nat.rfind_zero_none, map_id']
    congr; funext n
    simp only [map_map, Function.comp]
    refine map_id' (fun b => ?_) _
    cases b <;> rfl

Proof state:
case some.e_p.h
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map ((fun m => decide (m = 0)) ∘ fun b => bif b then 0 else 1) (p a n) = p a n

Tactic:
refine map_id' (fun b => ?_) _

Result:
case some.e_p.h
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
b : Bool
⊢ ((fun m => decide (m = 0)) ∘ fun b => bif b then 0 else 1) b = b

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a =>
          Part.map encode ((fun a => Part.map (fun b => bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑(decode n)).bind fun a => Part.map encode ((fun a => Nat.rfind (p a)) a)

Tactic:
rcases e : decode (α := α) n with - | a <;> simp [e, Nat.rfind_zero_none, map_id']

Result:
case some
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) =
    Nat.rfind (p a)

Proof state:
case some.e_p.h
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n)) = p a n

Tactic:
simp only [map_map, Function.comp]

Result:
case some.e_p.h
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map ((fun m => decide (m = 0)) ∘ fun b => bif b then 0 else 1) (p a n) = p a n

Proof state:
case some.e_p.h
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
b : Bool
⊢ ((fun m => decide (m = 0)) ∘ fun b => bif b then 0 else 1) b = b

Tactic:
cases b <;> rfl

Result:
no goals

Proof state:
case some.e_p
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = p a

Tactic:
funext n

Result:
case some.e_p.h
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n)) = p a n

Proof state:
case some
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) =
    Nat.rfind (p a)

Tactic:
congr

Result:
case some.e_p
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = p a