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

State before:
α : Type u_1
xs : List α
i : Fin xs.length
⊢ (Index.ofFin i).val = xs.get i
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨0, _⟩ => rfl
  | ⟨i+1, _⟩ => simp [Index.ofFin, ih]
State after:
no goals

State before:
case nil
α : Type u_1
i : Fin [].length
⊢ (Index.ofFin i).val = [].get i
Tactic:
cases i
State after:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).val = [].get ⟨val✝, isLt✝⟩

State before:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).val = [].get ⟨val✝, isLt✝⟩
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).val = xs.get i
i : Fin (x :: xs).length
⊢ (Index.ofFin i).val = (x :: xs).get i
Tactic:
match i with
| ⟨0, _⟩ => rfl
| ⟨i+1, _⟩ => simp [Index.ofFin, ih]
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).val = xs.get i
i : Fin (x :: xs).length
isLt✝ : 0 < (x :: xs).length
⊢ (Index.ofFin ⟨0, isLt✝⟩).val = (x :: xs).get ⟨0, isLt✝⟩
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).val = xs.get i
i✝ : Fin (x :: xs).length
i : Nat
isLt✝ : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i + 1, isLt✝⟩).val = (x :: xs).get ⟨i + 1, isLt✝⟩
Tactic:
simp [Index.ofFin, ih]
State after:
no goals