Theorem: List.Index.toNat_lt_length (Extra/Index/Basic.lean)

State before:
α✝ : Type u_1
xs : List α✝
i : xs.Index
⊢ i.toNat < xs.length
Tactic:
induction xs with
| nil => cases i
| cons x xs ih =>
  cases i with
  | head => exact Nat.zero_lt_succ ..
  | tail => apply Nat.succ_lt_succ (ih _)
State after:
no goals

State before:
case nil
α✝ : Type u_1
i : [].Index
⊢ i.toNat < [].length
Tactic:
cases i
State after:
no goals

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), i.toNat < xs.length
i : (x :: xs).Index
⊢ i.toNat < (x :: xs).length
Tactic:
cases i with
| head => exact Nat.zero_lt_succ ..
| tail => apply Nat.succ_lt_succ (ih _)
State after:
no goals

State before:
case cons.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), i.toNat < xs.length
⊢ head.toNat < (x :: xs).length
Tactic:
exact Nat.zero_lt_succ ..
State after:
no goals

State before:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), i.toNat < xs.length
a✝ : xs.Index
⊢ a✝.tail.toNat < (x :: xs).length
Tactic:
apply Nat.succ_lt_succ (ih _)
State after:
no goals