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

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

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ len (same ⋯) = 0
Tactic:
unfold len
State after:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ 0 = 0

State before:
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
a✝¹ a✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : a✝¹ = a✝
val✝ : { x // x ∈ G.Z }
tail✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h_lhs : a✝¹ = Sum.inr val✝ :: tail✝
w : Word { x // x ∈ G.Z }
h_rhs : a✝ = Sum.inr <$> w
⊢ 0 = 0
Tactic:
rfl
State after:
no goals