internlm/Lean-Github huggingface dataset:
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))
Tactic:
unfold DFA.del_star_curried
Proof state after:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ M.δ (q, head✝) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ M.δ (q, head✝) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
Tactic:
rw [total_del_eq]
Proof state after:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ some (δ' M (q, head✝)) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ some (δ' M (q, head✝)) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
Tactic:
apply ih
Proof state after:
no goals
Theorem: TotalDFA.in_language_iff_del_star_final
Proof state before:
α qs : Type
M : TotalDFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M.toDFA ↔ del_star' M (M.q₀, w) ∈ M.F
Tactic:
rw [DFA.in_language_iff_del_star_final, total_del_star_eq]
Proof state after:
α qs : Type
M : TotalDFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ some (del_star' M (M.q₀, w)), qf ∈ M.F) ↔ del_star' M (M.q₀, w) ∈ M.F
Theorem: TotalDFA.in_language_iff_del_star_final
Proof state before:
α qs : Type
M : TotalDFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ some (del_star' M (M.q₀, w)), qf ∈ M.F) ↔ del_star' M (M.q₀, w) ∈ M.F
Tactic:
simp
Proof state after:
no goals
Theorem: totalDFA_del_eq_del
Proof state before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
a : { x // x ∈ M.Z }
⊢ M.δ (q, a) = ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, a))
Tactic:
simp [TotalDFA.δ']
Proof state after:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
a : { x // x ∈ M.Z }
⊢ M.δ (q, a) = ↑(Option.get ((DFA.toTotalDFA M).δ ({ val := some q, property := ⋯ }, a)) ⋯)
Theorem: totalDFA_del_eq_del
Proof state before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
a : { x // x ∈ M.Z }
⊢ M.δ (q, a) = ↑(Option.get ((DFA.toTotalDFA M).δ ({ val := some q, property := ⋯ }, a)) ⋯)
Tactic:
cases hd: M.δ _ <;> simp [DFA.toTotalDFA, hd]
Proof state after:
no goals
Theorem: totalDFA_del_star_none
Proof 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
Proof 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
Theorem: totalDFA_del_star_none
Proof 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
Proof 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
Theorem: totalDFA_del_star_none
Proof 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']
Proof 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
Theorem: totalDFA_del_star_none
Proof 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
Proof 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
Theorem: totalDFA_del_star_none
Proof 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]
Proof 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
Theorem: totalDFA_del_star_none
Proof 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
Proof state after:
no goals
Theorem: totalDFA_del_star_eq
Proof 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]
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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
Proof 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✝))
Theorem: totalDFA_del_star_eq
Proof 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
Proof state after:
no goals
Theorem: totalDFA_del_star_eq
Proof 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
Proof state after:
no goals
Theorem: totalDFA_del_star_eq
Proof 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
Proof state after:
no goals
Theorem: totalDFA_del_star_eq
Proof 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']
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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'
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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]
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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
Proof state after:
no goals
Theorem: totalDFA_del_star_eq
Proof 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
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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 _ ⟩
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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]
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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]
Proof state after:
no goals
Theorem: totalDFA_del_star_eq
Proof 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]
Proof 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))
Theorem: totalDFA_del_star_eq
Proof 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
Proof 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))