Theorem: foldFinCastLE (Controlbits/FoldFin.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ foldFin m (Fin.castLE ⋯ i) = i
Tactic:
rw [Fin.ext_iff, coe_foldFinLE (Nat.le_of_lt_succ i.isLt), Fin.coe_castLE]
State after:
no goals