import Init

def OA_statement : Prop := ((fun (lcs : Nat → List Nat → List Nat → Nat) =>
∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
 (∃ common : List Nat, common.Sublist xs ∧ common.Sublist ys ∧ common.length = lcs fuel xs ys) ∧
 (∀ common : List Nat, common.Sublist xs → common.Sublist ys → common.length ≤ lcs fuel xs ys))
(fun fuel => Nat.rec (fun _ _ : List Nat => 0)
 (fun _ recur xs ys => match xs, ys with
 | [], _ => 0
 | _, [] => 0
 | x :: xt, y :: yt => if x = y then 1 + recur xt yt
   else max (recur xt ys) (recur xs yt)) fuel))

theorem OA_target : OA_statement :=
  by
    have tailSub : ∀ (c : Nat) (cs l : List Nat) (a : Nat), (c :: cs).Sublist (a :: l) → cs.Sublist l := by
      intro c cs l a h
      rcases List.sublist_cons_iff.mp h with h1 | ⟨r, hr, h2⟩
      · exact List.Sublist.trans (List.sublist_cons_self c cs) h1
      · cases hr
        exact h2
    have headSub : ∀ (c : Nat) (cs l : List Nat) (a : Nat), (c :: cs).Sublist (a :: l) → c ≠ a → (c :: cs).Sublist l := by
      intro c cs l a h hne
      rcases List.sublist_cons_iff.mp h with h1 | ⟨r, hr, _⟩
      · exact h1
      · cases hr
        exact absurd rfl hne
    dsimp only [OA_statement]
    intro xs ys fuel
    induction fuel generalizing xs ys with
    | zero =>
      intro h
      have hx : xs = [] := List.eq_nil_of_length_eq_zero (by omega)
      have hy : ys = [] := List.eq_nil_of_length_eq_zero (by omega)
      subst hx
      subst hy
      refine ⟨⟨[], List.nil_sublist _, List.nil_sublist _, rfl⟩, ?_⟩
      intro common h1 _
      rw [List.sublist_nil.mp h1]
      exact Nat.le_refl _
    | succ n ih =>
      intro h
      dsimp only
      cases xs with
      | nil =>
        refine ⟨⟨[], List.nil_sublist _, List.nil_sublist _, rfl⟩, ?_⟩
        intro common h1 _
        rw [List.sublist_nil.mp h1]
        exact Nat.le_refl _
      | cons x xt =>
        cases ys with
        | nil =>
          refine ⟨⟨[], List.nil_sublist _, List.nil_sublist _, rfl⟩, ?_⟩
          intro common _ h2
          rw [List.sublist_nil.mp h2]
          exact Nat.le_refl _
        | cons y yt =>
          have h1 : xt.length + yt.length ≤ n := by simp at h; omega
          have h2 : xt.length + (y :: yt).length ≤ n := by simp at h ⊢; omega
          have h3 : (x :: xt).length + yt.length ≤ n := by simp at h ⊢; omega
          obtain ⟨⟨c1, s1x, s1y, l1⟩, m1⟩ := ih xt yt h1
          obtain ⟨⟨c2, s2x, s2y, l2⟩, m2⟩ := ih xt (y :: yt) h2
          obtain ⟨⟨c3, s3x, s3y, l3⟩, m3⟩ := ih (x :: xt) yt h3
          by_cases hxy : x = y
          · subst hxy
            simp only [ite_true]
            refine ⟨⟨x :: c1, List.cons_sublist_cons.mpr s1x, List.cons_sublist_cons.mpr s1y, ?_⟩, ?_⟩
            · simp only [List.length_cons]
              omega
            · intro common hc1 hc2
              cases common with
              | nil => exact Nat.zero_le _
              | cons c cs =>
                have := m1 cs (tailSub c cs xt x hc1) (tailSub c cs yt x hc2)
                simp only [List.length_cons]
                omega
          · simp only [hxy, ite_false]
            refine ⟨?_, ?_⟩
            · rcases Nat.le_total c2.length c3.length with hle | hle
              · exact ⟨c3, s3x, List.Sublist.cons y s3y, by omega⟩
              · exact ⟨c2, List.Sublist.cons x s2x, s2y, by omega⟩
            · intro common hc1 hc2
              cases common with
              | nil => exact Nat.zero_le _
              | cons c cs =>
                by_cases hcx : c = x
                · subst hcx
                  have := m3 (c :: cs) hc1 (headSub c cs yt y hc2 hxy)
                  omega
                · have := m2 (c :: cs) (headSub c cs xt x hc1 hcx) hc2
                  omega

#print axioms OA_target
#check OA_target