cases nn with
| succ m =>
  apply Or.inl
  unfold Language.plus
  exists (Nat.succ m)
  exact ⟨Nat.succ_ne_zero m, r⟩
| zero =>
  apply Or.inr
  exact r
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
nn : ℕ
r : (fun n => w ∈ L ^ n) nn
⊢ w ∈ L⁺ ∪ {ε}
no goals