Theorem: Grammar.DerivationStep.lhs_singleton (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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ step.pre = ε ∧ step.suf = ε
Tactic:
match hpre:step.pre with
| .cons _ _ =>
  have tmp := Eq.symm $ hpre ▸ step.sound
  simp [mul_assoc, HMul.hMul, Mul.mul, List.cons_append] at tmp
  rw [List.cons_eq_cons] at tmp
  simp_rw [List.append_eq_nil] at tmp
  have tmp := tmp.2.2.1
  have ⟨_, h⟩ := Production.lhs_contains_var step.prod.val
  rw [tmp] at h
  contradiction
| .nil =>
  have tmp := Eq.symm $ hpre ▸ step.sound
  simp [<- Word.eps_eq_nil, Word.mul_eq_cons] at tmp
  cases tmp
  case inl h =>
    have ⟨_, c⟩ := Production.lhs_contains_var step.prod.val
    have ⟨h, _⟩ := h
    rw [h] at c
    contradiction
  case inr h =>
    have ⟨_, ⟨h₁, h₂⟩ ⟩ := h
    have tmp := Word.mul_eq_eps.mp $ Eq.symm h₂
    have tmp' := tmp.1 ▸ h₁
    simp at tmp'
    constructor
    . assumption
    . constructor; rfl; exact tmp.right
State after:
no goals

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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
have tmp := Eq.symm $ hpre ▸ step.sound
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : (head✝ :: tail✝) * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : (head✝ :: tail✝) * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
simp [mul_assoc, HMul.hMul, Mul.mul, List.cons_append] at tmp
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ :: (tail✝ ++ (Production.lhs ↑step.prod ++ step.suf)) = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ :: (tail✝ ++ (Production.lhs ↑step.prod ++ step.suf)) = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
rw [List.cons_eq_cons] at tmp
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ ++ (Production.lhs ↑step.prod ++ step.suf) = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ ++ (Production.lhs ↑step.prod ++ step.suf) = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
simp_rw [List.append_eq_nil] at tmp
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
have tmp := tmp.2.2.1
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
have ⟨_, h⟩ := Production.lhs_contains_var step.prod.val
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
rw [tmp] at h
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε
Tactic:
contradiction
State after:
no goals

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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have tmp := Eq.symm $ hpre ▸ step.sound
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp : [] * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp : [] * Production.lhs ↑step.prod * step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
simp [<- Word.eps_eq_nil, Word.mul_eq_cons] at tmp
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp :
  Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v] ∨
    ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
tmp :
  Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v] ∨
    ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
cases tmp
State after:
case inl
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε

case inr
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
case inl h =>
  have ⟨_, c⟩ := Production.lhs_contains_var step.prod.val
  have ⟨h, _⟩ := h
  rw [h] at c
  contradiction
State after:
no goals

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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
case inr h =>
  have ⟨_, ⟨h₁, h₂⟩ ⟩ := h
  have tmp := Word.mul_eq_eps.mp $ Eq.symm h₂
  have tmp' := tmp.1 ▸ h₁
  simp at tmp'
  constructor
  . assumption
  . constructor; rfl; exact tmp.right
State after:
no goals

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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have ⟨_, c⟩ := Production.lhs_contains_var step.prod.val
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have ⟨h, _⟩ := h
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
rw [h] at c
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ ε
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ ε
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
contradiction
State after:
no goals

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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have ⟨_, ⟨h₁, h₂⟩ ⟩ := h
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have tmp := Word.mul_eq_eps.mp $ Eq.symm h₂
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
have tmp' := tmp.1 ▸ h₁
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = Sum.inl v :: ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = Sum.inl v :: ε
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
simp at tmp'
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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
Tactic:
constructor
State after:
case 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v]

case right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε

State before:
case 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v]

case right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Tactic:
. assumption
State after:
case right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε

State before:
case right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Tactic:
. constructor; rfl; exact tmp.right
State after:
no goals

State before:
case 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v]
Tactic:
assumption
State after:
no goals

State before:
case right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε ∧ step.suf = ε
Tactic:
constructor
State after:
case right.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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε

case right.right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε

State before:
case right.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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ [] = ε

case right.right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε
Tactic:
rfl
State after:
case right.right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε

State before:
case right.right
α 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 })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : ∃ w', Production.lhs ↑step.prod = Sum.inl v :: w' ∧ ε = w' * step.suf
w✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h₁ : Production.lhs ↑step.prod = Sum.inl v :: w✝
h₂ : ε = w✝ * step.suf
tmp : w✝ = ε ∧ step.suf = ε
tmp' : Production.lhs ↑step.prod = [Sum.inl v]
⊢ step.suf = ε
Tactic:
exact tmp.right
State after:
no goals