refactor: rename and restate theorem

* Remove the "_exists" part from the theorem's name.
* Remove the existential quantifiers from the theorem's statement and
  add new hypotheses.

Batteries/Data/List/Lemmas.lean

@@ -546,24 +546,35 @@ theorem commonPrefix_append_append (p l₁ l₂ : List α) :
   | []   => rfl
   | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂
 
-theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} :
-    ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧
-      l₂ = pre ++ c₂ :: suf₂ := by
+theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p)
+    (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧
+      t₁.head? ≠ t₂.head? := by
   constructor <;> intro h
-  · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1)
-    obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2)
-    simp only [cons_prefix_cons, not_and] at h
-    cases Decidable.em (c₁ = c₂)
-    · subst c₂
-      simp only [forall_const] at h
-      let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ :=
-        not_prefix_and_not_prefix_symm_iff_exists.mp h
-      exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩
-    · next hc =>
-      exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩
-  · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h
-    rw [heq₁, heq₂]
-    simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm]
+  · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1)
+    obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2)
+    cases Decidable.em (a₁ = a₂)
+    · subst a₂
+      simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂
+      simp only [cons_prefix_cons, true_and] at h
+      exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h
+    · next hne =>
+      simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂
+      simp [← h₁, ← h₂, hne]
+  · rw [h₁, h₂]
+    let ⟨ht₁, ht₂, hhd⟩ := h
+    obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁
+    obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂
+    simp only [head?_cons, ne_eq, Option.some.injEq] at hhd
+    rw [← ne_eq] at hhd
+    simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm]
+termination_by l₁.length
+decreasing_by
+  rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁
+    _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇
+  clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄
+    _₂₅ _₂₆ _₂₇
+  subst _l₁
+  simp
 
 end