import Mathlib
import Langlib.Grammars.Unrestricted.Toolbox
import Langlib.Classes.RecursivelyEnumerable.Definition
import Langlib.Utilities.ListUtils
import Langlib.Utilities.ClosurePredicates

/-! # RE Closure Under Concatenation

This file constructs an unrestricted grammar for the concatenation of two recursively enumerable languages.

## Main declarations

- `big_grammar`
- `in_big_of_in_concatenated`
- `in_concatenated_of_in_big`
- `RE_of_RE_c_RE`
-/


-- new nonterminal type
def nnn (T N₁ N₂ : Type) : Type :=
Option (N₁ ⊕ N₂) ⊕ (T ⊕ T)

-- new symbol type
abbrev nst (T N₁ N₂ : Type) : Type :=
symbol T (nnn T N₁ N₂)

variable {T : Type}


section the_construction

def wrap_symbol₁ {N₁ : Type} (N₂ : Type) : symbol T N₁ → nst T N₁ N₂
| (symbol.terminal t)    => symbol.nonterminal (Sum.inr (Sum.inl t))
| (symbol.nonterminal n) => symbol.nonterminal (Sum.inl (some (Sum.inl n)))

def wrap_symbol₂ {N₂ : Type} (N₁ : Type) : symbol T N₂ → nst T N₁ N₂
| (symbol.terminal t)    => symbol.nonterminal (Sum.inr (Sum.inr t))
| (symbol.nonterminal n) => symbol.nonterminal (Sum.inl (some (Sum.inr n)))

private def wrap_grule₁ {N₁ : Type} (N₂ : Type) (r : grule T N₁) : grule T (nnn T N₁ N₂) :=
grule.mk
  (List.map (wrap_symbol₁ N₂) r.input_L)
  (Sum.inl (some (Sum.inl r.input_N)))
  (List.map (wrap_symbol₁ N₂) r.input_R)
  (List.map (wrap_symbol₁ N₂) r.output_string)

private def wrap_grule₂ {N₂ : Type} (N₁ : Type) (r : grule T N₂) : grule T (nnn T N₁ N₂) :=
grule.mk
  (List.map (wrap_symbol₂ N₁) r.input_L)
  (Sum.inl (some (Sum.inr r.input_N)))
  (List.map (wrap_symbol₂ N₁) r.input_R)
  (List.map (wrap_symbol₂ N₁) r.output_string)

def rules_for_terminals₁ (N₂ : Type) (g : grammar T) : List (grule T (nnn T g.nt N₂)) :=
List.map (fun t => grule.mk [] (Sum.inr (Sum.inl t)) [] [symbol.terminal t]) (all_used_terminals g)

def rules_for_terminals₂ (N₁ : Type) (g : grammar T) : List (grule T (nnn T N₁ g.nt)) :=
List.map (fun t => grule.mk [] (Sum.inr (Sum.inr t)) [] [symbol.terminal t]) (all_used_terminals g)

-- the grammar for concatenation of `g₁` and `g₂` languages
def big_grammar (g₁ g₂ : grammar T) : grammar T :=
grammar.mk (nnn T g₁.nt g₂.nt) (Sum.inl none) (
  (grule.mk [] (Sum.inl none) [] [
    symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))),
    symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))]
  ) :: (
    (List.map (wrap_grule₁ g₂.nt) g₁.rules ++ List.map (wrap_grule₂ g₁.nt) g₂.rules) ++
    (rules_for_terminals₁ g₂.nt g₁ ++ rules_for_terminals₂ g₁.nt g₂)
  )
)

end the_construction


section easy_direction

lemma grammar_generates_only_legit_terminals
    {g : grammar T}
    {w : List (symbol T g.nt)}
    (ass : grammar_derives g [symbol.nonterminal g.initial] w)
    {s : symbol T g.nt}
    (symbol_derived : s ∈ w) :
  (∃ r : grule T g.nt, r ∈ g.rules ∧ s ∈ r.output_string) ∨
  (s = symbol.nonterminal g.initial) :=
by
  induction ass with
  | refl =>
      rw [List.mem_singleton] at symbol_derived
      right
      exact symbol_derived
  | tail _ orig ih =>
      rcases orig with ⟨r, rin, u, v, bef, aft⟩
      rw [aft] at symbol_derived
      rw [List.mem_append] at symbol_derived
      rw [List.mem_append] at symbol_derived
      cases symbol_derived with
      | inl symbol_derived =>
          cases symbol_derived with
          | inl symbol_derived =>
              apply ih
              rw [bef]
              repeat
                rw [List.mem_append]
                left
              exact symbol_derived
          | inr symbol_derived =>
              left
              refine ⟨r, rin, ?_⟩
              exact symbol_derived
      | inr symbol_derived =>
          apply ih
          rw [bef]
          rw [List.mem_append]
          right
          exact symbol_derived

private lemma first_transformation {g₁ g₂ : grammar T} :
  grammar_transforms (big_grammar g₁ g₂) [symbol.nonterminal (big_grammar g₁ g₂).initial] [
      symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))),
      symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))
    ] :=
by
  have hlen : 0 < (big_grammar g₁ g₂).rules.length := by
    simp [big_grammar]
  refine ⟨(big_grammar g₁ g₂).rules.nthLe 0 hlen, ?_, ?_⟩
  ·
    exact List.nthLe_mem hlen
  ·
    refine ⟨[], [], ?_, ?_⟩ <;> rfl

private lemma substitute_terminals
    {g₁ g₂ : grammar T}
    {side : T → T ⊕ T}
    {w : List T}
    (rule_for_each_terminal : ∀ t ∈ w,
      (grule.mk [] (Sum.inr (side t)) [] [symbol.terminal t]) ∈
        (rules_for_terminals₁ g₂.nt g₁ ++ rules_for_terminals₂ g₁.nt g₂)) :
  grammar_derives (big_grammar g₁ g₂)
    (List.map (symbol.nonterminal ∘ Sum.inr ∘ side) w)
    (List.map symbol.terminal w) :=
by
  induction w with
  | nil =>
      exact grammar_deri_self
  | cons d l ih =>
      simp [List.map]
      have step_head :
        grammar_transforms (big_grammar g₁ g₂)
          ([(symbol.nonterminal ∘ Sum.inr ∘ side) d] ++ List.map (symbol.nonterminal ∘ Sum.inr ∘ side) l)
          ([symbol.terminal d] ++ List.map (symbol.nonterminal ∘ Sum.inr ∘ side) l) := by
        refine ⟨grule.mk [] (Sum.inr (side d)) [] [symbol.terminal d], ?_, ?_⟩
        ·
          change _ ∈ List.cons _ _
          apply List.mem_cons_of_mem
          apply List.mem_append_right
          have : d ∈ d :: l := by simpa using (List.mem_cons_self d l)
          exact rule_for_each_terminal d this
        ·
          refine ⟨[], List.map (symbol.nonterminal ∘ Sum.inr ∘ side) l, ?_, ?_⟩ <;> rfl
      apply grammar_deri_of_tran_deri step_head
      apply grammar_deri_with_prefix
      apply ih
      intro t tin
      exact rule_for_each_terminal t (List.mem_cons_of_mem _ tin)

/-
PROVIDED SOLUTION
From ass, extract w₁ and w₂ with w = w₁ ++ w₂, w₁ ∈ grammar_language g₁, w₂ ∈ grammar_language g₂. The proof proceeds by:
1. Apply first_transformation to derive from initial to [wrap(g₁.initial), wrap(g₂.initial)].
2. Lift the derivation of g₁ generating w₁ using wrap_symbol₁, and the derivation of g₂ generating w₂ using wrap_symbol₂. The lifted rules are in big_grammar by construction.
3. Apply substitute_terminals to convert the wrapped terminal symbols to actual terminals.
4. Combine these three phases of derivation using grammar_deri_of_deri_deri.

Key steps: first_transformation gives the initial step. Then grammar_deri_with_postfix and grammar_deri_with_prefix allow combining the two independent derivations. Finally substitute_terminals handles the terminal conversion phase.
-/
lemma in_big_of_in_concatenated
    {g₁ g₂ : grammar T}
    {w : List T}
    (ass : w ∈ grammar_language g₁ * grammar_language g₂) :
  w ∈ grammar_language (big_grammar g₁ g₂) :=
by
  obtain ⟨w₁, w₂, hw₁, hw₂, rfl⟩ : ∃ w₁ w₂, w₁ ∈ grammar_language g₁ ∧ w₂ ∈ grammar_language g₂ ∧ w = w₁ ++ w₂ := by
    cases ass ; aesop;
  -- By definition of big_grammar, we know that if w₁ is generated by g₁ and w₂ is generated by g₂, then w₁ ++ w₂ can be generated by big_grammar.
  have h_derive : grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl none)] (List.map (wrap_symbol₁ g₂.nt) (List.map symbol.terminal w₁) ++ List.map (wrap_symbol₂ g₁.nt) (List.map symbol.terminal w₂)) := by
    have h_derive : grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))), symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))] (List.map (wrap_symbol₁ g₂.nt) (List.map symbol.terminal w₁) ++ List.map (wrap_symbol₂ g₁.nt) (List.map symbol.terminal w₂)) := by
      have h_derive : ∀ {w : List (symbol T g₁.nt)}, grammar_derives g₁ [symbol.nonterminal g₁.initial] w → grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial)))] (List.map (wrap_symbol₁ g₂.nt) w) := by
        intro w hw
        induction' hw with w' hw' ih;
        · constructor;
        · rename_i h₁ h₂;
          obtain ⟨ r, hr, u, v, rfl, rfl ⟩ := h₁;
          convert h₂.tail _ using 1;
          use wrap_grule₁ g₂.nt r;
          grind +locals;
      have h_derive₂ : ∀ {w : List (symbol T g₂.nt)}, grammar_derives g₂ [symbol.nonterminal g₂.initial] w → grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))] (List.map (wrap_symbol₂ g₁.nt) w) := by
        intro w hw
        induction' hw with w₁ w₂ hw₁ hw₂ ih;
        · constructor;
        · obtain ⟨ r, hr, u, v, rfl, rfl ⟩ := hw₂;
          refine' ih.tail _;
          use grule.mk (List.map (wrap_symbol₂ g₁.nt) r.input_L) (Sum.inl (some (Sum.inr r.input_N))) (List.map (wrap_symbol₂ g₁.nt) r.input_R) (List.map (wrap_symbol₂ g₁.nt) r.output_string);
          unfold big_grammar; aesop;
      convert grammar_deri_with_postfix _ ( h_derive hw₁ ) |> grammar_deri_of_deri_deri <| grammar_deri_with_prefix _ ( h_derive₂ hw₂ ) using 1;
    exact grammar_deri_of_deri_deri ( grammar_deri_of_tran ( first_transformation ) ) h_derive;
  -- Apply the substitute_terminals lemma to convert the wrapped terminal symbols to actual terminals.
  have h_subst : grammar_derives (big_grammar g₁ g₂) (List.map (wrap_symbol₁ g₂.nt) (List.map symbol.terminal w₁) ++ List.map (wrap_symbol₂ g₁.nt) (List.map symbol.terminal w₂)) (List.map symbol.terminal w₁ ++ List.map symbol.terminal w₂) := by
    have h_subst : ∀ t ∈ w₁, (grule.mk [] (Sum.inr (Sum.inl t)) [] [symbol.terminal t]) ∈ (rules_for_terminals₁ g₂.nt g₁ ++ rules_for_terminals₂ g₁.nt g₂) := by
      intro t ht
      have h_term : t ∈ all_used_terminals g₁ := by
        have h_term : ∀ {w : List (symbol T g₁.nt)}, grammar_derives g₁ [symbol.nonterminal g₁.initial] w → ∀ t ∈ w, t = symbol.nonterminal g₁.initial ∨ ∃ r ∈ g₁.rules, t ∈ r.output_string := by
          intros w hw t ht; exact (by
          have := grammar_generates_only_legit_terminals hw ht; aesop;);
        specialize h_term hw₁ (symbol.terminal t);
        unfold all_used_terminals; aesop;
      unfold rules_for_terminals₁; aesop;
    have h_subst : ∀ t ∈ w₂, (grule.mk [] (Sum.inr (Sum.inr t)) [] [symbol.terminal t]) ∈ (rules_for_terminals₁ g₂.nt g₁ ++ rules_for_terminals₂ g₁.nt g₂) := by
      intro t ht
      have h_subst : t ∈ all_used_terminals g₂ := by
        have h_subst : ∀ {w : List (symbol T g₂.nt)}, grammar_derives g₂ [symbol.nonterminal g₂.initial] w → ∀ s ∈ w, s = symbol.terminal t → t ∈ all_used_terminals g₂ := by
          intros w hw s hs hs_eq
          have h_subst : ∃ r : grule T g₂.nt, r ∈ g₂.rules ∧ s ∈ r.output_string := by
            have := grammar_generates_only_legit_terminals hw hs; aesop;
          unfold all_used_terminals; aesop;
        exact h_subst hw₂ _ ( List.mem_map.mpr ⟨ t, ht, rfl ⟩ ) rfl
      simp [rules_for_terminals₂, h_subst];
    convert grammar_deri_with_postfix _ ( substitute_terminals _ ) |> grammar_deri_of_deri_deri <| grammar_deri_with_prefix _ ( substitute_terminals _ ) using 1;
    rotate_left;
    use fun t => Sum.inl t;
    grind +splitIndPred;
    use fun t => Sum.inr t;
    · assumption;
    · unfold wrap_symbol₁ wrap_symbol₂; aesop;
  refine' h_derive.trans h_subst |> fun h => h.trans _;
  grind

