import Mathlib
import Langlib.Grammars.Unrestricted.Toolbox
import Langlib.Classes.RecursivelyEnumerable.Basics.Lifting
import Langlib.Classes.RecursivelyEnumerable.Definition
import Langlib.Classes.RecursivelyEnumerable.Closure.Concatenation
import Langlib.Utilities.ClosurePredicates
import Langlib.Utilities.ListUtils
import Langlib.Classes.RecursivelyEnumerable.Closure.Star.Helpers

/-! # RE Closure Under Kleene Star

This file proves that the class of recursively enumerable languages is closed under Kleene star.
The proof constructs an unrestricted grammar for `L*` given an unrestricted grammar for `L`,
following the construction from the Lean 3 proof `RE_star.lean`.

## Grammar Construction

Given a grammar `g` for `L` with nonterminals `N` and start symbol `S`:
- New nonterminals: `Z` (start), `H` (separator), `R` (scanner), plus lifted originals
- Rules:
  1. `Z → Z S H` (generate another copy)
  2. `Z → R H` (start terminal scanning)
  3. `R H → R` (scanner jumps over separator)
  4. `R H → ε` (scanner+separator deleted at end)
  5. All original rules (with nonterminals lifted)
  6. `R t → t R` for each terminal `t` (scanner moves left past terminals)

## Main declarations

- `RE_of_star_RE` — the main closure theorem
-/

variable {T : Type}

section construction

/-- New nonterminal type: original nonterminals ⊕ 3 fresh ones. -/
private abbrev nn (N : Type) : Type := N ⊕ Fin 3

/-- New symbol type. -/
private abbrev ns (T N : Type) : Type := symbol T (nn N)

private def Z {N : Type} : ns T N := symbol.nonterminal (Sum.inr 0)
private def H {N : Type} : ns T N := symbol.nonterminal (Sum.inr 1)
private def R {N : Type} : ns T N := symbol.nonterminal (Sum.inr 2)
private def S₀ {g : grammar T} : ns T g.nt := symbol.nonterminal (Sum.inl g.initial)

private def wrap_sym {N : Type} : symbol T N → ns T N
  | symbol.terminal t    => symbol.terminal t
  | symbol.nonterminal n => symbol.nonterminal (Sum.inl n)

private def wrap_gr {N : Type} (r : grule T N) : grule T (nn N) :=
  ⟨List.map wrap_sym r.input_L,
   Sum.inl r.input_N,
   List.map wrap_sym r.input_R,
   List.map wrap_sym r.output_string⟩

private def rules_that_scan_terminals (g : grammar T) : List (grule T (nn g.nt)) :=
  List.map (fun t => grule.mk [] (Sum.inr 2) [symbol.terminal t] [symbol.terminal t, R])
    (all_used_terminals g)

/-- The grammar for the Kleene star of a language generated by `g`. -/
private def star_grammar (g : grammar T) : grammar T :=
  ⟨nn g.nt, Sum.inr 0,
   grule.mk [] (Sum.inr 0) [] [Z, S₀, H] ::
   grule.mk [] (Sum.inr 0) [] [R, H] ::
   grule.mk [] (Sum.inr 2) [H] [R] ::
   grule.mk [] (Sum.inr 2) [H] [] ::
   List.map wrap_gr g.rules ++
   rules_that_scan_terminals g⟩

end construction

-- Utility: nonterminal not in map terminal
private lemma nonterminal_not_in_map_terminal {N : Type} {n : N} {w : List T} :
    symbol.nonterminal n ∉ List.map (symbol.terminal (N := N)) w := by
  intro h; rw [List.mem_map] at h; rcases h with ⟨_, _, h⟩; cases h

section easy_direction

private lemma wrap_sym_eq_lift_symbol {g : grammar T} :
    @wrap_sym T g.nt = lift_symbol_ Sum.inl := by
  ext x; cases x <;> rfl

private lemma wrap_gr_eq_lift_rule {g : grammar T} (r : grule T g.nt) :
    wrap_gr r = lift_rule_ Sum.inl r := by
  simp [wrap_gr, lift_rule_, lift_string_, ← wrap_sym_eq_lift_symbol]

/-- Wrapped rules of g are in star_grammar's rules. -/
private lemma wrapped_rule_mem {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) :
    wrap_gr r ∈ (star_grammar g).rules := by
  simp only [star_grammar]
  iterate 4 apply List.mem_cons_of_mem
  exact List.mem_append_left _ (List.mem_map_of_mem hr)

/-- Scanning rules are in star_grammar's rules. -/
private lemma scan_rule_mem {g : grammar T} {t : T} (ht : t ∈ all_used_terminals g) :
    grule.mk [] (Sum.inr 2) [symbol.terminal t] [symbol.terminal t, R] ∈ (star_grammar g).rules := by
  simp only [star_grammar]
  iterate 4 apply List.mem_cons_of_mem
  exact List.mem_append_right _ (List.mem_map_of_mem ht)

/-- The lifted grammar embedding g into star_grammar g. -/
private noncomputable def star_lg (g : grammar T) : lifted_grammar_ T := {
  g₀ := g
  g := star_grammar g
  lift_nt := Sum.inl
  sink_nt := Sum.getLeft?
  lift_inj := Sum.inl_injective
  sink_inj := by
    intro x y h
    match x, y with
    | Sum.inl a, Sum.inl b => left; simp [Sum.getLeft?] at h; exact congrArg Sum.inl h
    | Sum.inl _, Sum.inr _ => simp [Sum.getLeft?] at h
    | Sum.inr _, Sum.inl _ => simp [Sum.getLeft?] at h
    | Sum.inr _, Sum.inr _ => right; simp [Sum.getLeft?]
  lift_nt_sink := by intro n; simp [Sum.getLeft?]
  corresponding_rules := by
    intro r rin
    have := wrapped_rule_mem rin
    rw [wrap_gr_eq_lift_rule] at this
    exact this
  preimage_of_rules := by
    intro r ⟨rin, n₀, hn₀⟩
    have hinl : r.input_N = Sum.inl n₀ := hn₀.symm
    simp only [star_grammar] at rin
    rcases List.mem_cons.mp rin with rfl | rin
    · simp at hinl
    rcases List.mem_cons.mp rin with rfl | rin
    · simp at hinl
    rcases List.mem_cons.mp rin with rfl | rin
    · simp at hinl
    rcases List.mem_cons.mp rin with rfl | rin
    · simp at hinl
    rcases List.mem_append.mp rin with rin | rin
    · rw [List.mem_map] at rin
      rcases rin with ⟨r₀, hr₀, rfl⟩
      exact ⟨r₀, hr₀, by rw [wrap_gr_eq_lift_rule]⟩
    · simp only [rules_that_scan_terminals, List.mem_map] at rin
      rcases rin with ⟨t, _, rfl⟩; simp at hinl
}

/-- Lift a derivation from g to star_grammar g. -/
private lemma lift_generates {g : grammar T} {w : List T}
    (h : grammar_generates g w) :
  grammar_derives (star_grammar g) [S₀] (List.map symbol.terminal w) := by
  have lft := lift_deri_ (star_lg g) h
  simp only [lift_string_, List.map_cons, List.map_nil, lift_symbol_] at lft
  convert lft using 1
  simp [List.map_map, lift_symbol_]

/-- Terminal t from a derived word is in all_used_terminals. -/
private lemma terminal_in_all_used {g : grammar T} {w : List T}
    (hgen : grammar_generates g w) {t : T} (ht : t ∈ w) :
  t ∈ all_used_terminals g := by
  have stin : (symbol.terminal t : symbol T g.nt) ∈ List.map symbol.terminal w :=
    List.mem_map_of_mem (f := symbol.terminal) ht
  rcases grammar_generates_only_legit_terminals hgen stin with ⟨r, rin, htin⟩ | ⟨imposs⟩
  · simp only [all_used_terminals, List.mem_filterMap]
    exact ⟨symbol.terminal t,
      List.mem_flatten.mpr ⟨_, List.mem_map_of_mem (f := grule.output_string) rin, htin⟩,
      by simp [as_terminal]⟩
  · exact absurd imposs (by intro h; cases h)

/-
R scans left past a single word of terminals.
-/
private lemma scan_word {g : grammar T} {word : List T}
    (hw : ∀ t ∈ word, t ∈ all_used_terminals g)
    {sfx : List (ns T g.nt)} :
  grammar_derives (star_grammar g)
    ([R] ++ List.map symbol.terminal word ++ sfx)
    (List.map symbol.terminal word ++ [R] ++ sfx) := by
  have h_scan : ∀ (word : List T) (sfx : List (ns T g.nt)),
    (∀ t ∈ word, t ∈ all_used_terminals g) →
    grammar_derives (star_grammar g) ([R] ++ List.map symbol.terminal word ++ sfx) (List.map symbol.terminal word ++ [R] ++ sfx) := by
      intros word sfx hw
      induction' word with t word ih generalizing sfx;
      · exact?;
      · have h_scan : grammar_transforms (star_grammar g) ([R] ++ List.map symbol.terminal (t :: word) ++ sfx) ([symbol.terminal t] ++ [R] ++ List.map symbol.terminal word ++ sfx) := by
          use grule.mk [] (Sum.inr 2) [symbol.terminal t] [symbol.terminal t, R];
          simp +zetaDelta at *;
          exact ⟨ scan_rule_mem hw.1, [ ], List.map symbol.terminal word ++ sfx, rfl, rfl ⟩;
        have h_ind : grammar_derives (star_grammar g) ([symbol.terminal t] ++ [R] ++ List.map symbol.terminal word ++ sfx) ([symbol.terminal t] ++ List.map symbol.terminal word ++ [R] ++ sfx) := by
          convert grammar_deri_with_prefix [ symbol.terminal t ] ( ih sfx fun x hx => hw x ( List.mem_cons_of_mem _ hx ) ) using 1;
        exact grammar_deri_of_tran_deri h_scan h_ind;
  exact h_scan word sfx hw

