simp [HMul.hMul, Mul.mul]
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) =
    ↑{ val := ⟦w * (head✝ :: tail✝)⟧, property := ⋯ }
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) = ⟦w ++ head✝ :: tail✝⟧