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

case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ (Nat.rfind fun n => Part.some (decide (¬n✝ = n → False))) = Part.some n✝
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n : ℕ
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$> ↑(unpaired fun n m => if n = Nat.succ m then 0 else 1) (Nat.pair n n_1)) =
    ↑(Nat.ppred n)
cases n <;> simp
no goals
case zero
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
⊢ (Nat.rfind fun n => Part.some false) = Part.none
exact
  eq_none_iff.2 fun a ⟨⟨m, h, _⟩, _⟩ => by
    simp [show 0 ≠ m.succ by intro h; injection h] at h
no goals
this : Primrec₂ fun n m => if n = Nat.succ m 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 : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
⊢ False
simp [show 0 ≠ m.succ by intro h; injection h] at h
this : Primrec₂ fun n m => if n = Nat.succ m 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 : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
h : 0 = Nat.succ m
⊢ False
this : Primrec₂ fun n m => if n = Nat.succ m 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 : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
⊢ 0 ≠ Nat.succ m
intro h
no goals
this : Primrec₂ fun n m => if n = Nat.succ m 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 : ℕ), k < m → ((fun n => Part.some false) k).Dom
h✝ :
  Part.get (Nat.rfind fun n => Part.some false)
      (_ : ∃ n, true ∈ (fun n => Part.some false) n ∧ ∀ (k : ℕ), k < n → ((fun n => Part.some false) k).Dom) =
    a
h : 0 = Nat.succ m
⊢ False
injection h
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ n✝ ∈ Nat.rfind fun n => Part.some (decide (¬n✝ = n → False))
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ (Nat.rfind fun n => Part.some (decide (¬n✝ = n → False))) = Part.some n✝
refine' eq_some_iff.2 _
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬(¬n✝ = m → False)
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ n✝ ∈ Nat.rfind fun n => Part.some (decide (¬n✝ = n → False))
simp
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ m : ℕ
h : m < n✝
⊢ ¬(¬n✝ = m → False)
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬(¬n✝ = m → False)
intro m h
no goals
case succ
this : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1
n✝ m : ℕ
h : m < n✝
⊢ ¬(¬n✝ = m → False)
simp [ne_of_gt h]