unfold augment_left
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ (augment_left step w).pre * Production.rhs ↑(augment_left step w).prod * (augment_left step w).suf =
    w * (step.pre * Production.rhs ↑step.prod * step.suf)
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step : DerivationStep G u
w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
⊢ { prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.pre *
        Production.rhs ↑{ prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.prod *
      { prod := step.prod, pre := w * step.pre, suf := step.suf, sound := ⋯ }.suf =
    w * (step.pre * Production.rhs ↑step.prod * step.suf)