Theorem: totalDFA_del_star_none (FormalSystems/Chomsky/Regular/TotalDFA.lean)

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ (DFA.toTotalDFA M).Z }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, w)) = none
Tactic:
induction' w with x xs ih
State after:
case nil
α qs : Type
M : DFA α qs
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, [])) = none

case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x :: xs)) = none

State before:
case nil
α qs : Type
M : DFA α qs
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, [])) = none

case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x :: xs)) = none
Tactic:
rfl
State after:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x :: xs)) = none

State before:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x :: xs)) = none
Tactic:
simp [TotalDFA.del_star']
State after:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x), xs)) =
    none

State before:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x), xs)) =
    none
Tactic:
have : M.toTotalDFA.δ' (⟨none, Fintype.complete _⟩, x) = ⟨none, Fintype.complete _⟩ := rfl
State after:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
this : TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x) = { val := none, property := ⋯ }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x), xs)) =
    none

State before:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
this : TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x) = { val := none, property := ⋯ }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x), xs)) =
    none
Tactic:
rw [this]
State after:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
this : TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x) = { val := none, property := ⋯ }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none

State before:
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
this : TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x) = { val := none, property := ⋯ }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
Tactic:
apply ih
State after:
no goals