From 4e9c73e01a7a1633e7d88cbba8b4afc542aa251d Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Sat, 18 Nov 2023 09:23:03 -0500
Subject: [PATCH] [Imo1968P2] move mathlibby

---
 Compfiles/Imo1968P2.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/Compfiles/Imo1968P2.lean b/Compfiles/Imo1968P2.lean
index db16fb17..8058fefb 100644
--- a/Compfiles/Imo1968P2.lean
+++ b/Compfiles/Imo1968P2.lean
@@ -22,16 +22,13 @@ namespace Imo1968P2
 
 snip begin
 
+@[simp] theorem List.enum_eq_nil {α : Type*} {l : List α}
+    : List.enum l = [] ↔ l = [] := by
+  cases l <;> simp [List.enum_cons]
+
 @[simp] theorem List.mapIdx_eq_nil {α β : Type*} {f : ℕ → α → β} {l : List α}
     : List.mapIdx f l = [] ↔ l = [] := by
-  rw [List.mapIdx_eq_enum_map]
-  constructor
-  · intro hf
-    cases' l with l'
-    · rfl
-    · rw [List.enum_cons, List.map_cons] at hf
-      simp only [Function.uncurry_apply_pair] at hf
-  · exact fun _ => match l with | [] => rfl
+  rw [List.mapIdx_eq_enum_map, List.map_eq_nil, List.enum_eq_nil]
 
 lemma lemma0 {α β : Type} {f : ℕ → α → β} (l : List α) (h2 : l ≠ []) :
     List.getLast (List.mapIdx f l) (List.mapIdx_eq_nil.not.mpr h2) =