Theorem: foldFin_last (Controlbits/FoldFin.lean)

State before:
m : ℕ
⊢ foldFin m (Fin.last (2 * m)) = 0
Tactic:
cases' m with m
State after:
case zero

⊢ foldFin 0 (Fin.last (2 * 0)) = 0

case succ
m : ℕ
⊢ foldFin (m + 1) (Fin.last (2 * (m + 1))) = 0

State before:
case zero

⊢ foldFin 0 (Fin.last (2 * 0)) = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
m : ℕ
⊢ foldFin (m + 1) (Fin.last (2 * (m + 1))) = 0
Tactic:
rw [foldFin]
State after:
case succ
m : ℕ
⊢ (if h : ↑(Fin.last (2 * (m + 1))) < m + 1 + 1 then (Fin.last (2 * (m + 1))).castLT h
    else (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev) =
    0

State before:
case succ
m : ℕ
⊢ (if h : ↑(Fin.last (2 * (m + 1))) < m + 1 + 1 then (Fin.last (2 * (m + 1))).castLT h
    else (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev) =
    0
Tactic:
rw [dif_neg]
State after:
case succ
m : ℕ
⊢ (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = 0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1

State before:
case succ
m : ℕ
⊢ (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = 0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Tactic:
ext
State after:
case succ.h
m : ℕ
⊢ ↑(Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = ↑0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1

State before:
case succ.h
m : ℕ
⊢ ↑(Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = ↑0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Tactic:
simp
State after:
case succ.h
m : ℕ
⊢ m + 1 - (m + 1 + 1 + m - (m + 1)) = 0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1