end easy_direction


section hard_direction

section correspondence_for_terminals

private def corresponding_symbols {N₁ N₂ : Type} : nst T N₁ N₂ → nst T N₁ N₂ → Prop
| symbol.terminal t,                               symbol.terminal t'                               => t = t'
| symbol.nonterminal (Sum.inr (Sum.inl a)),        symbol.nonterminal (Sum.inr (Sum.inl a'))        => a = a'
| symbol.nonterminal (Sum.inr (Sum.inr a)),        symbol.nonterminal (Sum.inr (Sum.inr a'))        => a = a'
| symbol.nonterminal (Sum.inr (Sum.inl a)),        symbol.terminal t                                => t = a
| symbol.nonterminal (Sum.inr (Sum.inr a)),        symbol.terminal t                                => t = a
| symbol.nonterminal (Sum.inl (some (Sum.inl n))), symbol.nonterminal (Sum.inl (some (Sum.inl n'))) => n = n'
| symbol.nonterminal (Sum.inl (some (Sum.inr n))), symbol.nonterminal (Sum.inl (some (Sum.inr n'))) => n = n'
| symbol.nonterminal (Sum.inl none),               symbol.nonterminal (Sum.inl none)                => True
| _,                                               _                                                => False

private lemma corresponding_symbols_self {N₁ N₂ : Type} (s : nst T N₁ N₂) : corresponding_symbols s s :=
by
  cases s with
  | terminal t => rfl
  | nonterminal n =>
      cases n with
      | inl o =>
          cases o with
          | none => trivial
          | some s =>
              cases s with
              | inl => rfl
              | inr => rfl
      | inr s =>
          cases s with
          | inl => rfl
          | inr => rfl

private lemma corresponding_symbols_never₁ {N₁ N₂ : Type} {s₁ : symbol T N₁} {s₂ : symbol T N₂} :
  ¬ corresponding_symbols (wrap_symbol₁ N₂ s₁) (wrap_symbol₂ N₁ s₂) :=
by
  cases s₁ <;> cases s₂ <;> simp [wrap_symbol₁, wrap_symbol₂, corresponding_symbols]

private lemma corresponding_symbols_never₂ {N₁ N₂ : Type} {s₁ : symbol T N₁} {s₂ : symbol T N₂} :
  ¬ corresponding_symbols (wrap_symbol₂ N₁ s₂) (wrap_symbol₁ N₂ s₁) :=
by
  cases s₁ <;> cases s₂ <;> simp [wrap_symbol₁, wrap_symbol₂, corresponding_symbols]

private def corresponding_strings {N₁ N₂ : Type} : List (nst T N₁ N₂) → List (nst T N₁ N₂) → Prop :=
List.Forall₂ corresponding_symbols

private lemma corresponding_strings_self {N₁ N₂ : Type} {x : List (nst T N₁ N₂)} :
  corresponding_strings x x :=
by
  induction x with
  | nil =>
      simp [corresponding_strings]
  | cons s xs ih =>
      simp [corresponding_strings, corresponding_symbols_self, ih]

private lemma corresponding_strings_singleton {N₁ N₂ : Type} {s₁ s₂ : nst T N₁ N₂}
    (ass : corresponding_symbols s₁ s₂) :
  corresponding_strings [s₁] [s₂] :=
by
  simp [corresponding_strings, ass]

private lemma corresponding_strings_append {N₁ N₂ : Type} {x₁ x₂ y₁ y₂ : List (nst T N₁ N₂)}
    (ass₁ : corresponding_strings x₁ y₁)
    (ass₂ : corresponding_strings x₂ y₂) :
  corresponding_strings (x₁ ++ x₂) (y₁ ++ y₂) :=
by
  unfold corresponding_strings at *
  exact List.rel_append ass₁ ass₂

private lemma corresponding_strings_length {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)}
    (ass : corresponding_strings x y) :
  x.length = y.length :=
by
  unfold corresponding_strings at ass
  exact List.Forall₂.length_eq ass

/-
PROVIDED SOLUTION
This follows directly from list_forall₂_nth_le applied to corresponding_strings (which is just List.Forall₂ corresponding_symbols).
-/
private lemma corresponding_strings_nth_le {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)} {i : ℕ}
    (i_lt_len_x : i < x.length) (i_lt_len_y : i < y.length)
    (ass : corresponding_strings x y) :
  corresponding_symbols (x.nthLe i i_lt_len_x) (y.nthLe i i_lt_len_y) :=
by
  have h_nth : ∀ {x y : List (nst T N₁ N₂)}, List.Forall₂ corresponding_symbols x y → ∀ i i_lt_len_x i_lt_len_y, corresponding_symbols (x.nthLe i i_lt_len_x) (y.nthLe i i_lt_len_y) := by
    intros x y hxy i i_lt_len_x i_lt_len_y; induction' i with i ih generalizing x y;
    · rcases x with ( _ | ⟨ a, _ | ⟨ b, x ⟩ ⟩ ) <;> rcases y with ( _ | ⟨ c, _ | ⟨ d, y ⟩ ⟩ ) <;> simp_all +decide [ List.Forall₂ ];
      · contradiction;
      · exact hxy;
      · exact hxy.1;
    · rcases x with ( _ | ⟨ x, xs ⟩ ) <;> rcases y with ( _ | ⟨ y, ys ⟩ ) <;> norm_num at *;
      · contradiction;
      · contradiction;
      · contradiction;
      · exact ih hxy.2 ( by simpa using i_lt_len_x ) ( by simpa using i_lt_len_y );
  exact h_nth ass i i_lt_len_x i_lt_len_y

private lemma corresponding_strings_reverse {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)}
    (ass : corresponding_strings x y) :
  corresponding_strings x.reverse y.reverse :=
by
  unfold corresponding_strings at *
  rw [List.forall₂_reverse_iff]
  exact ass

private lemma corresponding_strings_of_reverse {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)}
    (ass : corresponding_strings x.reverse y.reverse) :
  corresponding_strings x y :=
by
  unfold corresponding_strings at *
  rw [List.forall₂_reverse_iff] at ass
  exact ass

private lemma corresponding_strings_take {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)}
    (n : ℕ) (ass : corresponding_strings x y) :
  corresponding_strings (List.take n x) (List.take n y) :=
by
  unfold corresponding_strings at *
  exact List.forall₂_take n ass

private lemma corresponding_strings_drop {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)}
    (n : ℕ) (ass : corresponding_strings x y) :
  corresponding_strings (List.drop n x) (List.drop n y) :=
by
  unfold corresponding_strings at *
  exact List.forall₂_drop n ass

private lemma corresponding_strings_split {N₁ N₂ : Type} {x y : List (nst T N₁ N₂)}
    (n : ℕ) (ass : corresponding_strings x y) :
  corresponding_strings (List.take n x) (List.take n y) ∧
  corresponding_strings (List.drop n x) (List.drop n y) :=
by
  constructor
  · exact corresponding_strings_take n ass
  · exact corresponding_strings_drop n ass

end correspondence_for_terminals


section unwrapping_nst

private def unwrap_symbol₁ {N₁ N₂ : Type} : nst T N₁ N₂ → Option (symbol T N₁)
| (symbol.terminal t)                               => some (symbol.terminal t)
| (symbol.nonterminal (Sum.inr (Sum.inl a)))        => some (symbol.terminal a)
| (symbol.nonterminal (Sum.inr (Sum.inr a)))        => none
| (symbol.nonterminal (Sum.inl (some (Sum.inl n)))) => some (symbol.nonterminal n)
| (symbol.nonterminal (Sum.inl (some (Sum.inr n)))) => none
| (symbol.nonterminal (Sum.inl none))               => none

private def unwrap_symbol₂ {N₁ N₂ : Type} : nst T N₁ N₂ → Option (symbol T N₂)
| (symbol.terminal t)                               => some (symbol.terminal t)
| (symbol.nonterminal (Sum.inr (Sum.inl a)))        => none
| (symbol.nonterminal (Sum.inr (Sum.inr a)))        => some (symbol.terminal a)
| (symbol.nonterminal (Sum.inl (some (Sum.inl n)))) => none
| (symbol.nonterminal (Sum.inl (some (Sum.inr n)))) => some (symbol.nonterminal n)
| (symbol.nonterminal (Sum.inl none))               => none


private lemma unwrap_wrap₁_symbol {N₁ N₂ : Type} : @unwrap_symbol₁ T N₁ N₂ ∘ wrap_symbol₁ N₂ = Option.some :=
by
  ext1 a
  cases a <;> rfl

private lemma unwrap_wrap₂_symbol {N₁ N₂ : Type} : @unwrap_symbol₂ T N₁ N₂ ∘ wrap_symbol₂ N₁ = Option.some :=
by
  ext1 a
  cases a <;> rfl

private lemma unwrap_wrap₁_string {N₁ N₂ : Type} {w : List (symbol T N₁)} :
  List.filterMap unwrap_symbol₁ (List.map (wrap_symbol₁ N₂) w) = w :=
by
  rw [List.filterMap_map]
  rw [unwrap_wrap₁_symbol]
  apply List.filterMap_some

private lemma unwrap_wrap₂_string {N₁ N₂ : Type} {w : List (symbol T N₂)} :
  List.filterMap unwrap_symbol₂ (List.map (wrap_symbol₂ N₁) w) = w :=
by
  rw [List.filterMap_map]
  rw [unwrap_wrap₂_symbol]
  apply List.filterMap_some

/-
PROVIDED SOLUTION
Case split on s₁ and s, then use the definition of corresponding_symbols and unwrap_symbol₁/wrap_symbol₁. For each case where corresponding_symbols holds, show that unwrap_symbol₁ gives back the original symbol.
-/
private lemma unwrap_eq_some_of_corresponding_symbols₁ {N₁ N₂ : Type} {s₁ : symbol T N₁} {s : nst T N₁ N₂}
    (ass : corresponding_symbols (wrap_symbol₁ N₂ s₁) s) :
  unwrap_symbol₁ s = some s₁ :=
by
  -- By definition of wrap_symbol₁, if wrap_symbol₁ s₁ is equal to s, then s must be a terminal or a nonterminal that wraps s₁.
  cases' s with s_term s_nonterm;
  · cases s₁ <;> cases ass ; aesop;
  · cases s₁ <;> cases s_nonterm <;> simp_all +decide [ corresponding_symbols ];
    · cases ‹Option ( N₁ ⊕ N₂ ) › <;> tauto;
    · cases ‹T ⊕ T› <;> simp_all +decide [ wrap_symbol₁ ];
      rfl;
    · rename_i n hn;
      rcases hn with ( _ | _ | _ ) <;> simp_all +decide [ wrap_symbol₁ ];
      exact?;
    · cases ‹T ⊕ T› <;> tauto

/-
PROVIDED SOLUTION
Case split on s₂ and s, then use the definition of corresponding_symbols and unwrap_symbol₂/wrap_symbol₂. Analogous to the ₁ version.
-/
private lemma unwrap_eq_some_of_corresponding_symbols₂ {N₁ N₂ : Type} {s₂ : symbol T N₂} {s : nst T N₁ N₂}
    (ass : corresponding_symbols (wrap_symbol₂ N₁ s₂) s) :
  unwrap_symbol₂ s = some s₂ :=
by
  -- By definition of `wrap_symbol₂`, we know that `wrap_symbol₂ N₁ s₂` is the wrapped version of `s₂`.
  cases' s₂ with t n₂;
  · unfold wrap_symbol₂ at ass;
    unfold corresponding_symbols at ass;
    unfold unwrap_symbol₂; aesop;
  · cases' s with t n₁ n₂ ; tauto;
    cases' n₁ with n₁ n₁;
    · cases' n₁ with n₁ n₁;
      · cases ass;
      · cases n₁ <;> cases ass;
        rfl;
    · cases n₁ <;> tauto

/-
PROVIDED SOLUTION
Induction on the Forall₂ relation (corresponding_strings). Base case is trivial. For the cons case, use unwrap_eq_some_of_corresponding_symbols₁ for the head and the inductive hypothesis for the tail.
-/
private lemma map_unwrap_eq_map_some_of_corresponding_strings₁ {N₁ N₂ : Type} :
  ∀ {v : List (symbol T N₁)}, ∀ {w : List (nst T N₁ N₂)},
    corresponding_strings (List.map (wrap_symbol₁ N₂) v) w →
      List.map unwrap_symbol₁ w = List.map Option.some v := by
  intro v w ass
  induction' v with v₁ v ih generalizing w <;> induction' w with w₁ w ihw <;> simp_all +decide [ List.Forall₂ ];
  · cases ass;
  · cases ass;
  · cases ass;
    exact ⟨ by exact? , ih ‹_› ⟩

/-
PROVIDED SOLUTION
Induction on the Forall₂ relation (corresponding_strings). Analogous to the ₁ version, using unwrap_eq_some_of_corresponding_symbols₂.
-/
private lemma map_unwrap_eq_map_some_of_corresponding_strings₂ {N₁ N₂ : Type} :
  ∀ {v : List (symbol T N₂)}, ∀ {w : List (nst T N₁ N₂)},
    corresponding_strings (List.map (wrap_symbol₂ N₁) v) w →
      List.map unwrap_symbol₂ w = List.map Option.some v := by
  intro v w ass
  have h_ind : ∀ {v : List (symbol T N₂)} {w : List (nst T N₁ N₂)}, corresponding_strings (List.map (wrap_symbol₂ N₁) v) w → List.map unwrap_symbol₂ w = List.map Option.some v := by
    intro v w ass
    induction' v with s₂ v ih generalizing w;
    · cases w <;> trivial;
    · rcases w with ( _ | ⟨ s, w ⟩ ) <;> simp_all +decide [ corresponding_strings ];
      grind +suggestions;
  exact h_ind ass

private lemma filter_map_unwrap_of_corresponding_strings₁ {N₁ N₂ : Type}
    {v : List (symbol T N₁)} {w : List (nst T N₁ N₂)}
    (ass : corresponding_strings (List.map (wrap_symbol₁ N₂) v) w) :
  List.filterMap unwrap_symbol₁ w = v :=
by
  apply list_filter_map_eq_of_map_eq_map_some
  exact map_unwrap_eq_map_some_of_corresponding_strings₁ ass

private lemma filter_map_unwrap_of_corresponding_strings₂ {N₁ N₂ : Type}
    {v : List (symbol T N₂)} {w : List (nst T N₁ N₂)}
    (ass : corresponding_strings (List.map (wrap_symbol₂ N₁) v) w) :
  List.filterMap unwrap_symbol₂ w = v :=
by
  apply list_filter_map_eq_of_map_eq_map_some
  exact map_unwrap_eq_map_some_of_corresponding_strings₂ ass

/-
PROVIDED SOLUTION
From ass, get z with corresponding_strings (map (wrap_symbol₁ N₂) z) w. Then filter_map_unwrap_of_corresponding_strings₁ gives filterMap unwrap_symbol₁ w = z. Substituting z back and using corresponding_string_after_wrap_unwrap_self₁'s hypothesis, we get the result. More precisely: since corresponding_strings (map (wrap_symbol₁ N₂) z) w, by filter_map_unwrap_of_corresponding_strings₁ we get filterMap unwrap_symbol₁ w = z. So map (wrap_symbol₁ N₂) (filterMap unwrap_symbol₁ w) = map (wrap_symbol₁ N₂) z, and corresponding_strings (map (wrap_symbol₁ N₂) z) w gives us the result.
-/
private lemma corresponding_string_after_wrap_unwrap_self₁ {N₁ N₂ : Type} {w : List (nst T N₁ N₂)}
    (ass : ∃ z : List (symbol T N₁), corresponding_strings (List.map (wrap_symbol₁ N₂) z) w) :
  corresponding_strings (List.map (wrap_symbol₁ N₂) (List.filterMap unwrap_symbol₁ w)) w :=
by
  obtain ⟨ z, hz ⟩ := ass; rw [ filter_map_unwrap_of_corresponding_strings₁ hz ] ; exact hz;

/-
PROVIDED SOLUTION
Analogous to ₁ version: from ass get z, use filter_map_unwrap_of_corresponding_strings₂ to get filterMap unwrap_symbol₂ w = z, then substitute back.
-/
private lemma corresponding_string_after_wrap_unwrap_self₂ {N₁ N₂ : Type} {w : List (nst T N₁ N₂)}
    (ass : ∃ z : List (symbol T N₂), corresponding_strings (List.map (wrap_symbol₂ N₁) z) w) :
  corresponding_strings (List.map (wrap_symbol₂ N₁) (List.filterMap unwrap_symbol₂ w)) w :=
by
  obtain ⟨ z, hz ⟩ := ass;
  rw [ filter_map_unwrap_of_corresponding_strings₂ hz ];
  assumption

end unwrapping_nst


section helpers_for_induction_steps

variable {N₁ N₂ : Type}

/-
PROVIDED SOLUTION
Cases on s, both give rfl.
-/
private lemma unwrap₁_of_wrap₂_eq_none (s : symbol T N₂) :
    @unwrap_symbol₁ T N₁ N₂ (wrap_symbol₂ N₁ s) = none := by
      cases s <;> rfl

/-
PROVIDED SOLUTION
Cases on s, both give rfl.
-/
private lemma unwrap₂_of_wrap₁_eq_none (s : symbol T N₁) :
    @unwrap_symbol₂ T N₁ N₂ (wrap_symbol₁ N₂ s) = none := by
      cases s <;> rfl

/-
PROVIDED SOLUTION
Induction on w, using unwrap₁_of_wrap₂_eq_none at each step.
-/
private lemma filterMap_unwrap₁_map_wrap₂ (w : List (symbol T N₂)) :
    List.filterMap (@unwrap_symbol₁ T N₁ N₂) (List.map (wrap_symbol₂ N₁) w) = [] := by
      have h_filterMap_none : ∀ s ∈ List.map (wrap_symbol₂ N₁) w, @unwrap_symbol₁ T N₁ N₂ s = none := by
        intro s hs
        obtain ⟨s', hs', rfl⟩ := List.mem_map.mp hs
        exact (by
        exact?);
      rw [ List.filterMap_eq_nil_iff ] ; aesop

/-
PROVIDED SOLUTION
Induction on w, using unwrap₂_of_wrap₁_eq_none at each step.
-/
private lemma filterMap_unwrap₂_map_wrap₁ (w : List (symbol T N₁)) :
    List.filterMap (@unwrap_symbol₂ T N₁ N₂) (List.map (wrap_symbol₁ N₂) w) = [] := by
      -- By the induction hypothesis, the filterMap of the map of wrap_symbol₁ N₂ over w is empty.
      simp [List.map_append, List.filterMap_append, *];
      exact?

/-
PROBLEM
Splitting Forall₂ at an append boundary

PROVIDED SOLUTION
Use m₁ = take l₁.length m and m₂ = drop l₁.length m. Then m = m₁ ++ m₂ by List.take_append_drop. Use List.forall₂_take and List.forall₂_drop, plus List.take_append (taking l₁.length from l₁ ++ l₂ gives l₁) and List.drop_append (dropping l₁.length from l₁ ++ l₂ gives l₂).
-/
private lemma forall₂_append_split {α β : Type} {R : α → β → Prop} {l₁ l₂ : List α} {m : List β}
    (h : List.Forall₂ R (l₁ ++ l₂) m) :
    ∃ m₁ m₂, m = m₁ ++ m₂ ∧ List.Forall₂ R l₁ m₁ ∧ List.Forall₂ R l₂ m₂ := by
      have h_split : ∀ {l₁ l₂ : List α} {m : List β}, List.Forall₂ R (l₁ ++ l₂) m → ∃ m₁ m₂, m = m₁ ++ m₂ ∧ List.Forall₂ R l₁ m₁ ∧ List.Forall₂ R l₂ m₂ := by
        intros l₁ l₂ m h; induction' l₁ with a l₁ ih generalizing l₂ m; aesop; (
        rcases m with ( _ | ⟨ b, m ⟩ ) <;> simp_all +decide [ List.forall₂_cons ];
        rcases ih h.2 with ⟨ m₁, m₂, rfl, hm₁, hm₂ ⟩ ; exact ⟨ b :: m₁, m₂, rfl, by aesop ⟩ ;);
      grind

/-
PROBLEM
The wrap_symbol₁ nonterminal Sum.inl (some (Sum.inl n₁)) cannot correspond to any wrap_symbol₂ output

PROVIDED SOLUTION
Cases on s₂. For terminal t: wrap_symbol₂ = nonterminal (Sum.inr (Sum.inr t)), corresponding_symbols with nonterminal (Sum.inl (some (Sum.inl n₁))) is False by definition. For nonterminal n: wrap_symbol₂ = nonterminal (Sum.inl (some (Sum.inr n))), corresponding_symbols with nonterminal (Sum.inl (some (Sum.inl n₁))) is False by definition.
-/
private lemma no_wrap₂_corr_sum_inl_inl {n₁ : N₁} {s₂ : symbol T N₂} :
    ¬ corresponding_symbols (wrap_symbol₂ N₁ s₂)
      (symbol.nonterminal (Sum.inl (some (Sum.inl n₁))) : nst T N₁ N₂) := by
        cases s₂ <;> aesop

/-
PROBLEM
Symmetric: wrap_symbol₂ nonterminal Sum.inl (some (Sum.inr n₂)) cannot correspond to any wrap_symbol₁ output

PROVIDED SOLUTION
Cases on s₁. For terminal t: wrap_symbol₁ = nonterminal (Sum.inr (Sum.inl t)), corresponding_symbols with nonterminal (Sum.inl (some (Sum.inr n₂))) is False. For nonterminal n: wrap_symbol₁ = nonterminal (Sum.inl (some (Sum.inl n))), corresponding_symbols with nonterminal (Sum.inl (some (Sum.inr n₂))) is False.
-/
private lemma no_wrap₁_corr_sum_inl_inr {n₂ : N₂} {s₁ : symbol T N₁} :
    ¬ corresponding_symbols (wrap_symbol₁ N₂ s₁)
      (symbol.nonterminal (Sum.inl (some (Sum.inr n₂))) : nst T N₁ N₂) := by
        cases s₁ <;> aesop

/-
PROBLEM
If corresponding_strings (map wrap₁ x ++ map wrap₂ y) a, then filterMap unwrap₁ (take x.length a) = x

PROVIDED SOLUTION
Use corresponding_strings_take x.length h. This gives corresponding_strings (take x.length (map wrap₁ x ++ map wrap₂ y)) (take x.length a). Since |map wrap₁ x| = x.length, take x.length (map wrap₁ x ++ map wrap₂ y) = map wrap₁ x (by List.take_left). So we get corresponding_strings (map wrap₁ x) (take x.length a). Then apply filter_map_unwrap_of_corresponding_strings₁.
-/
private lemma x_from_take_filterMap
    {x : List (symbol T N₁)} {y : List (symbol T N₂)}
    {a : List (nst T N₁ N₂)}
    (h : corresponding_strings (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a) :
    List.filterMap (@unwrap_symbol₁ T N₁ N₂) (List.take x.length a) = x := by
      convert filter_map_unwrap_of_corresponding_strings₁ _;
      convert corresponding_strings_take x.length h using 1;
      simp +decide [ List.take_append ]

/-
PROBLEM
Symmetric: filterMap unwrap₂ (drop x.length a) = y

PROVIDED SOLUTION
Use corresponding_strings_drop x.length h. This gives corresponding_strings (drop x.length (map wrap₁ x ++ map wrap₂ y)) (drop x.length a). Since |map wrap₁ x| = x.length, drop x.length (map wrap₁ x ++ map wrap₂ y) = map wrap₂ y (by List.drop_left). So we get corresponding_strings (map wrap₂ y) (drop x.length a). Then apply filter_map_unwrap_of_corresponding_strings₂.
-/
private lemma y_from_drop_filterMap
    {x : List (symbol T N₁)} {y : List (symbol T N₂)}
    {a : List (nst T N₁ N₂)}
    (h : corresponding_strings (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a) :
    List.filterMap (@unwrap_symbol₂ T N₁ N₂) (List.drop x.length a) = y := by
      convert filter_map_unwrap_of_corresponding_strings₂ _;
      convert corresponding_strings_drop x.length h using 1;
      simp +decide [ List.drop_append ]

/-
PROBLEM
The rule pattern from g₁ (wrapped) fits entirely within the first x.length elements

PROVIDED SOLUTION
By contradiction. Assume u.length + r₁.input_L.length + 1 + r₁.input_R.length > x.length. Then position p = u.length + r₁.input_L.length (the nonterminal position) satisfies p ≥ x.length (since p + 1 ≤ u.length + r₁.input_L.length + 1 + r₁.input_R.length > x.length, so p ≥ x.length).

At position p in a (from bef), a[p] = symbol.nonterminal (Sum.inl (some (Sum.inl r₁.input_N))).

From ih_concat, at position p, the corresponding element in (map wrap₁ x ++ map wrap₂ y) is at position p. Since p ≥ x.length = |map wrap₁ x|, this element is in map wrap₂ y, specifically (map wrap₂ y)[p - x.length] = wrap_symbol₂ N₁ (y[p - x.length]).

So corresponding_symbols (wrap_symbol₂ N₁ (y[p - x.length])) (nt (Sum.inl (some (Sum.inl r₁.input_N)))) holds.

But this contradicts no_wrap₂_corr_sum_inl_inl.

Use corresponding_strings_nth_le or List.Forall₂ indexed access to get the element at position p.
-/
private lemma rule_in_first_half
    {x : List (symbol T N₁)} {y : List (symbol T N₂)}
    {a u v : List (nst T N₁ N₂)}
    {r₁ : grule T N₁}
    (ih_concat : corresponding_strings
      (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a)
    (bef : a = u ++ (List.map (wrap_symbol₁ N₂) r₁.input_L) ++
               [symbol.nonterminal (Sum.inl (some (Sum.inl r₁.input_N)))] ++
               (List.map (wrap_symbol₁ N₂) r₁.input_R) ++ v) :
    u.length + r₁.input_L.length + 1 + r₁.input_R.length ≤ x.length := by
      contrapose! ih_concat; simp_all +decide [ corresponding_strings ] ;
      intro h; have := List.forall₂_iff_get.mp h; simp_all +decide [ List.getElem_append ] ;
      have := this.2 ( u.length + r₁.input_L.length ) ( by linarith ) ( by linarith ) ; simp_all +decide [ add_assoc ] ;
      split_ifs at this <;> simp_all +decide [ add_comm, add_left_comm, add_assoc ] ;
      · cases h : x[r₁.input_L.length + u.length] <;> simp_all +decide [ corresponding_symbols ];
        · cases this;
        · cases this;
          have := this.2 ( r₁.input_L.length + u.length + r₁.input_R.length ) ( by linarith ) ( by linarith ) ; simp_all +decide [ add_assoc ] ;
          grind +suggestions;
      · exact no_wrap₂_corr_sum_inl_inl this

/-
PROBLEM
Symmetric: rule from g₂ fits in the last y.length elements (i.e., starts at or after x.length)

PROVIDED SOLUTION
By contradiction. Assume x.length > u.length. Then position p = u.length + r₂.input_L.length (the nonterminal position) satisfies p ≤ u.length + r₂.input_L.length.

Actually, even just the nonterminal at position u.length + r₂.input_L.length: from bef, a[u.length + r₂.input_L.length] = symbol.nonterminal (Sum.inl (some (Sum.inr r₂.input_N))).

If this position < x.length, then in the reference list (map wrap₁ x ++ map wrap₂ y), the element at this position is (map wrap₁ x)[u.length + r₂.input_L.length] = wrap_symbol₁ N₂ (x[...]).

So corresponding_symbols (wrap_symbol₁ N₂ (...)) (nt (Sum.inl (some (Sum.inr r₂.input_N)))) holds.

But this contradicts no_wrap₁_corr_sum_inl_inr.

Actually the argument needs more care: we need u.length + r₂.input_L.length < x.length. Since x.length > u.length and r₂.input_L.length ≥ 0, we need x.length > u.length but u.length + r₂.input_L.length could be ≥ x.length. Let me fix: if u.length < x.length, then at position u.length in a, a[u.length] is the first element of r₂.input_L (if nonempty) or the nonterminal (if input_L is empty). If r₂.input_L is empty, the nonterminal is at position u.length < x.length, and we use no_wrap₁_corr_sum_inl_inr as above. If r₂.input_L is nonempty, at position u.length we have (map wrap₂ r₂.input_L)[0] = wrap_symbol₂ N₁ (r₂.input_L[0]), which is a wrap₂ output. The reference at position u.length < x.length is (map wrap₁ x)[u.length] = wrap_symbol₁ N₂ (x[u.length]). So corresponding_symbols (wrap_symbol₁ N₂ (...)) (wrap_symbol₂ N₁ (...)), which contradicts corresponding_symbols_never₂ (noting the order: corresponding_symbols (wrap₁ ...) (wrap₂ ...)). Wait, corresponding_symbols_never₂ says ¬ corresponding_symbols (wrap₂ ...) (wrap₁ ...). The order matters. Let me check: ih_concat says Forall₂ corresponding_symbols ref a, so corresponding_symbols (ref[i]) (a[i]). At position i = u.length, ref[i] = wrap₁ x[u.length], a[i] = wrap₂ r₂.input_L[0]. So corresponding_symbols (wrap₁ ...) (wrap₂ ...), which is ¬ by corresponding_symbols_never₁. Use that.
-/
private lemma rule_in_second_half
    {x : List (symbol T N₁)} {y : List (symbol T N₂)}
    {a u v : List (nst T N₁ N₂)}
    {r₂ : grule T N₂}
    (ih_concat : corresponding_strings
      (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a)
    (bef : a = u ++ (List.map (wrap_symbol₂ N₁) r₂.input_L) ++
               [symbol.nonterminal (Sum.inl (some (Sum.inr r₂.input_N)))] ++
               (List.map (wrap_symbol₂ N₁) r₂.input_R) ++ v) :
    x.length ≤ u.length := by
      have h_p_le_x : u.length < x.length → False := by
        intro h_lt_x
        have h_p_le_x : corresponding_symbols (wrap_symbol₁ N₂ (x.get ⟨u.length, h_lt_x⟩)) (a.get ⟨u.length, by
          simp +arith +decide [ bef ]⟩) := by
          have := List.forall₂_iff_get.mp ih_concat;
          grind
        generalize_proofs at *;
        by_cases h : r₂.input_L.length = 0 <;> simp_all +decide [ List.getElem_append ];
        · exact no_wrap₁_corr_sum_inl_inr h_p_le_x |> fun h => by tauto;
        · split_ifs at h_p_le_x <;> simp_all +decide [ corresponding_symbols_never₁ ]
      exact le_of_not_gt h_p_le_x

/-
PROBLEM
Pure list fact: take of a concatenation u ++ L ++ [n] ++ R ++ v when the take length
exceeds u ++ L ++ [n] ++ R

PROVIDED SOLUTION
Since |u| + |L| + 1 + |R| ≤ m, taking m elements from u ++ L ++ [n] ++ R ++ v first takes all of u (|u| elements), then all of L (|L| elements), then [n] (1 element), then all of R (|R| elements), and then m - |u| - |L| - 1 - |R| elements from v. Use List.take_append_of_le_length repeatedly, or simp with List.take_append, List.length_append.
-/
private lemma take_of_append_five {α : Type} {u L : List α} {n : α} {R v : List α} {m : ℕ}
    (h_le : u.length + L.length + 1 + R.length ≤ m) :
    List.take m (u ++ L ++ [n] ++ R ++ v) =
      u ++ L ++ [n] ++ R ++ List.take (m - (u.length + L.length + 1 + R.length)) v := by
        rw [ List.take_append, List.take_append, List.take_append, List.take_append ] ; simp +arith +decide [ * ] ; ring;
        rw [ List.take_of_length_le, List.take_of_length_le, List.take_of_length_le ] <;> norm_num <;> omega;

/-
PROVIDED SOLUTION
Since |u| + |L| + 1 + |R| ≤ m ≤ |u| + |L| + 1 + |R| + |v|, dropping m elements from u ++ L ++ [n] ++ R ++ v first drops all of u, L, [n], R, then drops m - |u| - |L| - 1 - |R| elements from v. Use List.drop_append_of_le_length or omega/simp.
-/
private lemma drop_of_append_five {α : Type} {u L : List α} {n : α} {R v : List α} {m : ℕ}
    (h_le : u.length + L.length + 1 + R.length ≤ m)
    (h_le2 : m ≤ u.length + L.length + 1 + R.length + v.length) :
    List.drop m (u ++ L ++ [n] ++ R ++ v) =
      List.drop (m - (u.length + L.length + 1 + R.length)) v := by
        rw [ show m = 1 + u.length + L.length + R.length + ( m - ( 1 + u.length + L.length + R.length ) ) by rw [ add_tsub_cancel_of_le ] ; linarith ] ; simp +decide [ List.drop_append, add_comm, add_left_comm, add_assoc ] ; ring;
        rw [ List.drop_eq_nil_of_le, List.drop_eq_nil_of_le ] <;> simp +arith +decide

end helpers_for_induction_steps

section very_complicated

/-
PROVIDED SOLUTION
1. obtain ⟨r₁, hr₁_mem, rfl⟩ from List.mem_map.mp rin. simp only [wrap_grule₁] at bef aft.
2. have h_le := rule_in_first_half ih_concat bef.
3. set v₁ := take (x.length - (u.length + r₁.input_L.length + 1 + r₁.input_R.length)) v, v₂ := drop ... v.
4. Show take x.length a = u ++ map wrap₁ r₁.input_L ++ [nt (Sum.inl (some (Sum.inl r₁.input_N)))] ++ map wrap₁ r₁.input_R ++ v₁ using take_of_append_five on bef.
5. Show drop x.length a = v₂ using drop_of_append_five on bef.
6. Get h_corr_take from corresponding_strings_take and h_corr_drop from corresponding_strings_drop of ih_concat (using simp [List.take_left/drop_left]).
7. Get h_x_eq using filter_map_unwrap_of_corresponding_strings₁ on the take correspondence.
8. Simplify h_x_eq using filterMap_append, unwrap_wrap₁_string to get x = filterMap u ++ r₁.input_L ++ [nt r₁.input_N] ++ r₁.input_R ++ filterMap v₁.
9. Witness x' = filterMap unwrap₁ u ++ r₁.output_string ++ filterMap unwrap₁ v₁.
10. grammar_transforms via ⟨r₁, hr₁_mem, filterMap u, filterMap v₁, h_x_decomp, rfl⟩.
11. Correspondence: rw [aft, v=v₁++v₂], simp [List.map_append, List.append_assoc], then apply corresponding_strings_append 3 times for 4 parts:
   (a) map wrap₁ (filterMap unwrap₁ u) ~ u: use corresponding_string_after_wrap_unwrap_self₁ with witness from corresponding_strings_take u.length on the take-correspondence (need List.map_take to convert)
   (b) map wrap₁ r₁.output_string ~ map wrap₁ r₁.output_string: corresponding_strings_self
   (c) map wrap₁ (filterMap unwrap₁ v₁) ~ v₁: corresponding_string_after_wrap_unwrap_self₁ with witness from corresponding_strings_drop plen on take-correspondence (need List.map_drop to convert)
   (d) map wrap₂ y ~ v₂: from corresponding_strings_drop of ih_concat
-/
set_option maxHeartbeats 800000 in
private lemma induction_step_for_lifted_rule_from_g₁
    {g₁ g₂ : grammar T}
    {a b u v : List (nst T g₁.nt g₂.nt)}
    {x : List (symbol T g₁.nt)}
    {y : List (symbol T g₂.nt)}
    {r : grule T (nnn T g₁.nt g₂.nt)}
    (rin : r ∈ List.map (wrap_grule₁ g₂.nt) g₁.rules)
    (bef : a = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v)
    (aft : b = u ++ r.output_string ++ v)
    (ih_x : grammar_derives g₁ [symbol.nonterminal g₁.initial] x)
    (ih_y : grammar_derives g₂ [symbol.nonterminal g₂.initial] y)
    (ih_concat :
      corresponding_strings
        (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y)
        a) :
  ∃ (x' : List (symbol T g₁.nt)),
      (grammar_derives g₁ [symbol.nonterminal g₁.initial] x') ∧
      (grammar_derives g₂ [symbol.nonterminal g₂.initial] y) ∧
      (corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x' ++ List.map (wrap_symbol₂ g₁.nt) y) b) :=
by
  by_contra h_contra';
  obtain ⟨ r₁, hr₁_mem, rfl ⟩ := List.mem_map.mp rin;
  -- Set `v₁` and `v₂` as described.
  set v₁ := List.take (x.length - (u.length + r₁.input_L.length + 1 + r₁.input_R.length)) v
  set v₂ := List.drop (x.length - (u.length + r₁.input_L.length + 1 + r₁.input_R.length)) v;
  -- Show that the take of the list up to x.length is equal to the concatenation of the take of the first part and the take of the second part.
  have h_take : List.take x.length a = u ++ (List.map (wrap_symbol₁ g₂.nt) r₁.input_L) ++ [symbol.nonterminal (Sum.inl (some (Sum.inl r₁.input_N)))] ++ (List.map (wrap_symbol₁ g₂.nt) r₁.input_R) ++ v₁ := by
    have h_le : u.length + r₁.input_L.length + 1 + r₁.input_R.length ≤ x.length := by
      apply rule_in_first_half ih_concat bef;
    rw [bef];
    rw [take_of_append_five];
    · unfold wrap_grule₁; aesop;
    · unfold wrap_grule₁; aesop;
  -- Show that the drop of the list up to x.length is equal to the concatenation of the drop of the first part and the drop of the second part.
  have h_drop : List.drop x.length a = v₂ := by
    convert drop_of_append_five _ _ using 1;
    congr! 1;
    · unfold wrap_grule₁; aesop;
    · convert rule_in_first_half ih_concat bef using 1;
      unfold wrap_grule₁; simp +arith +decide;
    · have := corresponding_strings_length ih_concat; simp_all +decide ;
      lia;
  -- Show that the corresponding strings of the take and drop parts hold.
  have h_take_corr : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x) (List.take x.length a) := by
    have h_take_corr : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a := by
      exact ih_concat;
    have := corresponding_strings_take x.length h_take_corr; aesop;
  have h_drop_corr : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) y) (List.drop x.length a) := by
    convert corresponding_strings_drop x.length ih_concat using 1;
    simp +decide [ List.drop_append ];
  -- Show that the corresponding strings of the take and drop parts hold for the new list b.
  have h_new_corr : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) (List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) u ++ r₁.output_string ++ List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) v₁) ++ List.map (wrap_symbol₂ g₁.nt) y) b := by
    have h_new_corr : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) (List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) u) ++ List.map (wrap_symbol₁ g₂.nt) r₁.output_string ++ List.map (wrap_symbol₁ g₂.nt) (List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) v₁)) (u ++ (wrap_grule₁ g₂.nt r₁).output_string ++ v₁) := by
      have h_new_corr : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) (List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) u)) u := by
        apply corresponding_string_after_wrap_unwrap_self₁
        generalize_proofs at *; (
        use List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) (List.take x.length a) |> fun z => z.take (u.length) |> fun z => z; (
        have h_filterMap_take : List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) (List.take x.length a) = x := by
          exact x_from_take_filterMap ih_concat
        generalize_proofs at *; (
        have := corresponding_strings_take u.length h_take_corr; simp_all +decide [ List.take_append ] ;));)
      have h_new_corr' : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) (List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) v₁)) v₁ := by
        have h_new_corr' : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x) (List.take x.length a) := by
          exact h_take_corr;
        have := corresponding_strings_split ( u.length + r₁.input_L.length + 1 + r₁.input_R.length ) h_new_corr'; simp_all +decide [ List.take_append, List.drop_append ] ;
        apply corresponding_string_after_wrap_unwrap_self₁; exact (by
          have := this.right; simp_all +decide [ List.drop_append, List.take_append ] ;
          simp_all +decide [ List.drop_eq_nil_of_le, add_assoc, add_tsub_assoc_of_le ];
          use List.drop (u.length + (r₁.input_L.length + (1 + r₁.input_R.length))) x; simp_all +decide [ List.drop_append, List.take_append ] ;
          convert this using 1 ; simp +decide [ add_comm, add_left_comm, add_assoc ] ;
        )
      have h_new_corr'' : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) r₁.output_string) (wrap_grule₁ g₂.nt r₁).output_string := by
        exact corresponding_strings_self
      exact corresponding_strings_append (corresponding_strings_append h_new_corr h_new_corr'') h_new_corr' |> fun h => by simpa [List.map_append] using h;
    convert corresponding_strings_append h_new_corr ( h_drop_corr ) using 1 ; simp +decide [ aft ] ; ring!;
    rw [ aft, h_drop ] ; simp +decide [ List.append_assoc ] ; ring!;
    rw [ show x.length - ( 1 + u.length + r₁.input_L.length + r₁.input_R.length ) = x.length - ( u.length + r₁.input_L.length + 1 + r₁.input_R.length ) by ring, List.take_append_drop ];
  refine h_contra' ⟨ List.filterMap unwrap_symbol₁ u ++ r₁.output_string ++ List.filterMap unwrap_symbol₁ v₁, ?_, ih_y, h_new_corr ⟩;
  have h_x_eq : x = List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) u ++ r₁.input_L ++ [symbol.nonterminal r₁.input_N] ++ r₁.input_R ++ List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) v₁ := by
    have h_x_eq : List.filterMap (@unwrap_symbol₁ T g₁.nt g₂.nt) (List.take x.length a) = x := by
      apply x_from_take_filterMap; assumption;
    rw [ ← h_x_eq, h_take, List.filterMap_append, List.filterMap_append, List.filterMap_append, List.filterMap_append ];
    simp +decide [ unwrap_wrap₁_string ];
    rw [ show unwrap_symbol₁ ∘ wrap_symbol₁ g₂.nt = Option.some from funext fun x => ?_ ] ; simp +decide [ List.filterMap ] ;
    · rfl;
    · cases x <;> rfl;
  rw [h_x_eq] at ih_x;
  exact grammar_deri_of_deri_tran ih_x ( by exact ⟨ r₁, hr₁_mem, List.filterMap unwrap_symbol₁ u, List.filterMap unwrap_symbol₁ v₁, rfl, rfl ⟩ )

