n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b : ℕ
⊢ (∃ a, (a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) ∧ b = pred (f (a ::ᵥ v))) ↔
    ∃ a,
      (a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))) ∧
        ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b : ℕ
⊢ (b ∈ Part.bind (Nat.rfind fun n_1 => Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))) fun a => ↑pred (f (a ::ᵥ v))) ↔
    b ∈ Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v))
simp only [Nat.rfindOpt, exists_prop, tsub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
  Part.mem_some_iff, Option.mem_def, Part.mem_coe]
case refine'_1
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : 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 (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))))

case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b : ℕ
⊢ (∃ a, (a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) ∧ b = pred (f (a ::ᵥ v))) ↔
    ∃ a,
      (a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))) ∧
        ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
refine'
  exists_congr fun a => (and_congr (iff_of_eq _) Iff.rfl).trans (and_congr_right fun h => _)
case refine'_1.e_a.e_p
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
⊢ (fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) = fun n_1 =>
    ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
case refine'_1
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : 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 (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))))
congr
case refine'_1.e_a.e_p.h
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (Option.isSome (ofNat (Option ℕ) (f (n ::ᵥ v)))))
case refine'_1.e_a.e_p
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
⊢ (fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) = fun n_1 =>
    ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
funext n
case refine'_1.e_a.e_p.h
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (Option.isSome (ofNat (Option ℕ) (f (n ::ᵥ v)))))
case refine'_1.e_a.e_p.h
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (Option.isSome (ofNat (Option ℕ) (f (n ::ᵥ v)))))
simp only [Part.some_inj, PFun.coe_val]
case refine'_1.e_a.e_p.h.succ
n✝¹ : ℕ
f : Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ true = Option.isSome (ofNat (Option ℕ) (succ n✝))
case refine'_1.e_a.e_p.h
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (Option.isSome (ofNat (Option ℕ) (f (n ::ᵥ v)))))
cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ]
no goals
case refine'_1.e_a.e_p.h.succ
n✝¹ : ℕ
f : Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ true = Option.isSome (ofNat (Option ℕ) (succ n✝))
rfl
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true ∈ ↑(some (Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v)))))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have := Nat.rfind_spec h
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true = Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v)))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true ∈ ↑(some (Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v)))))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
simp only [Part.coe_some, Part.mem_some_iff] at this
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ true = Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v))) →
    (b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true = Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v)))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
revert this
case refine'_2.zero
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true = Option.isSome (ofNat (Option ℕ) zero)
⊢ b = pred zero ↔ ofNat (Option ℕ) zero = some b

case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
this : true = Option.isSome (ofNat (Option ℕ) (succ c))
⊢ b = pred (succ c) ↔ ofNat (Option ℕ) (succ c) = some b
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ true = Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v))) →
    (b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)
cases' f (a ::ᵥ v) with c <;> intro this
case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
this : true = Option.isSome (ofNat (Option ℕ) (succ c))
⊢ some (pred (succ c)) = some b ↔ ofNat (Option ℕ) (succ c) = some b
case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
this : true = Option.isSome (ofNat (Option ℕ) (succ c))
⊢ b = pred (succ c) ↔ ofNat (Option ℕ) (succ c) = some b
rw [← Option.some_inj, eq_comm]
no goals
case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
this : true = Option.isSome (ofNat (Option ℕ) (succ c))
⊢ some (pred (succ c)) = some b ↔ ofNat (Option ℕ) (succ c) = some b
rfl
no goals
case refine'_2.zero
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true = Option.isSome (ofNat (Option ℕ) zero)
⊢ b = pred zero ↔ ofNat (Option ℕ) zero = some b
cases this