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

State before:
α✝ : Type u_1
xs : List α✝
i : xs.Index
⊢ Index.ofFin i.toFin = i
Tactic:
induction xs with
| nil => cases i
| cons x xs ih =>
  cases i with
  | head => rfl
  | tail i =>
    apply congrArg tail
    exact ih ..
State after:
no goals

State before:
case nil
α✝ : Type u_1
i : [].Index
⊢ Index.ofFin i.toFin = i
Tactic:
cases i
State after:
no goals

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : (x :: xs).Index
⊢ Index.ofFin i.toFin = i
Tactic:
cases i with
| head => rfl
| tail i =>
  apply congrArg tail
  exact ih ..
State after:
no goals

State before:
case cons.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
⊢ Index.ofFin head.toFin = head
Tactic:
rfl
State after:
no goals

State before:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : xs.Index
⊢ Index.ofFin i.tail.toFin = i.tail
Tactic:
apply congrArg tail
State after:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : xs.Index
⊢ Index.ofFin ⟨i.toNat, ⋯⟩ = i

State before:
case cons.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ (i : xs.Index), Index.ofFin i.toFin = i
i : xs.Index
⊢ Index.ofFin ⟨i.toNat, ⋯⟩ = i
Tactic:
exact ih ..
State after:
no goals