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
α 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 = ε
no goals