/-
Terminal scan over multiple words separated by H's.
-/
private lemma terminal_scan {g : grammar T} {w : List (List T)}
    (hw : ∀ v ∈ w, ∀ t ∈ v, t ∈ all_used_terminals g) :
  grammar_derives (star_grammar g)
    ([R] ++ (List.map (fun v => [H] ++ List.map symbol.terminal v) w).flatten ++ [H])
    (List.map symbol.terminal w.flatten ++ [R, H]) := by
  revert w;
  intro w hw; induction' w with v w hw ih <;> simp_all +decide [ List.flatten ] ;
  · exact Relation.ReflTransGen.refl;
  · have h_scan : grammar_derives (star_grammar g) (R :: H :: (List.map symbol.terminal v ++ ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H]))) (R :: (List.map symbol.terminal v ++ ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H]))) := by
      have h_scan : grammar_transforms (star_grammar g) (R :: H :: (List.map symbol.terminal v ++ ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H]))) (R :: (List.map symbol.terminal v ++ ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H]))) := by
        unfold grammar_transforms; simp +decide [ star_grammar ] ;
        exact Or.inr <| Or.inr <| Or.inl ⟨ [ ], List.map symbol.terminal v ++ ( ( List.map ( fun v => H :: List.map symbol.terminal v ) w ).flatten ++ [ H ] ), rfl, rfl ⟩;
      exact Relation.ReflTransGen.single h_scan;
    have h_scan : grammar_derives (star_grammar g) (R :: (List.map symbol.terminal v ++ ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H]))) (List.map symbol.terminal v ++ R :: ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H])) := by
      convert scan_word _ using 1 ; aesop;
      exact hw.1;
    have h_scan : grammar_derives (star_grammar g) (List.map symbol.terminal v ++ R :: ((List.map (fun v => H :: List.map symbol.terminal v) w).flatten ++ [H])) (List.map symbol.terminal v ++ ((List.map (List.map symbol.terminal) w).flatten ++ [R, H])) := by
      apply grammar_deri_with_prefix; aesop;
    exact grammar_deri_of_deri_deri ‹_› ( grammar_deri_of_deri_deri ‹_› ‹_› )

/-
The short induction builds derivations for each word.
-/
private lemma short_induction {g : grammar T} {w : List (List T)}
    (ass : ∀ wᵢ ∈ w.reverse, grammar_generates g wᵢ) :
  grammar_derives (star_grammar g) [Z]
    (Z :: (List.map (· ++ [H]) (List.map (List.map symbol.terminal) w.reverse)).flatten) := by
  induction' w using List.reverseRecOn with w ih;
  · constructor;
  · rename_i h; specialize h ( fun wᵢ hwᵢ => ass wᵢ <| by simp +decide [ hwᵢ ] ) ; simp_all +decide [ List.map_append, List.flatten_append ] ;
    -- Apply the step_Z_expand rule to get [Z, S₀, H] ++ ih.
    have h_expand : grammar_derives (star_grammar g) [Z] ([Z, S₀, H] ++ (List.map ((fun x => x ++ [H]) ∘ List.map symbol.terminal) w).reverse.flatten) := by
      convert grammar_deri_of_deri_deri h ( grammar_deri_of_tran _ ) using 1;
      unfold grammar_transforms; simp +decide [ star_grammar ] ;
      exact Or.inl ⟨ [ ], _, rfl, rfl ⟩;
    have h_lift : grammar_derives (star_grammar g) [S₀, H] (List.map symbol.terminal ih ++ [H]) := by
      have h_lift : grammar_derives (star_grammar g) [S₀] (List.map symbol.terminal ih) := by
        exact lift_generates ass.1;
      apply grammar_deri_with_postfix [H] h_lift;
    convert grammar_deri_of_deri_deri h_expand _ using 1;
    convert grammar_deri_with_prefix [ Z ] ( grammar_deri_with_postfix ( ( List.map ( ( fun x => x ++ [ H ] ) ∘ List.map symbol.terminal ) w ).reverse.flatten ) h_lift ) using 1;
    simp +decide [ List.append_assoc ]

/-
The easy direction: L* ⊆ grammar_language (star_grammar g)
-/
private lemma in_star_grammar_of_in_star {g : grammar T} {w : List T}
    (hw : w ∈ KStar.kstar (grammar_language g)) :
  grammar_generates (star_grammar g) w := by
  obtain ⟨L, rfl, hL⟩ := hw;
  -- Set v = L.reverse. Then v.reverse = L.
  set v := L.reverse;
  -- Use short_induction to get: grammar_derives [Z] (Z :: (map (· ++ [H]) (map (map terminal) L)).flatten)
  have h1 : grammar_derives (star_grammar g) [Z] (Z :: (List.map (· ++ [H]) (List.map (List.map symbol.terminal) L)).flatten) := by
    convert short_induction _;
    exact?;
    aesop;
  -- Apply step_Z_to_RH (Z → R H) with postfix = rest of the string.
  have h2 : grammar_derives (star_grammar g) (Z :: (List.map (· ++ [H]) (List.map (List.map symbol.terminal) L)).flatten) ([R, H] ++ (List.map (· ++ [H]) (List.map (List.map symbol.terminal) L)).flatten) := by
    -- Apply the rule Z → R H to the initial symbol Z.
    have h_step : grammar_transforms (star_grammar g) [Z] [R, H] := by
      constructor;
      swap;
      exact grule.mk [] ( Sum.inr 0 ) [] [ R, H ];
      simp +decide [ star_grammar ];
      exists [ ], [ ];
    exact grammar_deri_of_tran_deri h_step ( grammar_deri_self ) |> fun h => by simpa using grammar_deri_with_postfix _ h;
  -- Apply terminal_scan to derive: [R] ++ (map (fun v => [H] ++ map terminal v) L).flatten ++ [H] →* map terminal L.flatten ++ [R, H]
  have h3 : grammar_derives (star_grammar g) ([R] ++ (List.map (fun v => [H] ++ List.map symbol.terminal v) L).flatten ++ [H]) (List.map symbol.terminal L.flatten ++ [R, H]) := by
    apply terminal_scan;
    exact?;
  -- Apply step_RH_delete (R H → ε) at the end.
  have h4 : grammar_derives (star_grammar g) (List.map symbol.terminal L.flatten ++ [R, H]) (List.map symbol.terminal L.flatten) := by
    apply grammar_deri_of_tran_deri;
    rotate_right;
    exact List.map symbol.terminal L.flatten;
    · constructor;
      swap;
      exact grule.mk [] ( Sum.inr 2 ) [ symbol.nonterminal ( Sum.inr 1 ) ] [ ];
      simp +decide [ star_grammar ];
      exact ⟨ Or.inl rfl, ( List.map ( List.map symbol.terminal ) L ).flatten, [ ], by simp +decide [ H, R ] ⟩;
    · exact?;
  -- Reorganize the separator structure:
  have h5 : grammar_derives (star_grammar g) ([R, H] ++ (List.map (· ++ [H]) (List.map (List.map symbol.terminal) L)).flatten) ([R] ++ (List.map (fun v => [H] ++ List.map symbol.terminal v) L).flatten ++ [H]) := by
    have h5 : grammar_derives (star_grammar g) ([R, H] ++ (List.map (· ++ [H]) (List.map (List.map symbol.terminal) L)).flatten) ([R] ++ [H] ++ (List.map (fun v => List.map symbol.terminal v ++ [H]) L).flatten) := by
      simp +decide [ List.map_map ];
      exact Relation.ReflTransGen.refl;
    convert h5 using 1;
    clear h1 h2 h3 h4 h5 hL v;
    induction L <;> aesop;
  exact grammar_deri_of_deri_deri ( grammar_deri_of_deri_deri ( grammar_deri_of_deri_deri h1 h2 ) h5 ) ( grammar_deri_of_deri_deri h3 h4 )

end easy_direction

section hard_direction

