rw [@Quotient.lift_mk _ _ (myhillNerodeEquivalence L) _ _ _]
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ Quotient.lift (fun x => x ∈ L) ⋯ ⟦w⟧ ↔ w ∈ L
no goals