Dfa num state ge

theorem dfa_num_state_ge    {l : Language α} {ws : Set (List α)} [Finite ws]    (hws : ws.Pairwise (¬ (l.NerodeCongruence).r · ·))    {State : Type*} [Finite State] {M : DA.FinAcc State α} (hm : language M = l) :    Nat.card State ≥ Nat.card ws := by  -- In this proof it is easier to work with `Fintype` rather than `Finite` because of the use of  -- the theorem `Fintype.exists_ne_map_eq_of_card_lt` below.  have : Fintype State := Fintype.ofFinite _  have : Fintype ws := Fintype.ofFinite _  simp only [Nat.card_eq_fintype_card]  by_contra! h  by_cases h_card : Fintype.card ws ≤ 1  · grind [Fintype.card_pos_iff.mpr ⟨M.start⟩]  · obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, _, _⟩ :=      Fintype.exists_ne_map_eq_of_card_lt (f := fun w : ws ↦ M.mtr M.start w) h    grind [hws hx hy, da_nerodeCongruence_iff M x y]