-- The star_induction invariant
private def StarInvariant (g : grammar T) (α : List (ns T g.nt)) : Prop :=
  (∃ x : List (List (symbol T g.nt)),
    (∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) ∧
    α = [Z] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) ∨
  (∃ x : List (List (symbol T g.nt)),
    (∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) ∧
    α = [R, H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) ∨
  (∃ w : List (List T), ∃ β : List T, ∃ γ : List (symbol T g.nt),
    ∃ x : List (List (symbol T g.nt)),
    (∀ wᵢ ∈ w, grammar_generates g wᵢ) ∧
    (grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ)) ∧
    (∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) ∧
    α = List.map symbol.terminal w.flatten ++
        List.map symbol.terminal β ++ [R] ++
        List.map wrap_sym γ ++ [H] ++
        (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) ∨
  (∃ u : List T, u ∈ KStar.kstar (grammar_language g) ∧
    α = List.map symbol.terminal u) ∨
  (∃ σ : List (symbol T g.nt), α = List.map wrap_sym σ ++ [R]) ∨
  ((∃ ω : List (ns T g.nt), α = ω ++ [H]) ∧ Z ∉ α ∧ R ∉ α)

/-
No grammar can transform a string of all terminals.
-/
private lemma no_transform_all_terminals {g' : grammar T} {u : List T} {α' : List (symbol T g'.nt)} :
    ¬ grammar_transforms g' (List.map symbol.terminal u) α' := by
  rintro ⟨ r, hr, u, v, hv ⟩;
  replace hv := congr_arg ( fun x => symbol.nonterminal r.input_N ∈ x ) hv.1 ; aesop

-- Helper: wrap_sym properties
private lemma wrap_sym_injective {N : Type} : Function.Injective (@wrap_sym T N) := by
  intro a b h; cases a <;> cases b <;> simp [wrap_sym] at h <;> exact congrArg _ h

private lemma wrap_sym_ne_Z {N : Type} (a : symbol T N) : wrap_sym a ≠ @Z T N := by
  cases a <;> simp [wrap_sym, Z]

private lemma wrap_sym_ne_H {N : Type} (a : symbol T N) : wrap_sym a ≠ @H T N := by
  cases a <;> simp [wrap_sym, H]

private lemma wrap_sym_ne_R {N : Type} (a : symbol T N) : wrap_sym a ≠ @R T N := by
  cases a <;> simp [wrap_sym, R]

private lemma Z_not_in_map_wrap {N : Type} {l : List (symbol T N)} :
    Z ∉ List.map wrap_sym l := by
  intro h; rw [List.mem_map] at h; rcases h with ⟨a, _, ha⟩; exact wrap_sym_ne_Z a ha

private lemma H_not_in_map_wrap {N : Type} {l : List (symbol T N)} :
    H ∉ List.map wrap_sym l := by
  intro h; rw [List.mem_map] at h; rcases h with ⟨a, _, ha⟩; exact wrap_sym_ne_H a ha

private lemma R_not_in_map_wrap {N : Type} {l : List (symbol T N)} :
    R ∉ List.map wrap_sym l := by
  intro h; rw [List.mem_map] at h; rcases h with ⟨a, _, ha⟩; exact wrap_sym_ne_R a ha

/-
The hard direction cases are very complex (see RE_star.lean Lean 3 proof, ~2000 lines).

Case 1: β = [Z] ++ (map (\cdot ++ [H]) (map (map wrap_sym) x)).flatten
-/
private lemma star_case_1 {g : grammar T} {α' : List (ns T g.nt)}
    {x : List (List (symbol T g.nt))}
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (h_step : grammar_transforms (star_grammar g)
      ([Z] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) α') :
  StarInvariant g α' := by
  revert h_step;
  unfold grammar_transforms;
  simp +decide [ star_grammar ];
  rintro ( ⟨ u, v, huv, rfl ⟩ | ⟨ u, v, huv, rfl ⟩ | ⟨ u, v, huv, rfl ⟩ | ⟨ u, v, huv, rfl ⟩ | ⟨ a, ha, u, v, huv, rfl ⟩ );
  · rcases u with ( _ | ⟨ a, u ⟩ ) <;> simp_all +decide [ Z ];
    · refine' Or.inl ⟨ _, _, _ ⟩;
      exact [ [ symbol.nonterminal g.initial ] ] ++ x;
      · grind +suggestions;
      · aesop;
    · have h_contradiction : symbol.nonterminal (Sum.inr 0) ∉ (List.map (fun x => x ++ [H]) (List.map (List.map wrap_sym) x)).flatten := by
        convert Z_not_in_blocks using 1;
      aesop;
  · rcases u with ( _ | ⟨ a, u ⟩ ) <;> simp_all +decide [ Z ];
    · exact Or.inr <| Or.inl ⟨ x, hx, by aesop ⟩;
    · have h_contradiction : symbol.nonterminal (Sum.inr 0) ∈ (List.map ((fun x => x ++ [H]) ∘ List.map wrap_sym) x).flatten := by
        aesop;
      exact absurd h_contradiction ( by simpa using Z_not_in_blocks );
  · rcases u with ( _ | ⟨ a, u ⟩ ) <;> simp_all +decide [ Z ];
    have h_contra : symbol.nonterminal (Sum.inr 2) ∈ (List.map ((fun x => x ++ [H]) ∘ List.map wrap_sym) x).flatten := by
      aesop;
    exact absurd h_contra ( by simpa using R_not_in_blocks );
  · rcases u with ( _ | ⟨ a, u ⟩ ) <;> simp_all +decide [ Z ];
    have h_contradiction : symbol.nonterminal (Sum.inr 2) ∈ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten := by
      aesop;
    exact absurd h_contradiction ( by simpa using R_not_in_blocks );
  · rcases ha with ( ⟨ r, hr, rfl ⟩ | ha );
    · rcases u with ( _ | ⟨ u, u ⟩ ) <;> simp_all +decide [ wrap_gr ];
      · replace huv := congr_arg List.head? huv ; simp_all +decide [ Z ];
        cases h : r.input_L.head? <;> simp_all +decide [ wrap_sym ];
        cases ‹symbol T g.nt› <;> cases huv;
      · -- Apply the match_in_block lemma to find the block in x that contains the nonterminal.
        obtain ⟨x₁, xₘ, x₂, u₁, v₁, hx₁, hx₂, hu₁, hv₁⟩ : ∃ x₁ xₘ x₂ u₁ v₁, x = x₁ ++ [xₘ] ++ x₂ ∧ xₘ = u₁ ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v₁ ∧ u = (List.map (· ++ [H]) (List.map (List.map wrap_sym) x₁)).flatten ++ List.map wrap_sym u₁ ∧ v = List.map wrap_sym v₁ ++ [H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x₂)).flatten := by
          apply match_in_block;
          · rintro rfl; simp_all +decide [ List.flatten ];
          · aesop;
        -- Apply the valid_update_block lemma to show that the new block is valid.
        have h_valid_update : ∀ xᵢ ∈ x₁ ++ [u₁ ++ r.output_string ++ v₁] ++ x₂, grammar_derives g [symbol.nonterminal g.initial] xᵢ := by
          apply valid_update_block;
          · grind;
          · assumption;
        exact Or.inl ⟨ x₁ ++ [ u₁ ++ r.output_string ++ v₁ ] ++ x₂, h_valid_update, by aesop ⟩;
    · unfold rules_that_scan_terminals at ha; simp_all +decide [ List.mem_map ] ;
      rcases ha with ⟨ t, ht, rfl ⟩;
      rcases u with ( _ | ⟨ u, u ⟩ ) <;> simp_all +decide [ Z ];
      have h_contradiction : symbol.nonterminal (Sum.inr 2) ∉ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten := by
        convert R_not_in_blocks using 1;
      aesop

/-
The blocks structure ends with [H] when x ≠ [].
-/
private lemma blocks_end_with_H {N : Type} {x : List (List (symbol T N))} (hne : x ≠ []) :
    ∃ ω : List (ns T N), (List.map (· ++ [@H T N]) (List.map (List.map wrap_sym) x)).flatten = ω ++ [H] := by
  induction' x using List.reverseRecOn with x xs ih <;> simp_all +decide [ List.map ];
  by_cases hx : x = [] <;> simp_all +decide [ Function.comp ];
  exact ⟨ _, by rw [ ih.choose_spec, ← List.append_assoc ] ⟩

/-
R uniqueness: if R only appears at position 0 in R :: tail, and
    R :: tail = u ++ [R] ++ rest, then u = [].
-/
private lemma R_at_head_means_u_nil {g : grammar T}
    {x : List (List (symbol T g.nt))}
    {u rest : List (ns T g.nt)}
    (hbef : R :: H :: (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
      u ++ [R] ++ rest) :
  u = [] := by
  -- Apply the lemma head_unique_elem with the given hypotheses.
  have := head_unique_elem (by
  rfl : R :: H :: (List.map (· ++ [@H T g.nt]) (List.map (List.map wrap_sym) x)).flatten = @R T g.nt :: (R :: H :: (List.map (· ++ [@H T g.nt]) (List.map (List.map wrap_sym) x)).flatten).tail) (by
  convert R_only_at_head using 1 : @R T g.nt ∉ (R :: H :: (List.map (· ++ [@H T g.nt]) (List.map (List.map wrap_sym) x)).flatten).tail) hbef; aesop

/-
Case 2 wrapped rule sub-case
-/
private lemma star_case_2_wrapped {g : grammar T}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt}
    {u v : List (ns T g.nt)}
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (hr₀ : r₀ ∈ g.rules)
    (hbef : [R, H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
      u ++ List.map wrap_sym r₀.input_L ++
        [symbol.nonterminal (Sum.inl r₀.input_N)] ++
        List.map wrap_sym r₀.input_R ++ v) :
  StarInvariant g (u ++ List.map wrap_sym r₀.output_string ++ v) := by
  rcases u with ( _ | ⟨ u, _ | ⟨ u, u ⟩ ⟩ ) <;> simp_all +decide [ List.map ];
  · replace hbef := congr_arg List.head? hbef ; simp_all +decide;
    cases h : r₀.input_L <;> simp_all +decide [ R ];
    cases ‹symbol T g.nt› <;> cases hbef;
  · rcases hbef with ⟨ rfl, hbef ⟩;
    cases h : r₀.input_L <;> simp_all +decide [ Function.comp ];
    · cases hbef.1;
    · cases ‹symbol T g.nt› <;> cases hbef.1;
  · rcases hbef with ⟨ rfl, rfl, h ⟩;
    have := @match_in_block;
    specialize @this T g.nt r₀ x u v ; simp_all +decide [ List.map ];
    by_cases hx : x = [] <;> simp_all +decide [ List.map ];
    obtain ⟨ x₁, x₂, u₁, v₁, rfl, rfl, rfl ⟩ := this h; ( have := @valid_update_block; simp_all +decide [ List.map ] ; );
    refine' Or.inr <| Or.inl ⟨ x₁ ++ [ u₁ ++ ( r₀.output_string ++ v₁ ) ] ++ x₂, _, _ ⟩ <;> simp_all +decide [ List.map ];
    · exact this hx hr₀;
    · congr! 2

/-- Z is not in [R, H] ++ blocks(x) -/
private lemma Z_not_in_case2_string {g : grammar T}
    {x : List (List (symbol T g.nt))} :
    Z ∉ ([R, H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten : List (ns T g.nt)) := by
  simp [List.mem_append, R, H, Z]
  intro a _ b _; cases b <;> simp [wrap_sym]

/-- R only appears at position 0 in [R, H] ++ blocks(x) -/
private lemma R_unique_in_case2 {g : grammar T}
    {x : List (List (symbol T g.nt))}
    {u rest : List (ns T g.nt)}
    (h : ([R, H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten : List (ns T g.nt)) =
      u ++ [symbol.nonterminal (Sum.inr 2)] ++ rest) :
    u = [] := by
  have := R_at_head_means_u_nil (show R :: H :: _ = u ++ [R] ++ rest from by
    simp [List.append_assoc] at h ⊢; exact h)
  exact this

/-- No rule of star_grammar has input_N = Sum.inr 1 (H) -/
private lemma no_H_rule {g : grammar T} {r : grule T (nn g.nt)}
    (hr : r ∈ (star_grammar g).rules) (hi : r.input_N = Sum.inr 1) : False := by
  simp [star_grammar] at hr
  rcases hr with rfl | rfl | rfl | rfl | ⟨a, ha, rfl⟩ | hr <;>
    simp_all +decide [wrap_gr, rules_that_scan_terminals, List.mem_map]
  rcases hr with ⟨t, ht, rfl⟩; simp at hi

/-- Extract wrapped rule from star_grammar rule that is not Sum.inr -/
private lemma extract_wrapped_rule {g : grammar T} {r : grule T (nn g.nt)}
    (hr : r ∈ (star_grammar g).rules)
    (hinr : ∀ i : Fin 3, r.input_N ≠ Sum.inr i) :
    ∃ r₀ ∈ g.rules, r = wrap_gr r₀ := by
  simp [star_grammar] at hr
  rcases hr with rfl | rfl | rfl | rfl | ⟨r₀, hr₀, rfl⟩ | hr
  · exact absurd rfl (hinr 0)
  · exact absurd rfl (hinr 0)
  · exact absurd rfl (hinr 2)
  · exact absurd rfl (hinr 2)
  · exact ⟨r₀, hr₀, rfl⟩
  · simp [rules_that_scan_terminals, List.mem_map] at hr
    rcases hr with ⟨t, ht, rfl⟩
    exact absurd rfl (hinr 2)

/-
Sub-case: R·H→R in case 2. hbef simplifies to v = blocks(x).
-/
private lemma star_case_2_RH_to_R {g : grammar T}
    {x : List (List (symbol T g.nt))}
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) :
    StarInvariant g ([R] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  rcases x with ( _ | ⟨ y, _ | ⟨ z, x ⟩ ⟩ ) <;> simp_all +decide [ StarInvariant ];
  · refine Or.inr <| Or.inr <| Or.inl ⟨ [ ], ?_, [ ], y, ?_, [ ], ?_, rfl ⟩ <;> aesop;
  · refine Or.inr <| Or.inr <| Or.inl <| ?_;
    use [];
    refine' ⟨ by tauto, [ ], y, _, x.cons z, _, _ ⟩ <;> aesop

/-
Sub-case: R·H→ε in case 2. Result is blocks(x).
-/
private lemma star_case_2_RH_to_eps {g : grammar T}
    {x : List (List (symbol T g.nt))}
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) :
    StarInvariant g ((List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  by_cases hx_empty : x = [];
  · exact Or.inr <| Or.inr <| Or.inr <| Or.inl ⟨ [ ],Language.nil_mem_kstar _, by simp +decide [ hx_empty ] ⟩;
  · obtain ⟨ω, hω⟩ := blocks_end_with_H hx_empty;
    refine' Or.inr ( Or.inr ( Or.inr ( Or.inr ( Or.inr ⟨ ⟨ ω, by aesop ⟩, _, _ ⟩ ) ) ) ) <;> simp_all +decide [ List.map_append, List.map_map ];
    · refine' ⟨ _, _ ⟩;
      · intro hZω
        have hZω' : Z ∈ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten := by
          grind
        exact Z_not_in_blocks hZω';
      · rintro ⟨ ⟩;
    · have hR_not_in_blocks : R ∉ (List.map (· ++ [@H T g.nt]) (List.map (List.map wrap_sym) x)).flatten := by
        convert R_not_in_blocks using 1;
      aesop

/-
Case 2: β = [R, H] ++ blocks(x)
-/
private lemma star_case_2 {g : grammar T} {α' : List (ns T g.nt)}
    {x : List (List (symbol T g.nt))}
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (h_step : grammar_transforms (star_grammar g)
      ([R, H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) α') :
  StarInvariant g α' := by
  obtain ⟨ r, hr, u, v, hbef, _, rfl ⟩ := h_step;
  by_cases h : ∃ i : Fin 3, r.input_N = Sum.inr i;
  · rcases h with ⟨ i, hi ⟩ ; fin_cases i <;> simp_all +decide [ star_grammar ] ;
    · have h_contradiction : Z ∈ [R, H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten := by
        grind +locals;
      exact absurd h_contradiction ( by simpa using Z_not_in_case2_string );
    · grind +locals;
    · -- Since $u ++ r.input_L = []$, we have $u = []$ and $r.input_L = []$.
      have hu_empty : u = [] := by
        apply R_at_head_means_u_nil;
        rotate_left;
        exact x;
        exact r.input_R ++ v;
        rcases hr with ( rfl | rfl | rfl | rfl | ⟨ a, ha, rfl ⟩ | hr ) <;> simp_all +decide [ Function.comp ];
        · rfl;
        · rfl;
        · cases hi;
        · unfold rules_that_scan_terminals at hr; aesop;
      have hr_input_L_empty : r.input_L = [] := by
        grind +locals;
      -- Since $r.input_R = [H]$, we have $v = (List.map ((fun x => x ++ [H]) ∘ List.map wrap_sym) x).flatten$.
      have hv_eq : v = (List.map ((fun x => x ++ [H]) ∘ List.map wrap_sym) x).flatten := by
        grind +locals;
      rcases hr with ( rfl | rfl | rfl | rfl | ⟨ a, ha, rfl ⟩ | hr ) <;> simp_all +decide [ star_grammar ];
      · convert star_case_2_RH_to_R hx using 1;
        aesop;
      · convert star_case_2_RH_to_eps hx using 1;
        rw [ List.map_map ];
      · unfold wrap_gr at hi; aesop;
      · unfold rules_that_scan_terminals at hr; simp_all +decide [ List.mem_map ] ;
        rcases hr with ⟨ a, ha, rfl ⟩ ; simp_all +decide [ StarInvariant ] ;
        cases hbef.2;
  · obtain ⟨ r₀, hr₀, rfl ⟩ := extract_wrapped_rule hr ( by simpa using h ) ; exact star_case_2_wrapped hx hr₀ hbef;

/-
Z is not in case 3 string
-/
private lemma Z_not_in_case3_string {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))} :
    Z ∉ (List.map symbol.terminal w.flatten ++
         List.map symbol.terminal β ++ [R] ++
         List.map wrap_sym γ ++ [H] ++
         (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten :
         List (ns T g.nt)) := by
  unfold Z; simp +decide [ List.mem_append ] ;
  unfold R H; simp +decide ;
  exact ⟨ fun _ _ => wrap_sym_ne_Z _, fun _ _ _ _ => wrap_sym_ne_Z _ ⟩

/-
R is unique in case 3 string
-/
private lemma R_unique_in_case3 {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {u rest : List (ns T g.nt)}
    (h : List.map symbol.terminal w.flatten ++
         List.map symbol.terminal β ++ [R] ++
         List.map wrap_sym γ ++ [H] ++
         (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
       u ++ [R] ++ rest) :
    u = List.map symbol.terminal (w.flatten ++ β) := by
  have h_u : ∀ {l₁ l₂ l₃ : List (ns T g.nt)}, l₁ ++ [R] ++ l₂ = l₃ ++ [R] ++ rest → R ∉ l₁ → R ∉ l₂ → l₁ = l₃ := by
    intros l₁ l₂ l₃ h_eq h₁ h₂; induction' l₁ with l₁_head l₁_tail l₁_ih generalizing l₃ <;> induction' l₃ with l₃_head l₃_tail l₃_ih <;> simp_all +decide [ List.append_assoc ] ;
  contrapose! h_u;
  refine' ⟨ ( List.map ( List.map symbol.terminal ) w ).flatten ++ List.map symbol.terminal β, List.map wrap_sym γ ++ H :: ( List.map ( ( fun x => x ++ [ H ] ) ∘ List.map wrap_sym ) x ).flatten, u, _, _, _, _ ⟩ <;> simp_all +decide [ List.append_assoc ];
  · exact ⟨ fun x hx y hy => ne_of_apply_ne ( fun z => z ) ( by simp +decide [ R ] ), fun x hx => ne_of_apply_ne ( fun z => z ) ( by simp +decide [ R ] ) ⟩;
  · exact ⟨ fun x hx => by intro H; have := wrap_sym_ne_R x; aesop, by rintro ⟨ ⟩, fun x hx => ⟨ fun y hy => by intro H; have := wrap_sym_ne_R y; aesop, by rintro ⟨ ⟩ ⟩ ⟩;
  · grind +ring

/-
Wrapped match in γ: decompose γ and update derivation
-/
private lemma star_case_3_wrapped_in_gamma {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt}
    {γ_L γ_R : List (symbol T g.nt)}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (hr₀ : r₀ ∈ g.rules)
    (hγ_eq : γ = γ_L ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++
              r₀.input_R ++ γ_R) :
    StarInvariant g
      (List.map symbol.terminal w.flatten ++
       List.map symbol.terminal β ++ [R] ++
       List.map wrap_sym (γ_L ++ r₀.output_string ++ γ_R) ++ [H] ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  refine Or.inr <| Or.inr <| Or.inl ⟨ w, β, γ_L ++ r₀.output_string ++ γ_R, x, hw, ?_, hx, ?_ ⟩;
  · convert grammar_deri_of_deri_tran hβγ _ using 1;
    exact ⟨ r₀, hr₀, List.map symbol.terminal β ++ γ_L, γ_R, by aesop ⟩;
  · rfl

/-
Wrapped match in blocks: update block
-/
private lemma star_case_3_wrapped_in_blocks {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt}
    {x₁ : List (List (symbol T g.nt))} {xₘ : List (symbol T g.nt)}
    {x₂ : List (List (symbol T g.nt))}
    {u₁ v₁ : List (symbol T g.nt)}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (hr₀ : r₀ ∈ g.rules)
    (hx_eq : x = x₁ ++ [xₘ] ++ x₂)
    (hxₘ_eq : xₘ = u₁ ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++
              r₀.input_R ++ v₁) :
    StarInvariant g
      (List.map symbol.terminal w.flatten ++
       List.map symbol.terminal β ++ [R] ++
       List.map wrap_sym γ ++ [H] ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym)
         (x₁ ++ [u₁ ++ r₀.output_string ++ v₁] ++ x₂))).flatten) := by
  -- Apply the valid_update_block lemma to conclude the proof.
  have h_valid_update : ∀ xᵢ ∈ x₁ ++ [u₁ ++ r₀.output_string ++ v₁] ++ x₂, grammar_derives g [symbol.nonterminal g.initial] xᵢ := by
    apply_rules [ valid_update_block ];
    aesop;
  apply Or.inr;
  refine Or.inr <| Or.inl ⟨ w, β, γ, x₁ ++ [ u₁ ++ r₀.output_string ++ v₁ ] ++ x₂, hw, hβγ, h_valid_update, ?_ ⟩;
  rfl

/-
R is not in the wrapped rule input pattern.
-/
private lemma R_not_in_wrapped_input_local {g : grammar T} {r₀ : grule T g.nt} :
    R ∉ List.map wrap_sym r₀.input_L ++
      [symbol.nonterminal (Sum.inl r₀.input_N)] ++
      List.map wrap_sym r₀.input_R := by
  simp +decide [ R, wrap_sym ];
  constructor <;> intro x hx <;> cases x <;> simp +decide [ * ] at hx ⊢

/-
R is not in wrap(γ) ++ [H] ++ blocks(x)
-/
private lemma R_not_in_gamma_H_blocks {g : grammar T}
    {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))} :
    R ∉ (List.map wrap_sym γ ++ [H] ++
        (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten :
        List (ns T g.nt)) := by
  unfold R H wrap_sym; aesop;

/-- The nonterminal Sum.inl n can only appear in wrap(γ) or blocks, not in terminals or [R].
    So u must contain the terminal prefix and [R]. -/
private lemma case3_wrapped_strip_prefix {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt} {u v : List (ns T g.nt)}
    (hbef : List.map symbol.terminal w.flatten ++
            List.map symbol.terminal β ++ [R] ++
            List.map wrap_sym γ ++ [H] ++
            (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
          u ++ List.map wrap_sym r₀.input_L ++
            [symbol.nonterminal (Sum.inl r₀.input_N)] ++
            List.map wrap_sym r₀.input_R ++ v) :
    ∃ u' : List (ns T g.nt),
      u = List.map symbol.terminal (w.flatten ++ β) ++ [R] ++ u' ∧
      List.map wrap_sym γ ++ [H] ++
        (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
        u' ++ List.map wrap_sym r₀.input_L ++
          [symbol.nonterminal (Sum.inl r₀.input_N)] ++
          List.map wrap_sym r₀.input_R ++ v := by
  -- R appears once on the LHS at the boundary between terminals and wrap(γ).
  -- The wrapped rule pattern doesn't contain R.
  -- So using split_at_H with separator=R, the match must be after R.
  have h_R_not_in_mid : R ∉ (List.map wrap_sym r₀.input_L ++
      [symbol.nonterminal (Sum.inl r₀.input_N)] ++
      List.map wrap_sym r₀.input_R) := R_not_in_wrapped_input_local
  have hbef' : List.map symbol.terminal (w.flatten ++ β) ++ [R] ++
      (List.map wrap_sym γ ++ [H] ++
        (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) =
      u ++ (List.map wrap_sym r₀.input_L ++
        [symbol.nonterminal (Sum.inl r₀.input_N)] ++
        List.map wrap_sym r₀.input_R) ++ v := by
    simp only [List.append_assoc, List.map_append] at hbef ⊢; exact hbef
  rcases split_at_separator h_R_not_in_mid hbef' with ⟨u₁, h_a, h_v₁⟩ | ⟨v₁, h_u₁, h_b₁⟩
  · -- Case: match is in terminals. But terminals can't contain nonterminals.
    exfalso
    have : symbol.nonterminal (Sum.inl r₀.input_N) ∈
        List.map (symbol.terminal (N := nn g.nt)) (w.flatten ++ β) := by
      rw [h_a]; simp [List.mem_append]
    exact nonterminal_not_in_map_terminal this
  · -- Case: match is after R. Then u = terminals ++ [R] ++ v₁.
    exact ⟨v₁, h_u₁, by simp only [List.append_assoc] at h_b₁ ⊢; exact h_b₁⟩

/-
H is not in the wrapped rule input pattern (local version).
-/
private lemma H_not_in_wrapped_input_local {g : grammar T} {r₀ : grule T g.nt} :
    H ∉ List.map wrap_sym r₀.input_L ++
      [symbol.nonterminal (Sum.inl r₀.input_N)] ++
      List.map wrap_sym r₀.input_R := by
  simp +decide [ H, wrap_sym ];
  constructor <;> intros x hx <;> cases x <;> simp +decide [ Sum.inl.injEq, Sum.inr.injEq ] at hx ⊢

/-
Local version of split_at_separator for H
-/
private lemma split_at_H {g : grammar T}
    {a b u v : List (ns T g.nt)}
    {mid : List (ns T g.nt)}
    (h_H_not_in_mid : H ∉ mid)
    (h_eq : a ++ [H] ++ b = u ++ mid ++ v) :
  (∃ u' : List (ns T g.nt), a = u ++ mid ++ u' ∧ v = u' ++ [H] ++ b) ∨
  (∃ v' : List (ns T g.nt), u = a ++ [H] ++ v' ∧ b = v' ++ mid ++ v) := by
  by_cases hu : u.length ≤ a.length <;> simp_all +decide [ List.append_eq_append_iff ];
  · rcases h_eq with ( ⟨ as, rfl, h ⟩ | ⟨ bs, rfl, h ⟩ ) <;> simp_all +decide [ List.append_assoc ];
    · cases mid <;> aesop;
    · rcases h with ( ⟨ as, rfl, rfl ⟩ | ⟨ bs', rfl, h ⟩ ) <;> simp_all +decide [ List.append_assoc ];
      cases bs' <;> aesop;
  · rcases h_eq with ( ⟨ as, rfl, h ⟩ | ⟨ bs, rfl, h ⟩ ) <;> simp_all +decide [ List.length_append ];
    cases as <;> aesop

/-
Case 3 wrapped: match in γ
-/
private lemma case3_wrapped_gamma {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt}
    {u' u'' : List (ns T g.nt)}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (hr₀ : r₀ ∈ g.rules)
    (h_gamma : List.map wrap_sym γ =
      u' ++ List.map wrap_sym r₀.input_L ++
        [symbol.nonterminal (Sum.inl r₀.input_N)] ++
        List.map wrap_sym r₀.input_R ++ u'') :
    StarInvariant g
      (List.map symbol.terminal (w.flatten ++ β) ++ [R] ++
       u' ++ List.map wrap_sym r₀.output_string ++ u'' ++ [H] ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  -- Let's verify that $u'$ and $u''$ are in the range of $wrap_sym$.
  have hu'_in_range : ∃ γ_L : List (symbol T g.nt), u' = List.map wrap_sym γ_L := by
    have hu'_in_range : ∀ u' : List (ns T g.nt), (∀ u'ᵢ ∈ u', u'ᵢ ∈ List.map wrap_sym γ) → ∃ γ_L : List (symbol T g.nt), u' = List.map wrap_sym γ_L := by
      intros u' hu'
      induction' u' with u' ih;
      · exact ⟨ [ ], rfl ⟩;
      · simp +zetaDelta at *;
        rcases hu' with ⟨ ⟨ a, ha, rfl ⟩, hu' ⟩ ; rcases ‹ ( ∀ u'ᵢ ∈ ih, ∃ a ∈ γ, wrap_sym a = u'ᵢ ) → ∃ γ_L, ih = List.map wrap_sym γ_L › hu' with ⟨ γ_L, rfl ⟩ ; exact ⟨ a :: γ_L, by simp +decide ⟩ ;
    exact hu'_in_range u' fun u'ᵢ hu'ᵢ => h_gamma.symm ▸ List.mem_append_left _ ( List.mem_append_left _ ( List.mem_append_left _ ( List.mem_append_left _ hu'ᵢ ) ) )
  have hu''_in_range : ∃ γ_R : List (symbol T g.nt), u'' = List.map wrap_sym γ_R := by
    have hu''_in_range : ∀ a ∈ u'', ∃ b : symbol T g.nt, a = wrap_sym b := by
      intro a ha
      have ha_gamma : a ∈ List.map wrap_sym γ := by
        grind;
      rw [ List.mem_map ] at ha_gamma; obtain ⟨ b, hb, rfl ⟩ := ha_gamma; exact ⟨ b, rfl ⟩ ;
    have hu''_in_range : ∀ {l : List (ns T g.nt)}, (∀ a ∈ l, ∃ b : symbol T g.nt, a = wrap_sym b) → ∃ γ_R : List (symbol T g.nt), l = List.map wrap_sym γ_R := by
      intros l hl; induction' l with a l ih <;> simp_all +decide [ List.map ] ;
      rcases hl.1 with ⟨ b, rfl ⟩ ; rcases ih with ⟨ γ_R, rfl ⟩ ; exact ⟨ b :: γ_R, by simp +decide ⟩ ;
    exact hu''_in_range ‹_›;
  obtain ⟨ γ_L, rfl ⟩ := hu'_in_range; obtain ⟨ γ_R, rfl ⟩ := hu''_in_range;
  -- Let's verify that γ = γ_L ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R ++ γ_R.
  have h_gamma_eq : γ = γ_L ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R ++ γ_R := by
    have h_gamma_eq : List.map wrap_sym γ = List.map wrap_sym (γ_L ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R ++ γ_R) := by
      aesop;
    exact List.map_injective_iff.mpr ( wrap_sym_injective ) h_gamma_eq;
  convert star_case_3_wrapped_in_gamma hw hβγ hx hr₀ h_gamma_eq using 1;
  simp +decide [ List.map_append ]

/-
Case 3 wrapped: match in blocks
-/
private lemma case3_wrapped_blocks {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt}
    {v' v : List (ns T g.nt)}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (hr₀ : r₀ ∈ g.rules)
    (h_blocks : (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
      v' ++ List.map wrap_sym r₀.input_L ++
        [symbol.nonterminal (Sum.inl r₀.input_N)] ++
        List.map wrap_sym r₀.input_R ++ v) :
    StarInvariant g
      (List.map symbol.terminal (w.flatten ++ β) ++ [R] ++
       List.map wrap_sym γ ++ [H] ++
       v' ++ List.map wrap_sym r₀.output_string ++ v) := by
  by_contra h_contra;
  obtain ⟨x₁, xₘ, x₂, u₁, v₁, hx_eq, hxₘ_eq⟩ : ∃ x₁ : List (List (symbol T g.nt)), ∃ xₘ : List (symbol T g.nt), ∃ x₂ : List (List (symbol T g.nt)), ∃ u₁ : List (symbol T g.nt), ∃ v₁ : List (symbol T g.nt), x = x₁ ++ [xₘ] ++ x₂ ∧ xₘ = u₁ ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R ++ v₁ ∧ v' = (List.map (· ++ [H]) (List.map (List.map wrap_sym) x₁)).flatten ++ List.map wrap_sym u₁ ∧ v = List.map wrap_sym v₁ ++ [H] ++ (List.map (· ++ [H]) (List.map (List.map wrap_sym) x₂)).flatten := by
    have := @match_in_block T g.nt r₀ x v' v;
    by_cases hx' : x = [] <;> simp_all +decide;
    convert this _;
    convert h_blocks using 1;
  refine' h_contra _;
  convert star_case_3_wrapped_in_blocks hw hβγ ( fun xᵢ hxᵢ => hx xᵢ ( by aesop ) ) hr₀ hx_eq hxₘ_eq.1 using 1;
  simp +decide [ hxₘ_eq, List.flatten ]

/-- Case 3 wrapped rule sub-case -/
private lemma star_case_3_wrapped {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {r₀ : grule T g.nt} {u v : List (ns T g.nt)}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (hr₀ : r₀ ∈ g.rules)
    (hbef : List.map symbol.terminal w.flatten ++
            List.map symbol.terminal β ++ [R] ++
            List.map wrap_sym γ ++ [H] ++
            (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
          u ++ List.map wrap_sym r₀.input_L ++
            [symbol.nonterminal (Sum.inl r₀.input_N)] ++
            List.map wrap_sym r₀.input_R ++ v) :
    StarInvariant g (u ++ List.map wrap_sym r₀.output_string ++ v) := by
  obtain ⟨u', hu_eq, h_suffix⟩ := case3_wrapped_strip_prefix hbef
  rw [hu_eq]
  have h_suffix' : List.map wrap_sym γ ++ [H] ++
      (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
      u' ++ (List.map wrap_sym r₀.input_L ++
        [symbol.nonterminal (Sum.inl r₀.input_N)] ++
        List.map wrap_sym r₀.input_R) ++ v := by
    simp only [List.append_assoc] at h_suffix ⊢; exact h_suffix
  rcases split_at_H H_not_in_wrapped_input_local h_suffix' with ⟨u'', h_gamma, h_v⟩ | ⟨v', h_u', h_blocks⟩
  · rw [h_v]
    have h_gamma' : List.map wrap_sym γ =
        u' ++ List.map wrap_sym r₀.input_L ++
          [symbol.nonterminal (Sum.inl r₀.input_N)] ++
          List.map wrap_sym r₀.input_R ++ u'' := by
      simp only [List.append_assoc] at h_gamma ⊢; exact h_gamma
    convert case3_wrapped_gamma hw hβγ hx hr₀ h_gamma' using 1
    simp [List.append_assoc]
  · rw [h_u']
    have h_blocks' : (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten =
        v' ++ List.map wrap_sym r₀.input_L ++
          [symbol.nonterminal (Sum.inl r₀.input_N)] ++
          List.map wrap_sym r₀.input_R ++ v := by
      simp only [List.append_assoc] at h_blocks ⊢; exact h_blocks
    convert case3_wrapped_blocks hw hβγ hx hr₀ h_blocks' using 1
    simp [List.append_assoc]

/-
Case 3 sub-case: R·H → R with γ = []
-/
private lemma star_case_3_RH_to_R {g : grammar T}
    {w : List (List T)} {β : List T}
    {x : List (List (symbol T g.nt))}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβ : grammar_generates g β)
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) :
    StarInvariant g
      (List.map symbol.terminal (w.flatten ++ β) ++ [R] ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  by_cases hx_empty : x = [];
  · -- Since x is empty, the result string simplifies to terminals(w.flatten ++ β) ++ [R], which is case 5.
    use Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨List.map symbol.terminal (w.flatten ++ β), by
      unfold wrap_sym; aesop;⟩))) );
  · -- Since x is not empty, we can take y as the first element of x.
    obtain ⟨y, rest, hx_eq⟩ : ∃ y rest, x = y :: rest := by
      exact List.exists_cons_of_ne_nil hx_empty;
    apply Or.inr; apply Or.inr; apply Or.inl; use w ++ [β], [], y, rest; aesop;

/-
Case 3 sub-case: R·H → ε with γ = []
-/
private lemma star_case_3_RH_to_eps {g : grammar T}
    {w : List (List T)} {β : List T}
    {x : List (List (symbol T g.nt))}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβ : grammar_generates g β)
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) :
    StarInvariant g
      (List.map symbol.terminal (w.flatten ++ β) ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  by_cases hx_empty : x = [] <;> simp_all +decide [ StarInvariant ];
  · refine Or.inr <| Or.inr <| Or.inr <| Or.inl ⟨ w.flatten ++ β, ?_, ?_ ⟩ <;> simp_all +decide [ KStar.kstar ];
    exact ⟨ w ++ [ β ], by simp +decide, fun y hy => by aesop ⟩;
  · right;
    right;
    refine Or.inr <| Or.inr <| Or.inr ?_;
    refine' ⟨ _, _, _, _ ⟩;
    · exact blocks_end_with_H hx_empty |> fun ⟨ ω, hω ⟩ => ⟨ ( List.map ( List.map symbol.terminal ) w ).flatten ++ ( List.map symbol.terminal β ) ++ ω, by aesop ⟩;
    · refine' ⟨ _, _, _ ⟩;
      · exact fun _ _ _ _ => by rintro ⟨ ⟩ ;
      · exact fun t ht => by rintro ⟨ ⟩ ;
      · exact fun y hy => ⟨ fun z hz => wrap_sym_ne_Z z, by rintro ⟨ ⟩ ⟩;
    · rintro x hx y hy; exact ne_of_apply_ne ( fun z => z ) ( by simp +decide [ R ] ) ;
    · exact ⟨ fun x hx => by rintro ⟨ ⟩, fun x hx => ⟨ fun y hy => wrap_sym_ne_R _, by rintro ⟨ ⟩ ⟩ ⟩

/-
Case 3 sub-case: R·t → t·R scanning
-/
private lemma star_case_3_scan {g : grammar T}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    {t : T}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ symbol.terminal t :: γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ) :
    StarInvariant g
      (List.map symbol.terminal (w.flatten ++ β ++ [t]) ++ [R] ++
       List.map wrap_sym γ ++ [H] ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) := by
  refine Or.inr <| Or.inr <| Or.inl ⟨ w, β ++ [ t ], γ, x, ?_, ?_, ?_, ?_ ⟩;
  · assumption;
  · aesop;
  · assumption;
  · simp +decide [ List.map_append ]

/-
Case 3: Scanning phase
-/
private lemma star_case_3 {g : grammar T} {α' : List (ns T g.nt)}
    {w : List (List T)} {β : List T} {γ : List (symbol T g.nt)}
    {x : List (List (symbol T g.nt))}
    (hw : ∀ wᵢ ∈ w, grammar_generates g wᵢ)
    (hβγ : grammar_derives g [symbol.nonterminal g.initial]
      (List.map symbol.terminal β ++ γ))
    (hx : ∀ xᵢ ∈ x, grammar_derives g [symbol.nonterminal g.initial] xᵢ)
    (h_step : grammar_transforms (star_grammar g)
      (List.map symbol.terminal w.flatten ++
       List.map symbol.terminal β ++ [R] ++
       List.map wrap_sym γ ++ [H] ++
       (List.map (· ++ [H]) (List.map (List.map wrap_sym) x)).flatten) α') :
  StarInvariant g α' := by
  obtain ⟨ r, hr, u, v, hbef, rfl ⟩ := h_step;
  by_cases h : ∃ i : Fin 3, r.input_N = Sum.inr i;
  · rcases h with ⟨ i, hi ⟩ ; fin_cases i <;> simp_all +decide [ star_grammar ] ;
    · replace hbef := congr_arg ( fun l => Z ∈ l ) hbef ; simp_all +decide [ Z_not_in_case3_string ] ;
      contrapose! hbef; simp_all +decide [ Z, R, H ] ;
      exact ⟨ fun a ha => wrap_sym_ne_Z a, fun a ha b hb => wrap_sym_ne_Z b ⟩;
    · exact False.elim <| no_H_rule ( by
        unfold star_grammar; aesop; ) hi;
    · -- By R_unique_in_case3, u = map terminal (w.flatten ++ β).
      have hu : u = List.map symbol.terminal (w.flatten ++ β) := by
        apply R_unique_in_case3;
        convert hbef using 1;
        rotate_left;
        rotate_left;
        exact γ;
        exact x;
        exact r.input_R ++ v;
        · simp +decide [ List.map_flatMap, List.flatten ];
        · rcases hr with ( rfl | rfl | rfl | rfl | ⟨ a, ha, rfl ⟩ | hr ) <;> simp_all +decide [ wrap_gr ];
          · rfl;
          · rfl;
          · unfold rules_that_scan_terminals at hr; aesop;
      rcases hr with ( rfl | rfl | rfl | rfl | ⟨ r₀, hr₀, rfl ⟩ | hr_scan ) <;> simp_all +decide [ star_grammar ];
      · have hγ : γ = [] := by
          cases γ <;> simp_all +decide [ List.map ];
          cases ‹symbol T g.nt› <;> simp_all +decide [ wrap_sym ];
          · cases hbef.2.1;
          · cases hbef.2.1;
        convert star_case_3_RH_to_R hw ( show grammar_generates g β from ?_ ) hx using 1;
        · aesop;
        · unfold grammar_generates; aesop;
      · cases γ <;> simp_all +decide [ wrap_sym ];
        · convert star_case_3_RH_to_eps hw _ hx using 1;
          rotate_left;
          exact β;
          · convert hβγ using 1;
          · simp +decide [ ← hbef.2, List.map_append, List.flatten_append ];
        · cases ‹symbol T g.nt› <;> simp_all +decide [ H ];
      · unfold wrap_gr at hi; aesop;
      · unfold rules_that_scan_terminals at hr_scan; simp_all +decide [ List.mem_map ] ;
        rcases hr_scan with ⟨ a, ha, rfl ⟩ ; simp_all +decide [ List.map ] ;
        cases γ <;> simp_all +decide [ List.map ];
        · cases hbef.2.1;
        · cases ‹symbol T g.nt› <;> simp_all +decide [ wrap_sym ];
          exact Or.inr <| Or.inr <| Or.inl ⟨ w, β ++ [ a ], ‹_›, x, hw, by
            simpa [ List.map_append ] using hβγ, hx, by
            grind ⟩;
  · obtain ⟨ r₀, hr₀, rfl ⟩ := extract_wrapped_rule hr ( by simpa using h );
    convert star_case_3_wrapped hw hβγ hx hr₀ hbef using 1

/-
No rule of star_grammar with input_N = Sum.inr can match a string
    of the form `map wrap_sym σ ++ [R]`.
-/
private lemma no_inr_rule_on_wrap_R {g : grammar T} {σ : List (symbol T g.nt)}
    {r : grule T (nn g.nt)} {u v : List (ns T g.nt)}
    (hr : r ∈ (star_grammar g).rules)
    (hinr : ∃ i : Fin 3, r.input_N = Sum.inr i)
    (hbef : List.map wrap_sym σ ++ [R] =
      u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) :
  False := by
  rcases hinr with ⟨ i, hi ⟩ ; rcases i with ( _ | _ | _ | i ) <;> simp_all +decide [ star_grammar ];
  · replace hbef := congr_arg List.reverse hbef ; simp_all +decide [ List.reverse_append ];
    cases v : v.reverse <;> simp_all +decide [ List.reverse_singleton ];
    · grind +locals;
    · have h_contra : ∀ x ∈ List.map wrap_sym σ, x ≠ symbol.nonterminal (Sum.inr 0) := by
        simp +zetaDelta at *;
        intro a ha; cases a <;> simp +decide [ wrap_sym ] ;
      grind;
  · rcases hr with ( rfl | rfl | rfl | rfl | ⟨ a, ha, rfl ⟩ | hr ) <;> simp_all +decide [ List.append_assoc ];
    · cases hi;
    · unfold rules_that_scan_terminals at hr; aesop;
  · rcases hr with ( rfl | rfl | rfl | rfl | ⟨ a, ha, rfl ⟩ | hr ) <;> simp_all +decide [ List.append_assoc ];
    · replace hbef := congr_arg ( fun x => x.dropLast ) hbef ; simp_all +decide [ List.dropLast ] ;
      induction σ generalizing u v <;> simp_all +decide [ List.map ];
      cases u <;> simp_all +decide [ List.dropLast ];
      cases ‹symbol T g.nt› <;> simp_all +decide [ wrap_sym ];
    · replace hbef := congr_arg ( fun x => x.dropLast ) hbef ; simp_all +decide [ List.dropLast ] ;
      induction σ generalizing u v <;> simp_all +decide [ List.map ];
      cases u <;> simp_all +decide [ List.dropLast ];
      cases ‹symbol T g.nt› <;> simp_all +decide [ wrap_sym ];
    · cases hi;
    · replace hbef := congr_arg List.reverse hbef ; simp_all +decide [ List.reverse_append ];
      replace hbef := congr_arg List.tail hbef ; simp_all +decide [ List.tail_append ];
      split_ifs at hbef <;> simp_all +decide [ List.map_eq_append_iff ];
      · unfold rules_that_scan_terminals at hr; aesop;
      · obtain ⟨ l₁, l₁_1, l₂, rfl, hu, hl₁, hl₂ ⟩ := hbef; replace hl₂ := congr_arg List.head? hl₂; simp_all +decide [ List.head? ] ;
        cases l₂ <;> simp_all +decide [ wrap_sym ];
        cases ‹symbol T g.nt› <;> cases hl₂;
      · rcases hbef with ⟨ l₁, l₁_1, l₂, rfl, rfl, h₁, h₂ ⟩ ; replace h₂ := congr_arg List.head? h₂ ; simp_all +decide [ List.head? ] ;
        rcases l₂ with ( _ | ⟨ a, l₂ ⟩ ) <;> simp_all +decide [ List.map ];
        cases a <;> cases h₂;
  · linarith

/-
Case 5: β = map wrap_sym σ ++ [R]
-/
private lemma star_case_5 {g : grammar T} {α' : List (ns T g.nt)}
    {σ : List (symbol T g.nt)}
    (h_step : grammar_transforms (star_grammar g)
      (List.map wrap_sym σ ++ [R]) α') :
  StarInvariant g α' := by
  unfold grammar_transforms at h_step; unfold StarInvariant at *;
  obtain ⟨ r, hr, u, v, hbef, rfl ⟩ := h_step;
  by_cases h : ∃ i : Fin 3, r.input_N = Sum.inr i;
  · exact False.elim <| no_inr_rule_on_wrap_R hr h hbef;
  · -- Since r is a wrapped rule, we can write it as r = wrap_gr r₀ for some r₀ ∈ g.rules.
    obtain ⟨r₀, hr₀, hr_eq⟩ : ∃ r₀ ∈ g.rules, r = wrap_gr r₀ := by
      unfold star_grammar at hr; simp_all +decide [ List.mem_map ] ;
      unfold rules_that_scan_terminals at hr; simp_all +decide [ List.mem_map ] ;
      rcases hr with ( rfl | rfl | rfl | rfl | ⟨ r₀, hr₀, rfl ⟩ | ⟨ t, ht, rfl ⟩ ) <;> tauto;
    -- Since R is not in the map of wrap_sym, the only way for R to appear in the list is if it is the last element of v.
    have hv_last : R ∈ v := by
      replace hbef := congr_arg List.reverse hbef ; simp_all +decide [ List.reverse_append ] ;
      replace hbef := congr_arg List.head? hbef ; simp_all +decide;
      cases v <;> simp_all +decide [ List.getLast? ];
      cases h : ( wrap_gr r₀ ).input_R <;> simp_all +decide [ List.getLast ];
      · cases h : ( wrap_gr r₀ ).input_N <;> simp_all +decide [ R ];
        tauto;
      · unfold wrap_gr at h; simp_all +decide [ List.getLast ] ;
        grind +suggestions;
    -- Since R is the last element of v, we can write v as v' ++ [R] for some v'.
    obtain ⟨v', hv'⟩ : ∃ v', v = v' ++ [R] := by
      have hv_last : R ∈ v → ∃ v', v = v' ++ [R] := by
        intro hv_last
        induction' v with v ih;
        · contradiction;
        · induction' ih using List.reverseRecOn with ih ih ih <;> simp_all +decide [ List.map ];
          replace hbef := congr_arg List.reverse hbef ; simp_all +decide [ List.reverse_append ];
          cases ih <;> simp_all +decide [ wrap_gr ];
          · cases hbef.1;
          · exact ⟨ v :: ih, by simp +decide ⟩;
      exact hv_last ‹_›;
    simp_all +decide [ wrap_gr ];
    -- Since `wrap_sym` is injective, we can find preimages `u₀` and `v₀` for `u` and `v'` respectively.
    obtain ⟨u₀, hu₀⟩ : ∃ u₀ : List (symbol T g.nt), List.map wrap_sym u₀ = u := by
      have hu₀ : u = List.take (u.length) (List.map wrap_sym σ ++ [R]) := by
        rw [ hbef, List.take_append_of_le_length ] <;> norm_num;
      rw [ hu₀, List.take_append_of_le_length ] <;> norm_num;
      · exact ⟨ List.take u.length σ, by rw [ List.map_take ] ⟩;
      · grind
    obtain ⟨v₀, hv₀⟩ : ∃ v₀ : List (symbol T g.nt), List.map wrap_sym v₀ = v' := by
      have hv₀ : ∀ x ∈ v', ∃ y : symbol T g.nt, wrap_sym y = x := by
        intro x hx
        have hx_in_map : x ∈ List.map wrap_sym (σ ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R) := by
          replace hbef := congr_arg List.reverse hbef; simp_all +decide [ List.reverse_append ] ;
        exact List.mem_map.mp hx_in_map |> Exists.imp fun y hy => hy.2;
      have hv₀ : ∀ {l : List (ns T g.nt)}, (∀ x ∈ l, ∃ y : symbol T g.nt, wrap_sym y = x) → ∃ v₀ : List (symbol T g.nt), List.map wrap_sym v₀ = l := by
        intros l hl; induction' l with x l ih <;> simp_all +decide [ List.map ] ;
        rcases hl.1 with ⟨ y, rfl ⟩ ; obtain ⟨ v₀, hv₀ ⟩ := ih; exact ⟨ y :: v₀, by simp +decide [ hv₀ ] ⟩ ;
      exact hv₀ ‹_›;
    refine Or.inr <| Or.inr <| Or.inr <| Or.inr <| ⟨ u₀ ++ r₀.output_string ++ v₀, ?_ ⟩ ; aesop

-- Need: ∃ σ', u ++ map wrap_sym r₀.output ++ v' ++ [R] = map wrap_sym σ' ++ [R]

/-
Case 6: β = ω ++ [H], Z ∉ β, R ∉ β
-/
private lemma star_case_6 {g : grammar T} {α' : List (ns T g.nt)}
    {ω : List (ns T g.nt)}
    (h_noZ : Z ∉ ω ++ [H])
    (h_noR : R ∉ ω ++ [H])
    (h_step : grammar_transforms (star_grammar g) (ω ++ [H]) α') :
  StarInvariant g α' := by
  rcases h_step with ⟨ r, h₁, h₂, h₃, _, rfl, h₅ ⟩;
  rcases r with ⟨ L, N, R, S ⟩;
  rcases N with ( N | N ) <;> simp_all +decide [ star_grammar ];
  · rcases h₁ with ( ⟨ r, hr, hr' ⟩ | hr );
    · unfold wrap_gr at hr'; simp_all +decide [ List.map_append ] ;
      refine Or.inr <| Or.inr <| Or.inr <| Or.inr <| Or.inr ⟨ ?_, ?_, ?_ ⟩;
      · use h₂ ++ S ++ h₃.dropLast;
        simp_all +decide [ List.append_assoc ];
        rw [ List.dropLast_append_getLast? ];
        replace := congr_arg List.reverse ‹_›; norm_num [ List.reverse_append ] at this;
        replace this := congr_arg List.head? this; simp_all +decide ;
        cases h₃ <;> simp_all +decide [ List.getLast? ];
        cases R <;> simp_all +decide [ List.getLast ];
        · cases this;
        · grind +suggestions;
      · simp_all +decide [ ← hr'.2.2.2 ];
        exact?;
      · grind +suggestions;
    · unfold rules_that_scan_terminals at hr; aesop;
  · fin_cases N <;> simp_all +decide [ star_grammar ];
    · tauto;
    · rcases h₁ with ( ⟨ r, hr, hr' ⟩ | hr ) <;> simp_all +decide [ wrap_gr, rules_that_scan_terminals ];
    · unfold _root_.R at * ; tauto

/-- The StarInvariant is preserved under one grammar_transforms step. -/
private lemma star_invariant_step {g : grammar T} {β α' : List (ns T g.nt)}
    (h_inv : StarInvariant g β)
    (h_step : grammar_transforms (star_grammar g) β α') :
  StarInvariant g α' := by
  unfold StarInvariant at h_inv
  rcases h_inv with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩ |
    ⟨w, β, γ, x, hw, hβγ, hx, rfl⟩ | ⟨u, hu, rfl⟩ | ⟨σ, rfl⟩ | ⟨⟨ω, rfl⟩, hnoZ, hnoR⟩
  · exact star_case_1 hx h_step
  · exact star_case_2 hx h_step
  · exact star_case_3 hw hβγ hx h_step
  · exact absurd h_step no_transform_all_terminals
  · exact star_case_5 h_step
  · exact star_case_6 hnoZ hnoR h_step

private lemma star_induction {g : grammar T} {α : List (ns T g.nt)}
    (ass : grammar_derives (star_grammar g) [Z] α) :
  StarInvariant g α := by
  induction ass with
  | refl =>
    -- Base case: α = [Z], which is case 1 with x = []
    left
    exact ⟨[], by simp, by simp⟩
  | tail _ step ih =>
    exact star_invariant_step ih step

-- The hard direction: grammar_language (star_grammar g) ⊆ L*
private lemma in_star_of_in_star_grammar {g : grammar T} {w : List T}
    (hw : grammar_generates (star_grammar g) w) :
  w ∈ KStar.kstar (grammar_language g) := by
  have result := star_induction hw
  unfold StarInvariant at result
  rcases result with ⟨x, _, hα⟩ | ⟨x, _, hα⟩ |
    ⟨w', β, γ, x, _, _, _, hα⟩ | ⟨u, hu, hα⟩ | ⟨σ, hα⟩ | ⟨⟨ω, hα⟩, _, _⟩
  · exfalso
    have : (Z : ns T g.nt) ∈ List.map symbol.terminal w := by rw [hα]; simp
    exact nonterminal_not_in_map_terminal this
  · exfalso
    have : (R : ns T g.nt) ∈ List.map symbol.terminal w := by rw [hα]; simp
    exact nonterminal_not_in_map_terminal this
  · exfalso
    have : (R : ns T g.nt) ∈ List.map symbol.terminal w := by
      rw [hα]; simp [List.mem_append]
    exact nonterminal_not_in_map_terminal this
  · have w_eq : w = u := by
      have hinj : Function.Injective (symbol.terminal (T := T) (N := (star_grammar g).nt)) := by
        intro a b h; cases h; rfl
      exact (List.map_injective_iff.mpr hinj) hα
    rw [w_eq]; exact hu
  · exfalso
    have : (R : ns T g.nt) ∈ List.map symbol.terminal w := by
      rw [hα]; simp [List.mem_append]
    exact nonterminal_not_in_map_terminal this
  · exfalso
    have : (H : ns T g.nt) ∈ List.map symbol.terminal w := by
      rw [hα]; simp [List.mem_append]
    exact nonterminal_not_in_map_terminal this

end hard_direction

/-- The class of recursively enumerable languages is closed under the Kleene star. -/
theorem RE_of_star_RE (L : Language T) :
    is_RE L → is_RE (KStar.kstar L) := by
  rintro ⟨g, hg⟩
  use star_grammar g
  ext w
  constructor
  · intro hw
    rw [← hg]
    exact in_star_of_in_star_grammar hw
  · intro hw
    rw [← hg] at hw
    exact in_star_grammar_of_in_star hw

/-- The class of recursively enumerable languages is closed under Kleene star. -/
theorem RE_closedUnderKleeneStar : ClosedUnderKleeneStar (α := T) is_RE :=
  fun L hL => RE_of_star_RE L hL