chore: simplify the DFA example (#430)

The `deriving Fintype` machinery in mathlib already does the hard work
here, and the `Finite` theorems were useless.

Author: eric-wieser

CslibTests/DFA.lean

@@ -15,37 +15,19 @@ open Cslib.Automata
 inductive Floor where
 | one
 | two
-deriving DecidableEq
-
-def Floor.fintype : Fintype Floor := {
-  elems := {.one, .two}
-  complete floor := by grind [Floor]
-}
-
-theorem Floor.finite : Finite Floor := Floor.fintype.finite
+deriving DecidableEq, Fintype
 
 inductive Direction where
 | up
 | down
-deriving DecidableEq
-
-def Direction.fintype : Fintype Direction := {
-  elems := {.up, .down}
-  complete dir := by grind [Direction]
-}
+deriving DecidableEq, Fintype
 
-theorem Direction.finite : Finite Direction := Direction.fintype.finite
-
-def tr (floor : Floor) (dir : Direction) : Floor :=
-  match floor, dir with
+def elevator : DA Floor Direction where
+  tr
   | .one, .up => .two
   | .one, .down => .one
   | .two, .up => .two
   | .two, .down => .one
-
-def elevator : DA Floor Direction := {
-  tr := tr
   start := .one
-}
 
 end CslibTests