Theorem: DFA.toGrammar_prod_imp_transition (FormalSystems/Chomsky/Regular/DFA.lean)

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h : RegularProduction.cons v (a, v') ∈ (toGrammar M).productions
⊢ M.δ (v, a) = some v'
Tactic:
simp [toGrammar, transitionToRule] at h
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'
Tactic:
have ⟨_, _, _, _, _, _, _, _, c1, c2, c3⟩ := h
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'
Tactic:
rw [<- c1, <- c2, <- c3]
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
Tactic:
assumption
State after:
no goals