fin cases bashing

Stream: kbb

[Johan Commelin]

@Scott Morrison Could your tactic also expand things like (↑(finset.sum finset.univ (λ (j : fin 2), A 0 j * B j 1))? I would like to write expand_fin; ring as proof of a goal I'm currently having... (working with 2x2 matrices)