mathlib3

9e4609b0 - chore(data/fintype/card): add `fin.prod_univ_{one,two}` (#9987)

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.