/-
PROVIDED SOLUTION
Mirror of `induction_step_for_lifted_rule_from_g₁` (proved just above), with g₁↔g₂ swapped. Use `by_contra h_contra'`.

1. `obtain ⟨r₂, hr₂_mem, rfl⟩ := List.mem_map.mp rin` to get the original g₂ rule.
2. `rule_in_second_half ih_concat bef` gives `h_le : x.length ≤ u.length`.
3. Set `u₁ := List.take x.length u`, `u₂ := List.drop x.length u`.
4. Show `h_take : List.take x.length a = u₁` by rewriting bef and using that x.length ≤ u.length (so take x.length (u ++ ...) = take x.length u = u₁). Use `List.take_append_of_le_length` or just simp.
5. Show `h_drop : List.drop x.length a = u₂ ++ (List.map (wrap_symbol₂ g₁.nt) r₂.input_L) ++ [symbol.nonterminal (Sum.inl (some (Sum.inr r₂.input_N)))] ++ (List.map (wrap_symbol₂ g₁.nt) r₂.input_R) ++ v` by similar reasoning (drop x.length (u ++ ...) = drop x.length u ++ ... since x.length ≤ u.length).
6. Get `h_take_corr` from `corresponding_strings_take x.length ih_concat` and simplify with `List.take_left`.
7. Get `h_drop_corr` from `corresponding_strings_drop x.length ih_concat` and simplify with `List.drop_left`.
8. Get `h_y_eq` using `y_from_drop_filterMap ih_concat` giving `y = filterMap unwrap₂ (drop x.length a)`. Then rewrite h_drop into h_y_eq: `y = filterMap unwrap₂ u₂ ++ r₂.input_L ++ [nt r₂.input_N] ++ r₂.input_R ++ filterMap unwrap₂ v` (using filterMap_append, unwrap_wrap₂_string, and the identity `unwrap_symbol₂ ∘ wrap_symbol₂ g₁.nt = Option.some`).
9. Witness `y' = filterMap unwrap₂ u₂ ++ r₂.output_string ++ filterMap unwrap₂ v`.
10. Show grammar_transforms via `⟨r₂, hr₂_mem, filterMap unwrap₂ u₂, filterMap unwrap₂ v, h_y_eq, rfl⟩`.
11. Show new correspondence for b using corresponding_strings_append:
   (a) map wrap₁ x ~ u₁: from h_take_corr
   (b) map wrap₂ (filterMap unwrap₂ u₂) ~ u₂: corresponding_string_after_wrap_unwrap_self₂
   (c) map wrap₂ r₂.output_string ~ (wrap_grule₂ g₁.nt r₂).output_string: corresponding_strings_self
   (d) map wrap₂ (filterMap unwrap₂ v) ~ v: corresponding_string_after_wrap_unwrap_self₂
   Then b = u₁ ++ u₂ ++ wrap₂ r₂.output_string ++ v by rewriting aft and u = u₁ ++ u₂.
