Dfa num state min

theorem dfa_num_state_min {State : Type} {M : DA.FinAcc State α} [Finite State] :    Nat.card State ≥ Nat.card (language M).NerodeQuotient := by  let ws : Set (List α) := Set.range (Quotient.out : NerodeQuotient (language M) → List α)  have : Finite (language M).NerodeQuotient :=      IsRegular.iff_finite_nerodeQuotient.mp (IsRegular.iff_dfa.mpr ⟨State, inferInstance, M, rfl⟩)  have : Finite ws := Set.finite_range _ |>.to_subtype  have hws : ws.Pairwise (fun x y ↦ ¬((language M).NerodeCongruence).r x y) := by    rintro _ ⟨qx, rfl⟩ _ ⟨qy, rfl⟩ hne h    apply hne    simpa using Quotient.sound h  have h1 := dfa_num_state_ge hws rfl  rw [Nat.card_congr (Equiv.ofInjective _ Quotient.out_injective).symm] at h1  assumption