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

State before:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
⊢ isEps p → p = eps (lhs p)
Tactic:
intro h
State after:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
h : isEps p
⊢ p = eps (lhs p)

State before:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
h : isEps p
⊢ p = eps (lhs p)
Tactic:
match p with
| .eps _ => rfl
State after:
no goals

State before:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
lhs✝ : { x // x ∈ V }
h : isEps (eps lhs✝)
⊢ eps lhs✝ = eps (lhs (eps lhs✝))
Tactic:
rfl
State after:
no goals