-/
set_option maxHeartbeats 800000 in
private lemma induction_step_for_lifted_rule_from_g₂
    {g₁ g₂ : grammar T}
    {a b u v : List (nst T g₁.nt g₂.nt)}
    {x : List (symbol T g₁.nt)}
    {y : List (symbol T g₂.nt)}
    {r : grule T (nnn T g₁.nt g₂.nt)}
    (rin : r ∈ List.map (wrap_grule₂ g₁.nt) g₂.rules)
    (bef : a = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v)
    (aft : b = u ++ r.output_string ++ v)
    (ih_x : grammar_derives g₁ [symbol.nonterminal g₁.initial] x)
    (ih_y : grammar_derives g₂ [symbol.nonterminal g₂.initial] y)
    (ih_concat :
      corresponding_strings
        (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y)
        a) :
  ∃ (y' : List (symbol T g₂.nt)),
      (grammar_derives g₁ [symbol.nonterminal g₁.initial] x) ∧
      (grammar_derives g₂ [symbol.nonterminal g₂.initial] y') ∧
      (corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y') b) :=
by
  obtain ⟨r₂, hr₂_mem, rfl⟩ := List.mem_map.mp rin;
  obtain ⟨u₁, u₂, hu₁, hu₂⟩ : ∃ u₁ u₂ : List (nst T g₁.nt g₂.nt), u = u₁ ++ u₂ ∧ u₁.length = x.length := by
    use List.take x.length u, List.drop x.length u;
    have := rule_in_second_half ih_concat bef; aesop;
  -- By definition of `wrap_grule₂`, we know that `r₂` is a rule in `g₂`.
  use (List.filterMap (@unwrap_symbol₂ T g₁.nt g₂.nt) u₂) ++ r₂.output_string ++ (List.filterMap (@unwrap_symbol₂ T g₁.nt g₂.nt) v);
  refine' ⟨ ih_x, _, _ ⟩;
  · have h_y_eq : y = List.filterMap (@unwrap_symbol₂ T g₁.nt g₂.nt) u₂ ++ r₂.input_L ++ [symbol.nonterminal r₂.input_N] ++ r₂.input_R ++ List.filterMap (@unwrap_symbol₂ T g₁.nt g₂.nt) v := by
      have h_y_eq : y = List.filterMap (@unwrap_symbol₂ T g₁.nt g₂.nt) (List.drop x.length a) := by
        apply Eq.symm; exact (by
        apply y_from_drop_filterMap ih_concat);
      rw [h_y_eq, bef, hu₁];
      simp +decide [ hu₂, List.drop_append ];
      unfold wrap_grule₂; simp +decide [ List.filterMap_append ] ;
      simp +decide [ Function.comp, List.filterMap_cons ];
      rw [ show unwrap_symbol₂ ( symbol.nonterminal ( Sum.inl ( some ( Sum.inr r₂.input_N ) ) ) ) = some ( symbol.nonterminal r₂.input_N ) from rfl ] ; simp +decide [ Function.comp, List.filterMap_append ] ;
      rw [ show unwrap_symbol₂ ∘ wrap_symbol₂ g₁.nt = Option.some from funext fun x => by cases x <;> rfl ] ; simp +decide [ List.filterMap_map ] ;
    convert grammar_deri_of_deri_tran ih_y _ using 1;
    exact ⟨ r₂, hr₂_mem, List.filterMap unwrap_symbol₂ u₂, List.filterMap unwrap_symbol₂ v, by aesop ⟩;
  · simp_all +decide [ corresponding_strings_append ];
    have h_take : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x) u₁ := by
      have := corresponding_strings_take x.length ih_concat; aesop;
    have h_drop : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) (List.filterMap unwrap_symbol₂ u₂)) u₂ := by
      apply corresponding_string_after_wrap_unwrap_self₂;
      have h_drop : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) y) (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v))) := by
        have h_drop : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) (u₁ ++ (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v)))) → corresponding_strings (List.map (wrap_symbol₂ g₁.nt) y) (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v))) := by
          intro h_drop
          have h_drop : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) y) (List.drop x.length (u₁ ++ (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v))))) := by
            convert corresponding_strings_drop x.length h_drop using 1
            generalize_proofs at *; (
            simp +decide [ hu₂ ])
          generalize_proofs at *; (
          convert h_drop using 1 ; simp +decide [ hu₂ ]);
        exact h_drop ‹_›;
      have := corresponding_strings_take ( List.length u₂ ) h_drop; simp_all +decide [ corresponding_strings ] ;
      use List.take u₂.length y;
      rw [ List.forall₂_iff_get ] at *;
      grind +splitIndPred
    have h_drop' : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) (List.filterMap unwrap_symbol₂ v)) v := by
      apply corresponding_string_after_wrap_unwrap_self₂;
      have h_drop : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) y) (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v))) := by
        convert corresponding_strings_drop x.length ih_concat using 1;
        · simp +decide [ hu₂ ];
        · simp +decide [ hu₂, List.drop_append ];
      have h_drop : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) y) (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v))) → corresponding_strings (List.map (wrap_symbol₂ g₁.nt) (List.drop (u₂.length + ((wrap_grule₂ g₁.nt r₂).input_L.length + 1 + ((wrap_grule₂ g₁.nt r₂).input_R.length))) y)) v := by
        intro h_drop
        have h_drop' : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) (List.drop (u₂.length + ((wrap_grule₂ g₁.nt r₂).input_L.length + 1 + ((wrap_grule₂ g₁.nt r₂).input_R.length))) y)) (List.drop (u₂.length + ((wrap_grule₂ g₁.nt r₂).input_L.length + 1 + ((wrap_grule₂ g₁.nt r₂).input_R.length))) (u₂ ++ ((wrap_grule₂ g₁.nt r₂).input_L ++ symbol.nonterminal (wrap_grule₂ g₁.nt r₂).input_N :: ((wrap_grule₂ g₁.nt r₂).input_R ++ v)))) := by
          convert corresponding_strings_drop _ h_drop using 1;
          rw [ List.map_drop ];
        convert h_drop' using 1;
        simp +decide [ add_comm, add_left_comm, add_assoc, List.drop_eq_nil_of_le ];
      exact ⟨ _, h_drop ‹_› ⟩
    have h_drop'' : corresponding_strings (List.map (wrap_symbol₂ g₁.nt) r₂.output_string) ((wrap_grule₂ g₁.nt r₂).output_string) := by
      exact corresponding_strings_self;
    exact corresponding_strings_append h_take ( corresponding_strings_append h_drop ( corresponding_strings_append h_drop'' h_drop' ) )

/-
PROVIDED SOLUTION
Cases on s: terminal t gives nt (Sum.inr (Sum.inl t)) ≠ nt (Sum.inl none), nonterminal n gives nt (Sum.inl (some (Sum.inl n))) ≠ nt (Sum.inl none). Both are straightforward by definition.
-/
private lemma no_none_in_wrapped₁ {N₁ N₂ : Type} (s : symbol T N₁) :
    wrap_symbol₁ N₂ s ≠ symbol.nonterminal (Sum.inl none) := by
  cases s <;> simp +decide [ * ];
  · exact fun h => by cases h;
  · grind +locals

/-
PROVIDED SOLUTION
Cases on s: terminal t gives nt (Sum.inr (Sum.inr t)) ≠ nt (Sum.inl none), nonterminal n gives nt (Sum.inl (some (Sum.inr n))) ≠ nt (Sum.inl none). Both are straightforward.
-/
private lemma no_none_in_wrapped₂ {N₁ N₂ : Type} (s : symbol T N₂) :
    wrap_symbol₂ N₁ s ≠ symbol.nonterminal (Sum.inl none) := by
  cases s <;> simp_all +decide [ wrap_symbol₂ ];
  grind +ring

/-
PROVIDED SOLUTION
The rule replaces nt (Sum.inr (Sum.inl t)) with terminal t in the string, at position u.length. corresponding_symbols maps (Sum.inr (Sum.inl t)) to terminal t' when t = t', so replacing one with the other preserves the correspondence.

Use corresponding_strings = List.Forall₂ corresponding_symbols. From ih_concat and bef, we have Forall₂ relation on a. For b, the only change is at position u.length where nt (Sum.inr (Sum.inl t)) becomes terminal t. By definition of corresponding_symbols, corresponding_symbols (nt (Sum.inr (Sum.inl t))) (terminal t) holds (since t = t), so the correspondence is preserved.

Concretely: split a at position u.length using corresponding_strings_take and corresponding_strings_drop. In bef, the element at position u.length is nt (Sum.inr (Sum.inl t)). In the reference string (map wrap₁ x ++ map wrap₂ y), the element at that position has corresponding_symbols with nt (Sum.inr (Sum.inl t)), and by definition of corresponding_symbols, it also has corresponding_symbols with terminal t. Then reassemble using corresponding_strings_append.
-/
private lemma induction_step_for_terminal_rule₁
    {g₁ g₂ : grammar T}
    {a b u v : List (nst T g₁.nt g₂.nt)}
    {x : List (symbol T g₁.nt)}
    {y : List (symbol T g₂.nt)}
    {t : T}
    (ht : t ∈ all_used_terminals g₁)
    (bef : a = u ++ [symbol.nonterminal (Sum.inr (Sum.inl t))] ++ v)
    (aft : b = u ++ [symbol.terminal t] ++ v)
    (ih_concat : corresponding_strings
        (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a) :
  corresponding_strings
    (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) b := by
  have unfold_ih_concat : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) (u ++ [symbol.nonterminal (Sum.inr (Sum.inl t))] ++ v) := by
    aesop;
  have h_split : u.length < (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y).length := by
    have := corresponding_strings_length unfold_ih_concat; aesop;
  obtain ⟨l₁, l₂, hl₁, hl₂⟩ : ∃ l₁ l₂, List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y = l₁ ++ l₂ ∧ List.length l₁ = u.length ∧ corresponding_strings l₁ u ∧ corresponding_strings l₂ ([symbol.nonterminal (Sum.inr (Sum.inl t))] ++ v) := by
    obtain ⟨l₁, l₂, hl₁, hl₂⟩ : ∃ l₁ l₂, List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y = l₁ ++ l₂ ∧ List.length l₁ = u.length ∧ corresponding_strings l₁ (u ++ [symbol.nonterminal (Sum.inr (Sum.inl t))] ++ v |>.take u.length) := by
      use List.take u.length (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y), List.drop u.length (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y);
      exact ⟨ by rw [ List.take_append_drop ], by rw [ List.length_take, min_eq_left h_split.le ], by exact corresponding_strings_take _ unfold_ih_concat ⟩;
    simp_all +decide [ List.take_append ];
    exact ⟨ l₁, l₂, rfl, hl₂.1, hl₂.2, by simpa [ hl₂.1 ] using corresponding_strings_drop ( u.length ) ih_concat ⟩;
  have h_replace : corresponding_strings l₂ ([symbol.terminal t] ++ v) := by
    rcases l₂ with ( _ | ⟨ s, l₂ ⟩ ) <;> simp_all +decide [ corresponding_strings ];
    unfold corresponding_symbols at * ; aesop;
  convert corresponding_strings_append hl₂.2.1 h_replace using 1 ; aesop

/-
PROVIDED SOLUTION
Exactly symmetric to induction_step_for_terminal_rule₁ (proved just above). The rule replaces nt (Sum.inr (Sum.inr t)) with terminal t. By definition of corresponding_symbols, corresponding_symbols (nt (Sum.inr (Sum.inr t))) (terminal t) holds when t = t. Same approach: split the correspondence at position u.length, show the head element correspondence is preserved (Sum.inr (Sum.inr t) ↔ terminal t), reassemble with corresponding_strings_append.
-/
private lemma induction_step_for_terminal_rule₂
    {g₁ g₂ : grammar T}
    {a b u v : List (nst T g₁.nt g₂.nt)}
    {x : List (symbol T g₁.nt)}
    {y : List (symbol T g₂.nt)}
    {t : T}
    (ht : t ∈ all_used_terminals g₂)
    (bef : a = u ++ [symbol.nonterminal (Sum.inr (Sum.inr t))] ++ v)
    (aft : b = u ++ [symbol.terminal t] ++ v)
    (ih_concat : corresponding_strings
        (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a) :
  corresponding_strings
    (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) b := by
  rw [bef] at ih_concat
  unfold corresponding_strings at *;
  rw [ List.forall₂_iff_get ] at *;
  simp_all +decide [ List.getElem_append ];
  intro i hi; specialize ih_concat; rcases ih_concat with ⟨ h₁, h₂ ⟩ ; rcases lt_trichotomy i u.length with hi' | rfl | hi' <;> simp_all +decide [ Nat.lt_succ_iff ] ;
  · simpa [ hi' ] using h₂ i ( by linarith );
  · specialize h₂ u.length ( by linarith ) ; simp_all +decide [ List.getElem_append ] ;
    unfold corresponding_symbols at * ; aesop;
  · grind +splitIndPred

/-
PROVIDED SOLUTION
Induction on the derivation `ass` using `induction ass`.

Base case (refl): x = [nt g₁.initial], y = [nt g₂.initial], grammar_deri_self for both, and corresponding_strings holds by corresponding_strings_self since map wrap₁ [nt g₁.initial] ++ map wrap₂ [nt g₂.initial] equals the starting string.

Inductive case (tail): We have v →* w₁ (by ih) and w₁ →₁ w (step). By ih, get x, y with the invariant for w₁. Extract the rule r from the step: ⟨r, r_in, u, v', bef, aft⟩.

Case split on r_in. The rules of big_grammar are:
- Initial rule (head): r.input_N = Sum.inl none, r.input_L = [], r.input_R = []. This is impossible because bef says w₁ contains [nt (Sum.inl none)], but from the invariant all symbols in w₁ are wrapped (corresponding to wrap₁ or wrap₂ outputs), and neither produces Sum.inl none (by no_none_in_wrapped₁/₂). Show this by: the reference string (map wrap₁ x ++ map wrap₂ y) has length = w₁.length (from corresponding_strings_length). At position u.length, w₁[u.length] = nt (Sum.inl none). The reference at that position is either wrap₁ (x[...]) or wrap₂ (y[...]). Use corresponding_strings_nth_le to get corresponding_symbols (ref[u.length]) (nt (Sum.inl none)). But ref[u.length] is some wrap₁ or wrap₂ output, and none of them can have corresponding_symbols with nt (Sum.inl none). More directly: from List.Forall₂, every element of w₁ corresponds to an element of the reference string. Show that nt (Sum.inl none) cannot correspond to any wrap₁ or wrap₂ symbol.

- Rules from g₁ (in map wrap_grule₁): use induction_step_for_lifted_rule_from_g₁ to get new x', keep y.
- Rules from g₂ (in map wrap_grule₂): use induction_step_for_lifted_rule_from_g₂ to get new y', keep x.
- Terminal rules from g₁ (in rules_for_terminals₁): use induction_step_for_terminal_rule₁, keep same x, y.
- Terminal rules from g₂ (in rules_for_terminals₂): use induction_step_for_terminal_rule₂, keep same x, y.

For the membership case analysis: `List.mem_cons` gives initial rule ∨ rest. Then `List.mem_append` splits rest into (g₁_rules ++ g₂_rules) and (terminal_rules₁ ++ terminal_rules₂), etc.
-/
set_option maxHeartbeats 800000 in
private lemma big_induction
    {g₁ g₂ : grammar T}
    {w : List (nst T g₁.nt g₂.nt)}
    (ass :
      grammar_derives (big_grammar g₁ g₂)
        [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))),
         symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))]
        w) :
  ∃ x : List (symbol T g₁.nt),
  ∃ y : List (symbol T g₂.nt),
      (grammar_derives g₁ [symbol.nonterminal g₁.initial] x) ∧
      (grammar_derives g₂ [symbol.nonterminal g₂.initial] y) ∧
      (corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) w) :=
