Theorem: Grammar.Derivation.trans (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✝ u v w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
d1 : Derivation G u v
d2 : Derivation G v w
⊢ Derivation G u w
Tactic:
induction d1 with
| same h => exact h ▸ d2
| step l _ sound ih => exact step l (ih d2) sound
State after:
no goals

State before:
case same
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : u✝ = v✝
d2 : Derivation G v✝ w
⊢ Derivation G u✝ w
Tactic:
exact h ▸ d2
State after:
no goals

State before:
case step
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
l : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result l = u'✝
ih : Derivation G v✝ w → Derivation G u'✝ w
d2 : Derivation G v✝ w
⊢ Derivation G u✝ w
Tactic:
exact step l (ih d2) sound
State after:
no goals