Theorem: Nat.ArithPart₁.rfindPos (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f : Vector ℕ (n + 1) → ℕ
h : Arith₁ f
⊢ ∀ (i : Vector ℕ n),
    (Nat.rfind fun n_1 => Part.some (decide ((isLtNat 0 (f (n_1 ::ᵥ i))).inv = 0))) =
      Nat.rfind fun n_1 => Part.some (decide (0 < f (n_1 ::ᵥ i)))
Tactic:
simp
State after:
no goals