refactor: golf proofs

Co-authored-by: Kyle Miller <[email protected]>

Batteries/Data/List/Lemmas.lean

@@ -528,53 +528,23 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂
       simp [h]
 
 theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by
-   match l₁, l₂ with
-  | [],   _  => simp [commonPrefix]
-  | _::_, [] => simp [commonPrefix]
-  | a₁::l₁, a₂::l₂ =>
-    simp only [commonPrefix]
-    cases Decidable.em (a₁ = a₂)
-    · next h =>
-      simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
-      apply commonPrefix_prefix_right
-    · next h =>
-      simp [h]
+  rw [commonPrefix_comm]
+  apply commonPrefix_prefix_left
 
 theorem commonPrefix_append_append (p l₁ l₂ : List α) :
     commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by
   match p with
   | []   => rfl
   | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂
 
-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 ⟨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
+theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ : List α} (hp : commonPrefix l₁ l₂ = []) :
+    ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ l₁ ≠ [] ∧ l₂ ≠ [] ∧ l₁.head? ≠ l₂.head? := by
+  match l₁, l₂ with
+  | [], _  => simp
+  | _,  [] => simp
+  | a₁::l₁, a₂::l₂ =>
+    simp only [commonPrefix, ite_eq_right_iff, reduceCtorEq, imp_false] at hp
+    simp [hp, Ne.symm hp]
 
 end