mathlib

658cd387 - feat(tactic/derive_fintype): derive fintype instances (#3772)

feat(tactic/derive_fintype): derive fintype instances (#3772) This adds a `@[derive fintype]` implementation, like so: ``` @[derive fintype] inductive foo (α : Type) | A : α → foo | B : α → α → foo | C : α × α → foo | D : foo ```