Unique minimal

theorem unique_minimal [Finite State]    (l : Language α) (hr : l.IsRegular) (hm : M.IsMinimalAutomaton l) :    ∃! φ : State ≃ l.NerodeQuotient, ∀ x, φ (M.mtr M.start x) = ⟦ x ⟧ := by  obtain ⟨rfl, hc⟩ := hm  have := Language.IsRegular.iff_finite_nerodeQuotient.mp hr  let φ : State → Quotient ((language M).NerodeCongruence).eq :=    fun s ↦ ⟦ Classical.epsilon (fun x : List α ↦ M.mtr M.start x = s) ⟧  have hφ (x : List α) : φ (M.mtr M.start x) = ⟦ x ⟧ := by    apply Quotient.sound    apply stateCongruence_le_nerodeCongruence    intro z    have := @Classical.epsilon_spec _ (fun y : List α ↦ M.mtr M.start y = M.mtr M.start x) ⟨x, rfl⟩    grind [FLTS.mtr]  have hφ_surj : Function.Surjective φ := fun q ↦ q.inductionOn (fun x ↦ ⟨M.mtr M.start x, hφ x⟩)  have hφ_inj : Function.Injective φ := by    have eqT := Classical.inhabited_of_nonempty <| Finite.card_eq.mp hc    apply hφ_surj.injective_of_finite eqT.default  use Equiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩, hφ  intro ψ hψ  ext s  induction h : φ s using Quotient.inductionOn with  | h x => grind [hφ_inj ((hφ x).trans h.symm)]