by
  have h_ind : ∀ {w : List (nst T g₁.nt g₂.nt)}, grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))), symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))] w →
    ∃ x y : List (symbol T g₁.nt), ∃ y' : List (symbol T g₂.nt),
      (grammar_derives g₁ [symbol.nonterminal g₁.initial] x ∧
        grammar_derives g₂ [symbol.nonterminal g₂.initial] y' ∧
          corresponding_strings
            (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y' : List (nst T g₁.nt g₂.nt))
            w) := by
              intros w hw; induction' hw with w₁ w₂ hw₁ hw₂ ih₁ ih₂; simp_all +decide [ List.map_append ] ;
              · exact ⟨ [ symbol.nonterminal g₁.initial ], by tauto, [ symbol.nonterminal g₂.initial ], by tauto, by tauto ⟩;
              · obtain ⟨ x, y, y', hx, hy, hxy ⟩ := ih₁
                obtain ⟨ r, hr, u, v, bef, aft ⟩ := hw₂
                by_cases hr₁ : r ∈ List.map (wrap_grule₁ g₂.nt) g₁.rules ∨ r ∈ List.map (wrap_grule₂ g₁.nt) g₂.rules ∨ r ∈ rules_for_terminals₁ g₂.nt g₁ ∨ r ∈ rules_for_terminals₂ g₁.nt g₂ <;> simp_all +decide [ List.mem_append, List.mem_map ];
                · rcases hr₁ with ( ⟨ a, ha, rfl ⟩ | ⟨ a, ha, rfl ⟩ | hr₁ | hr₁ ) <;> simp_all +decide [ big_grammar ] ;
                  · have := induction_step_for_lifted_rule_from_g₁ ( show wrap_grule₁ g₂.nt a ∈ List.map ( wrap_grule₁ g₂.nt ) g₁.rules from List.mem_map.mpr ⟨ a, ha, rfl ⟩ ) ( by aesop ) ( by aesop ) hx hy hxy; aesop;
                  · obtain ⟨ y'', hy'', hxy'' ⟩ := induction_step_for_lifted_rule_from_g₂ ( List.mem_map.mpr ⟨ a, ha, rfl ⟩ ) ( by aesop ) ( by aesop ) hx hy hxy; use x, hx, y''; aesop;
                  · unfold rules_for_terminals₁ at hr₁; simp_all +decide [ List.mem_map ] ;
                    obtain ⟨ a, ha, rfl ⟩ := hr₁; exact ⟨ x, hx, y', hy, by simpa using induction_step_for_terminal_rule₁ ha ( by aesop ) ( by aesop ) hxy ⟩ ;
                  · unfold rules_for_terminals₂ at hr₁; simp_all +decide [ List.mem_map ] ;
                    obtain ⟨ a, ha, rfl ⟩ := hr₁; exact ⟨ x, hx, y', hy, by simpa using induction_step_for_terminal_rule₂ ha ( by aesop ) ( by aesop ) hxy ⟩ ;
                · unfold big_grammar at hr; simp_all +decide [ List.mem_append, List.mem_map ] ;
                  rcases hr with ( rfl | ⟨ a, ha, rfl ⟩ | ⟨ a, ha, rfl ⟩ ) <;> simp_all +decide [ wrap_grule₁, wrap_grule₂ ];
                  · have := hxy; ( have := List.forall₂_iff_get.mp this; simp_all +decide [ List.get ] ; );
                    have := this.2 ( u.length ) ( by linarith ) ( by linarith ) ; simp_all +decide [ List.getElem_append ] ;
                    split_ifs at this <;> simp_all +decide [ wrap_symbol₁, wrap_symbol₂ ] ;
                    · cases h : x[u.length] <;> simp_all +decide [ corresponding_symbols ];
                    · cases h : y'[u.length - x.length] <;> simp_all +decide [ corresponding_symbols ];
                  · exact False.elim <| hr₁.1 a ha rfl rfl rfl rfl;
                  · exact False.elim <| hr₁.2.1 a ha rfl rfl rfl rfl;
  exact Exists.elim ( h_ind ass ) fun x hx => Exists.elim hx fun y hy => Exists.elim hy fun z hz => ⟨ x, z, hz.1, hz.2.1, hz.2.2 ⟩

/-
PROVIDED SOLUTION
1. Unfold grammar_language at ass to get: grammar_derives (big_grammar g₁ g₂) [nt (big_grammar g₁ g₂).initial] (map terminal w), where (big_grammar g₁ g₂).initial = Sum.inl none.

2. The first step of any derivation from [nt (Sum.inl none)] must use the initial rule, giving [nt (Sum.inl (some (Sum.inl g₁.initial))), nt (Sum.inl (some (Sum.inr g₂.initial)))]. Use first_transformation or show this directly.

3. Apply big_induction to the remaining derivation to get x, y with grammar_derives g₁ ... x, grammar_derives g₂ ... y, and corresponding_strings (map wrap₁ x ++ map wrap₂ y) (map terminal w).

4. Since the final string is all terminals (map terminal w), and corresponding_strings relates each wrapped symbol to the terminal, unwrap to get that x = map terminal w₁ and y = map terminal w₂ for some w₁, w₂ with w = w₁ ++ w₂.

5. Use x_from_take_filterMap and y_from_drop_filterMap, plus the fact that filterMap unwrap₁ (map terminal w) = w (since unwrap_symbol₁ (terminal t) = some (terminal t)) to extract w₁ and w₂.

6. Conclude w₁ ∈ grammar_language g₁ and w₂ ∈ grammar_language g₂, so w ∈ L(g₁) * L(g₂).

Actually, a cleaner approach:
- From ass, we get grammar_derives (big_grammar g₁ g₂) [nt initial] (map terminal w).
- The initial step gives grammar_transforms to [nt (Sum.inl (some (Sum.inl g₁.initial))), nt (Sum.inl (some (Sum.inr g₂.initial)))].
- We need to extract this. Use the fact that grammar_derives has either refl or tail cases. In the refl case, [nt initial] = map terminal w is impossible. In the tail case, the first step must use the initial rule (the only rule with input_N = Sum.inl none).
- Then apply big_induction to get x, y with the invariant.
- Since the final word is map terminal w, corresponding_strings (map wrap₁ x ++ map wrap₂ y) (map terminal w).
- For each position, corresponding_symbols (wrap_X s) (terminal t) implies t equals the terminal embedded in s, which means s was terminal t itself.
- So x = map terminal w₁, y = map terminal w₂ for appropriate w₁, w₂ with w = w₁ ++ w₂.

Actually simplest: extract the derivation from the initial state, show it goes through the two-symbol state, then apply big_induction. The result gives x, y plus correspondence with map terminal w. Use the correspondence to split w into w₁ ++ w₂ and conclude.
-/
set_option maxHeartbeats 800000 in
lemma in_concatenated_of_in_big
    {g₁ g₂ : grammar T}
    {w : List T}
    (ass : w ∈ grammar_language (big_grammar g₁ g₂)) :
  w ∈ grammar_language g₁ * grammar_language g₂ :=
by
  -- Apply `big_induction` to obtain the existence of `x` and `y`.
  obtain ⟨x, y, hx, hy, hxy⟩ : ∃ x y, grammar_derives g₁ [symbol.nonterminal g₁.initial] x ∧ grammar_derives g₂ [symbol.nonterminal g₂.initial] y ∧ corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) (List.map symbol.terminal w) := by
    -- Apply the big_induction lemma to the derivation from the big grammar's initial state to the map of terminals w, to obtain x and y.
    obtain ⟨w', hw', hw'_eq⟩ : ∃ w', grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))), symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))] w' ∧ w' = List.map (symbol.terminal) w := by
      obtain ⟨w', hw'⟩ : ∃ w', grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (big_grammar g₁ g₂).initial] w' ∧ w' = List.map (symbol.terminal) w := by
        exact ⟨ _, ass, rfl ⟩;
      have := hw'.left;
      obtain ⟨w'', hw''⟩ : ∃ w'', grammar_transforms (big_grammar g₁ g₂) [symbol.nonterminal (big_grammar g₁ g₂).initial] w'' ∧ grammar_derives (big_grammar g₁ g₂) w'' w' := by
        have h_induction_step : ∀ {u v : List (symbol T (big_grammar g₁ g₂).nt)}, grammar_derives (big_grammar g₁ g₂) u v → u ≠ v → ∃ w, grammar_transforms (big_grammar g₁ g₂) u w ∧ grammar_derives (big_grammar g₁ g₂) w v := by
          intros u v huv huv_ne;
          have := huv;
          cases this ; tauto;
          grind +suggestions;
        apply h_induction_step this;
        cases w <;> simp +decide [ hw'.2 ] at hw' ⊢;
      have h_initial_rule : ∀ r ∈ (big_grammar g₁ g₂).rules, r.input_N = (big_grammar g₁ g₂).initial → r.input_L = [] ∧ r.input_R = [] ∧ r.output_string = [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))), symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))] := by
        grind +locals;
      obtain ⟨r, hr⟩ := hw''.left;
      obtain ⟨ u, v, h₁, h₂ ⟩ := hr.2;
      rcases u with ( _ | ⟨ u, u ⟩ ) <;> simp +decide at h₁ ⊢;
      rcases r : r.input_L with ( _ | ⟨ a, l ⟩ ) <;> simp +decide [ r ] at h₁ ⊢;
      grind +ring;
    have := big_induction hw';
    grind;
  -- By definition of `grammar_language`, we know that there exist `w₁` and `w₂` such that `w = w₁ ++ w₂`, `x.map unwrap_symbol₁ = w₁`, and `y.map unwrap_symbol₂ = w₂`.
  obtain ⟨w₁, w₂, hw₁, hw₂, hw⟩ : ∃ w₁ w₂ : List T, w = w₁ ++ w₂ ∧ x = List.map symbol.terminal w₁ ∧ y = List.map symbol.terminal w₂ := by
    -- By definition of `corresponding_strings`, we know that `x.map unwrap_symbol₁` and `y.map unwrap_symbol₂` are lists of terminals.
    have hx_terminals : ∀ s ∈ x, ∃ t : T, s = symbol.terminal t := by
      intro s hs
      obtain ⟨t, ht⟩ : ∃ t : T, corresponding_symbols (wrap_symbol₁ g₂.nt s) (symbol.terminal t) := by
        obtain ⟨ i, hi ⟩ := List.mem_iff_get.mp hs;
        have := List.forall₂_iff_get.mp hxy;
        simp_all +decide [ Fin.add_def, Nat.mod_eq_of_lt ];
        exact ⟨ w[i], by simpa [ hi, List.getElem_append, i.2 ] using this.2 i ( by linarith [ Fin.is_lt i ] ) ( by linarith [ Fin.is_lt i ] ) ⟩;
      cases s <;> aesop
    have hy_terminals : ∀ s ∈ y, ∃ t : T, s = symbol.terminal t := by
      intro s hs; have := hxy; simp_all +decide [ corresponding_strings ] ;
      obtain ⟨ i, hi ⟩ := List.mem_iff_get.mp hs; specialize hxy; simp_all +decide [ List.forall₂_iff_get ] ;
      specialize hxy ; have := hxy.2 ( x.length + i ) ( by linarith [ Fin.is_lt i ] ) ( by linarith [ Fin.is_lt i ] ) ; simp_all +decide [ List.getElem_append ] ;
      cases s <;> tauto;
    -- Since `x` and `y` are lists of terminals, we can extract the lists of terminals `w₁` and `w₂` such that `x = List.map symbol.terminal w₁` and `y = List.map symbol.terminal w₂`.
    obtain ⟨w₁, hw₁⟩ : ∃ w₁ : List T, x = List.map symbol.terminal w₁ := by
      have hx_terminals : ∀ {l : List (symbol T g₁.nt)}, (∀ s ∈ l, ∃ t : T, s = symbol.terminal t) → ∃ w : List T, l = List.map symbol.terminal w := by
        intros l hl; induction' l with s l ih <;> simp_all +decide [ List.map ] ;
        rcases hl.1 with ⟨ t, rfl ⟩ ; obtain ⟨ w, rfl ⟩ := ih; exact ⟨ t :: w, by simp +decide ⟩ ;
      exact hx_terminals ‹_›
    obtain ⟨w₂, hw₂⟩ : ∃ w₂ : List T, y = List.map symbol.terminal w₂ := by
      have hy_terminals : ∀ {l : List (symbol T g₂.nt)}, (∀ s ∈ l, ∃ t : T, s = symbol.terminal t) → ∃ w : List T, l = List.map symbol.terminal w := by
        intros l hl; induction' l with s l ih <;> simp_all +decide [ List.map ] ;
        rcases hl.1 with ⟨ t, rfl ⟩ ; obtain ⟨ w, rfl ⟩ := ih; exact ⟨ t :: w, by simp +decide ⟩ ;
      generalize_proofs at *; (
      exact hy_terminals ‹_›)
    use w₁, w₂;
    have := hxy; simp_all +decide [ corresponding_strings ] ;
    have h_eq : ∀ {l₁ l₂ : List T} {l₃ : List T}, List.Forall₂ (fun a c => corresponding_symbols a (symbol.terminal c)) (List.map (wrap_symbol₁ g₂.nt ∘ symbol.terminal) l₁ ++ List.map (wrap_symbol₂ g₁.nt ∘ symbol.terminal) l₂) l₃ → l₃ = l₁ ++ l₂ := by
      intros l₁ l₂ l₃ h; induction' l₁ with a l₁ ih generalizing l₂ l₃ <;> induction' l₂ with b l₂ ih' generalizing l₃ <;> simp_all +decide [ List.Forall₂ ] ;
      · rcases l₃ with ( _ | ⟨ c, l₃ ⟩ ) <;> simp_all +decide [ List.Forall₂ ];
        exact ⟨ by cases h.1; tauto, ih' h.2 ⟩;
      · rcases l₃ with ( _ | ⟨ b, l₃ ⟩ ) <;> simp_all +decide [ List.Forall₂ ];
        exact ⟨ by cases h.1; tauto, by simpa using ih ( show List.Forall₂ ( fun a c => corresponding_symbols a ( symbol.terminal c ) ) ( List.map ( wrap_symbol₁ g₂.nt ∘ symbol.terminal ) l₁ ++ List.map ( wrap_symbol₂ g₁.nt ∘ symbol.terminal ) [ ] ) l₃ from by simpa using h.2 ) ⟩;
      · rcases l₃ with ( _ | ⟨ c, l₃ ⟩ ) <;> simp_all +decide [ List.Forall₂ ];
        cases h.1 ; aesop ( simp_config := { singlePass := true } ) ;
    exact h_eq ‹_› ▸ rfl;
  exact ⟨ w₁, by aesop, w₂, by aesop, by aesop ⟩

