Theorem: RegularProduction.cons_step_result (FormalSystems/Chomsky/Regular/RegularGrammar.lean)

State before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
⊢ ↑p = cons v (w, b) → DerivationStep.result (DerivationStep.fromRule p) = [Sum.inr w, Sum.inl b]
Tactic:
intro h
State after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ DerivationStep.result (DerivationStep.fromRule p) = [Sum.inr w, Sum.inl b]

State before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ DerivationStep.result (DerivationStep.fromRule p) = [Sum.inr w, Sum.inl b]
Tactic:
simp [DerivationStep.fromRule, DerivationStep.result, h]
State after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ Production.rhs (cons v (w, b)) = [Sum.inr w, Sum.inl b]

State before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ Production.rhs (cons v (w, b)) = [Sum.inr w, Sum.inl b]
Tactic:
rfl
State after:
no goals