-- Mathlib/Computability/Halting.lean
theorem rfindOpt {n} {f : List.Vector ℕ (n + 1) → ℕ} (hf : @Partrec' (n + 1) f) :
    @Partrec' n fun v => Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v)) :=
  ((rfind <|
        (of_prim (Primrec.nat_sub.comp (_root_.Primrec.const 1) Primrec.vector_head)).comp₁
          (fun n => Part.some (1 - n)) hf).bind
    ((prim Nat.Primrec'.pred).comp₁ Nat.pred hf)).of_eq
    fun v =>
    Part.ext fun b => by
      simp only [Nat.rfindOpt, exists_prop, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
        Part.mem_some_iff, Option.mem_def, Part.mem_coe]
      refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)
      · congr
        funext n
        cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ] <;> rfl
      · have := Nat.rfind_spec h
        simp only [Part.coe_some, Part.mem_some_iff] at this
        revert this; rcases f (a ::ᵥ v) with - | c <;> intro this
        · cases this
        rw [← Option.some_inj, eq_comm]
        rfl

Proof state:
case refine_1
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
⊢ (a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome))

Tactic:
congr

Result:
case refine_1.e_a.e_p
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
⊢ (fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) = fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)

Proof state:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (∃ a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
refine
  exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)

Result:
case refine_1
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
⊢ (a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome))

case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Proof state:
case refine_1.e_a.e_p
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
⊢ (fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) = fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)

Tactic:
funext n

Result:
case refine_1.e_a.e_p.h
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (ofNat (Option ℕ) (f (n ::ᵥ v))).isSome)

Proof state:
case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome → (b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)

Tactic:
rcases f (a ::ᵥ v) with - | c <;> intro this

Result:
case refine_2.zero
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
this : true = (ofNat (Option ℕ) 0).isSome
⊢ b = pred 0 ↔ ofNat (Option ℕ) 0 = some b

case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b

Proof state:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
this : true ∈ ↑(some (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
simp only [Part.coe_some, Part.mem_some_iff] at this

Result:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
this : true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Proof state:
case refine_1.e_a.e_p.h
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (ofNat (Option ℕ) (f (n ::ᵥ v))).isSome)

Tactic:
cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ] <;> rfl

Result:
no goals

Proof state:
case refine_2.zero
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
this : true = (ofNat (Option ℕ) 0).isSome
⊢ b = pred 0 ↔ ofNat (Option ℕ) 0 = some b

Tactic:
cases this

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (b ∈ (Nat.rfind fun n_1 => Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))).bind fun a => ↑pred (f (a ::ᵥ v))) ↔
    b ∈ Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v))

Tactic:
simp only [Nat.rfindOpt, exists_prop, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
  Part.mem_some_iff, Option.mem_def, Part.mem_coe]

Result:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (∃ a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Proof state:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
this : true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
revert this

Result:
case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome → (b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)

Proof state:
case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
rw [← Option.some_inj, eq_comm]

Result:
case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b