-- Mathlib/Computability/ContextFreeGrammar.lean
lemma Rewrites.exists_parts (hr : r.Rewrites u v) :
    ∃ p q : List (Symbol T N),
      u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q

Proof state:
case cons.intro.intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ ∃ p q,
    x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
      x :: (p' ++ r.output ++ q') = p ++ r.output ++ q

Tactic:
use x :: p', q'

Result:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
    x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'

Proof state:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
    x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'

Tactic:
simp

Result:
no goals

Proof state:
case cons
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
s₁✝ s₂✝ : List (Symbol T N)
hrs✝ : r.Rewrites s₁✝ s₂✝
ih : ∃ p q, s₁✝ = p ++ [Symbol.nonterminal r.input] ++ q ∧ s₂✝ = p ++ r.output ++ q
⊢ ∃ p q, x :: s₁✝ = p ++ [Symbol.nonterminal r.input] ++ q ∧ x :: s₂✝ = p ++ r.output ++ q

Tactic:
rcases ih with ⟨p', q', rfl, rfl⟩

Result:
case cons.intro.intro.intro
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs✝ : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ ∃ p q,
    x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
      x :: (p' ++ r.output ++ q') = p ++ r.output ++ q

Proof state:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ Symbol.nonterminal r.input :: s = [] ++ [Symbol.nonterminal r.input] ++ s ∧ r.output ++ s = [] ++ r.output ++ s

Tactic:
simp

Result:
no goals

Proof state:
case head
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ ∃ p q, Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q

Tactic:
use [], s

Result:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ Symbol.nonterminal r.input :: s = [] ++ [Symbol.nonterminal r.input] ++ s ∧ r.output ++ s = [] ++ r.output ++ s

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hr : r.Rewrites u v
⊢ ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q

Tactic:
induction hr with
| head s =>
  use [], s
  simp
| cons x _ ih =>
  rcases ih with ⟨p', q', rfl, rfl⟩
  use x :: p', q'
  simp

Result:
no goals