Theorem: Grammar.Derivation.cancelLeft_len (FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean)

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
⊢ len (cancelLeft d h_lhs h_rhs) = len d
Tactic:
match d with
| .same _ => simp [len]
| .step _ _ _ =>
  simp [len]
  apply cancelLeft_len
State after:
no goals

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
h✝ : lhs = rhs
⊢ len (cancelLeft (same h✝) h_lhs h_rhs) = len (same h✝)
Tactic:
simp [len]
State after:
no goals

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step✝ : DerivationStep G lhs
x✝ : Derivation G u'✝ rhs
sound✝ : DerivationStep.result step✝ = u'✝
⊢ len (cancelLeft (step step✝ x✝ sound✝) h_lhs h_rhs) = len (step step✝ x✝ sound✝)
Tactic:
simp [len]
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step✝ : DerivationStep G lhs
x✝ : Derivation G u'✝ rhs
sound✝ : DerivationStep.result step✝ = u'✝
⊢ len (cancelLeft x✝ ⋯ h_rhs) = len x✝

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : lhs = Sum.inr val✝ :: tail✝
a✝ : Word { x // x ∈ G.Z }
h_rhs : rhs = Sum.inr <$> a✝
d : Derivation G lhs rhs
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
step✝ : DerivationStep G lhs
x✝ : Derivation G u'✝ rhs
sound✝ : DerivationStep.result step✝ = u'✝
⊢ len (cancelLeft x✝ ⋯ h_rhs) = len x✝
Tactic:
apply cancelLeft_len
State after:
no goals