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

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

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

State before:
case nil.mk
α : Type u_1
val✝ : Nat
isLt✝ : val✝ < [].length
⊢ (Index.ofFin ⟨val✝, isLt✝⟩).toNat = ↑⟨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).toNat = ↑i
i : Fin (x :: xs).length
⊢ (Index.ofFin i).toNat = ↑i
Tactic:
match i with
| ⟨0,_⟩ => rfl
| ⟨i+1,h⟩ =>
  apply congrArg Nat.succ
  rw [ih]
State after:
no goals

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

State before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i✝ : Fin (x :: xs).length
i : Nat
h : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i + 1, h⟩).toNat = ↑⟨i + 1, h⟩
Tactic:
apply congrArg Nat.succ
State after:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i✝ : Fin (x :: xs).length
i : Nat
h : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i, ⋯⟩).toNat = i

State before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : Fin xs.length), (Index.ofFin i).toNat = ↑i
i✝ : Fin (x :: xs).length
i : Nat
h : i + 1 < (x :: xs).length
⊢ (Index.ofFin ⟨i, ⋯⟩).toNat = i
Tactic:
rw [ih]
State after:
no goals