Theorem: del_star_eq (FormalSystems/Chomsky/Regular/Nerode.lean)

State before:
α✝ : 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))
w v : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, v)) = ↑{ val := ⟦w * v⟧, property := ⋯ }
Tactic:
induction v generalizing w
State after:
case nil
α✝ : 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))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, [])) =
    ↑{ val := ⟦w * []⟧, property := ⋯ }

case cons
α✝ : 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 }
tail_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 := ⋯ }

State before:
α✝ : 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))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, [])) =
    ↑{ val := ⟦w * []⟧, property := ⋯ }
Tactic:
case nil => simp [<-Word.eps_eq_nil, Word.monoid.mul_one]; rfl
State after:
no goals

State before:
α✝ : 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 := ⋯ }
Tactic:
case cons _ _ ih =>
  simp [HMul.hMul, Mul.mul]
  simp [TotalDFA.del_star']
  rw [List.append_cons]
  apply ih
State after:
no goals

State before:
α✝ : 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))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, [])) =
    ↑{ val := ⟦w * []⟧, property := ⋯ }
Tactic:
simp [<-Word.eps_eq_nil, Word.monoid.mul_one]
State after:
α✝ : 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))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, ε)) = ⟦w⟧

State before:
α✝ : 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))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, ε)) = ⟦w⟧
Tactic:
rfl
State after:
no goals

State before:
α✝ : 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 := ⋯ }
Tactic:
simp [HMul.hMul, Mul.mul]
State after:
α✝ : 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✝⟧

State before:
α✝ : 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✝⟧
Tactic:
simp [TotalDFA.del_star']
State after:
α✝ : 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)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ head✝ :: tail✝⟧

State before:
α✝ : 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)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ head✝ :: tail✝⟧
Tactic:
rw [List.append_cons]
State after:
α✝ : 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)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ [head✝] ++ tail✝⟧

State before:
α✝ : 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)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ [head✝] ++ tail✝⟧
Tactic:
apply ih
State after:
no goals