Theorem: List.get?_isSome_iff (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : List α
n : ℕ
⊢ Option.isSome (get? x n) = true ↔ n < length x
Tactic:
rw [← not_iff_not]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : List α
n : ℕ
⊢ ¬Option.isSome (get? x n) = true ↔ ¬n < length x

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : List α
n : ℕ
⊢ ¬Option.isSome (get? x n) = true ↔ ¬n < length x
Tactic:
simp [Option.isNone_iff_eq_none]
State after:
no goals