-- Mathlib/Computability/Partrec.lean
theorem ppred : Partrec fun n => ppred n :=
  have : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1 :=
    (Primrec.ite
      (@PrimrecRel.comp _ _ _ _ _ _ _ _ _ _
        Primrec.eq Primrec.fst (_root_.Primrec.succ.comp Primrec.snd))
      (_root_.Primrec.const 0) (_root_.Primrec.const 1)).to₂
  (of_primrec (Primrec₂.unpaired'.2 this)).rfind.of_eq fun n => by
    cases n <;> simp
    · exact
        eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by
          simp [show 0 ≠ m.succ by intro h; injection h] at h
    · refine eq_some_iff.2 ?_
      simp only [mem_rfind, not_true, IsEmpty.forall_iff, decide_true, mem_some_iff,
        false_eq_decide_iff, true_and]
      intro m h
      simp [ne_of_gt h]

Proof state:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ : ℕ
⊢ n✝ ∈ Nat.rfind fun n => Part.some (decide (n✝ = n))

Tactic:
simp only [mem_rfind, not_true, IsEmpty.forall_iff, decide_true, mem_some_iff,
  false_eq_decide_iff, true_and]

Result:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬n✝ = m

Proof state:
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h : true ∈ (fun n => Part.some false) m
right✝ : ∀ k < m, ((fun n => Part.some false) k).Dom
h✝ : (Nat.rfind fun n => Part.some false).get ⋯ = a
⊢ 0 ≠ m.succ

Tactic:
intro h

Result:
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h✝¹ : true ∈ (fun n => Part.some false) m
right✝ : ∀ k < m, ((fun n => Part.some false) k).Dom
h✝ : (Nat.rfind fun n => Part.some false).get ⋯ = a
h : 0 = m.succ
⊢ False

Proof state:
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n : ℕ
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$> ↑(unpaired fun n m => if n = m.succ then 0 else 1) (Nat.pair n n_1)) =
    ↑n.ppred

Tactic:
cases n <;> simp

Result:
case zero
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
⊢ (Nat.rfind fun n => Part.some false) = Part.none

case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ : ℕ
⊢ (Nat.rfind fun n => Part.some (decide (n✝ = n))) = Part.some n✝

Proof state:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬n✝ = m

Tactic:
intro m h

Result:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ m : ℕ
h : m < n✝
⊢ ¬n✝ = m

Proof state:
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h✝¹ : true ∈ (fun n => Part.some false) m
right✝ : ∀ k < m, ((fun n => Part.some false) k).Dom
h✝ : (Nat.rfind fun n => Part.some false).get ⋯ = a
h : 0 = m.succ
⊢ False

Tactic:
injection h

Result:
no goals

Proof state:
case zero
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
⊢ (Nat.rfind fun n => Part.some false) = Part.none

Tactic:
exact
  eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by
    simp [show 0 ≠ m.succ by intro h; injection h] at h

Result:
no goals

Proof state:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ m : ℕ
h : m < n✝
⊢ ¬n✝ = m

Tactic:
simp [ne_of_gt h]

Result:
no goals

Proof state:
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
a : ℕ
x✝ : a ∈ Nat.rfind fun n => Part.some false
m : ℕ
h : true ∈ (fun n => Part.some false) m
right✝ : ∀ k < m, ((fun n => Part.some false) k).Dom
h✝ : (Nat.rfind fun n => Part.some false).get ⋯ = a
⊢ False

Tactic:
simp [show 0 ≠ m.succ by intro h; injection h] at h

Result:
no goals

Proof state:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ : ℕ
⊢ (Nat.rfind fun n => Part.some (decide (n✝ = n))) = Part.some n✝

Tactic:
refine eq_some_iff.2 ?_

Result:
case succ
this : Primrec₂ fun n m => if n = m.succ then 0 else 1
n✝ : ℕ
⊢ n✝ ∈ Nat.rfind fun n => Part.some (decide (n✝ = n))