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

State before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star M (q, w) = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, w))
Tactic:
simp [DFA.del_star]
State after:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star_curried M w q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, w))

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

case cons
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
tail_ih✝ :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M tail✝ q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M (head✝ :: tail✝) q =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝ :: tail✝))

State before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M [] q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, []))
Tactic:
case nil => rfl
State after:
no goals

State before:
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M (head✝ :: xs) q =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝ :: xs))
Tactic:
case cons _ xs ih =>
  simp [DFA.del_star_curried, Option.bind_eq_bind, TotalDFA.del_star']
  cases' hd: M.δ _ with q'
  . rw [totalDFA_del_eq_del] at hd
    let q' : M.toTotalDFA.Q := ⟨ none, Fintype.complete _ ⟩
    have : q'.val = none := rfl
    rw [<-this] at hd
    simp [Subtype.eq hd]
    rw [totalDFA_del_star_none]
  . rw [Option.some_bind]
    rw [totalDFA_del_eq_del] at hd
    let q' : M.toTotalDFA.Q := ⟨ some q', Fintype.complete _ ⟩
    have : q'.val = some _ := rfl
    rw [<-this] at hd
    rw [Subtype.eq hd]
    apply ih
State after:
no goals

State before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M [] q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, []))
Tactic:
rfl
State after:
no goals

State before:
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M (head✝ :: xs) q =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝ :: xs))
Tactic:
simp [DFA.del_star_curried, Option.bind_eq_bind, TotalDFA.del_star']
State after:
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
⊢ Option.bind (M.δ (q, head✝)) (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
⊢ Option.bind (M.δ (q, head✝)) (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
cases' hd: M.δ _ with q'
State after:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ Option.bind (some q') (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ Option.bind (some q') (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
. rw [totalDFA_del_eq_del] at hd
  let q' : M.toTotalDFA.Q := ⟨ none, Fintype.complete _ ⟩
  have : q'.val = none := rfl
  rw [<-this] at hd
  simp [Subtype.eq hd]
  rw [totalDFA_del_star_none]
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ Option.bind (some q') (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ Option.bind (some q') (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
. rw [Option.some_bind]
  rw [totalDFA_del_eq_del] at hd
  let q' : M.toTotalDFA.Q := ⟨ some q', Fintype.complete _ ⟩
  have : q'.val = some _ := rfl
  rw [<-this] at hd
  rw [Subtype.eq hd]
  apply ih
State after:
no goals

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [totalDFA_del_eq_del] at hd
State after:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
let q' : M.toTotalDFA.Q := ⟨ none, Fintype.complete _ ⟩
State after:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = none
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = none
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
have : q'.val = none := rfl
State after:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = none
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
this : ↑q' = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = none
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
this : ↑q' = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [<-this] at hd
State after:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = none
⊢ Option.bind none (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
simp [Subtype.eq hd]
State after:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = none
⊢ none = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))

State before:
case none
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := none, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = none
⊢ none = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))
Tactic:
rw [totalDFA_del_star_none]
State after:
no goals

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ Option.bind (some q') (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [Option.some_bind]
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ DFA.del_star_curried M xs q' =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : M.δ (q, head✝) = some q'
⊢ DFA.del_star_curried M xs q' =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [totalDFA_del_eq_del] at hd
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'
⊢ DFA.del_star_curried M xs q' =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q' : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'
⊢ DFA.del_star_curried M xs q' =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
let q' : M.toTotalDFA.Q := ⟨ some q', Fintype.complete _ ⟩
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
have : q'.val = some _ := rfl
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = some q'✝
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [<-this] at hd
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
Tactic:
rw [Subtype.eq hd]
State after:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))

State before:
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))
Tactic:
apply ih
State after:
no goals