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

State before:
α✝¹ : Type
Z : Finset α✝¹
α✝ : Type
V : Finset α✝
p : RegularProduction Z V
⊢ Production.rhs p = Word.mk (Sum.inr <$> Option.toList (getRhs p).1) * Word.mk (Sum.inl <$> Option.toList (getRhs p).2)
Tactic:
cases p <;> rfl
State after:
no goals