Commit 2021-10-27 17:47 9e4609b0
View on Github →chore(data/fintype/card): add fin.prod_univ_{one,two} (#9987)
Sometimes Lean fails to simplify (default : fin 1) to 0 and
0.succ to 1 in complex expressions. These lemmas explicitly use
f 0 and f 1 in the output.