Theorem: Grammar.DerivationStep.augment_left_result (FormalSystems/Chomsky/Grammar.lean)

State before:
α 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 })
⊢ result (augment_left step w) = w * result step
Tactic:
unfold DerivationStep.result
State after:
α 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)

State before:
α 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)
Tactic:
unfold augment_left
State after:
α 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)

State before:
α 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)
Tactic:
simp [mul_assoc]
State after:
no goals