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

State before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
⊢ ↑p = eps v → DerivationStep.result (DerivationStep.fromRule p) = ε
Tactic:
intro h
State after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ DerivationStep.result (DerivationStep.fromRule p) = ε

State before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ DerivationStep.result (DerivationStep.fromRule p) = ε
Tactic:
simp [DerivationStep.fromRule, DerivationStep.result, h]
State after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ Production.rhs (eps v) = ε

State before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ Production.rhs (eps v) = ε
Tactic:
rfl
State after:
no goals