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

State before:
⊢ @Index.toNat = @toNatTR
Tactic:
funext _ _ i
State after:
case h.h.h
x✝¹ : Type u_1
x✝ : List x✝¹
i : x✝.Index
⊢ i.toNat = i.toNatTR

State before:
case h.h.h
x✝¹ : Type u_1
x✝ : List x✝¹
i : x✝.Index
⊢ i.toNat = i.toNatTR
Tactic:
induction i with simp_all only [Index.toNat, toNatTR, toNatTR.loop]
| tail => rw [lem]
State after:
no goals

State before:
case h.h.h.tail
x✝² : Type u_1
x✝¹ xs✝ : List x✝²
x✝ : x✝²
a✝ : xs✝.Index
a_ih✝ : a✝.toNat = toNatTR.loop a✝ 0
⊢ toNatTR.loop a✝ 0 + 1 = toNatTR.loop a✝ (0 + 1)
Tactic:
rw [lem]
State after:
no goals

State before:
α : Type ?u.14515
xs : List α
i : xs.Index
n : Nat
⊢ toNatTR.loop i (n + 1) = toNatTR.loop i n + 1
Tactic:
induction i generalizing n with
| head => rfl
| tail _ ih => simp [toNatTR.loop, ih]
State after:
no goals

State before:
case head
α : Type ?u.14515
xs : List α
x✝ : α
xs✝ : List α
n : Nat
⊢ toNatTR.loop head (n + 1) = toNatTR.loop head n + 1
Tactic:
rfl
State after:
no goals

State before:
case tail
α : Type ?u.14515
xs xs✝ : List α
x✝ : α
a✝ : xs✝.Index
ih : ∀ (n : Nat), toNatTR.loop a✝ (n + 1) = toNatTR.loop a✝ n + 1
n : Nat
⊢ toNatTR.loop a✝.tail (n + 1) = toNatTR.loop a✝.tail n + 1
Tactic:
simp [toNatTR.loop, ih]
State after:
no goals