end very_complicated

end hard_direction

/-
PROBLEM
The class of recursively-enumerable languages is closed under concatenation.

PROVIDED SOLUTION
From the hypotheses, extract g₁ with grammar_language g₁ = L₁ and g₂ with grammar_language g₂ = L₂. Witness big_grammar g₁ g₂. Show grammar_language (big_grammar g₁ g₂) = L₁ * L₂ using Set.Subset.antisymm with the two directions:
- Forward: use in_concatenated_of_in_big (rewriting L₁ and L₂)
- Backward: use in_big_of_in_concatenated (rewriting L₁ and L₂)
-/
theorem RE_of_RE_c_RE (L₁ : Language T) (L₂ : Language T) :
  is_RE L₁  ∧  is_RE L₂   →   is_RE (L₁ * L₂)   :=
by
  intro h
  obtain ⟨g₁, hg₁⟩ := h.left
  obtain ⟨g₂, hg₂⟩ := h.right
  use big_grammar g₁ g₂
  ext w
  apply Iff.intro;
  · convert in_concatenated_of_in_big ; aesop;
    exact hg₂.symm;
  · convert in_big_of_in_concatenated using 1;
    rw [ ← hg₁, ← hg₂ ]

/-- The class of recursively enumerable languages is closed under concatenation. -/
theorem RE_closedUnderConcatenation : ClosedUnderConcatenation (α := T) is_RE :=
  fun L₁ L₂ h₁ h₂ => RE_of_RE_c_RE L₁ L₂ ⟨h₁, h₂⟩
