From 68ff701134546dbd6e5fbb91ac509f6885ecf080 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Wed, 15 Jan 2025 16:53:56 -0500
Subject: [PATCH] [Imo1968P2] simplification found by LeanCopilot with
 tryAtEachStep

---
 Compfiles/Imo1968P2.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Compfiles/Imo1968P2.lean b/Compfiles/Imo1968P2.lean
index 15f2c13..380046c 100644
--- a/Compfiles/Imo1968P2.lean
+++ b/Compfiles/Imo1968P2.lean
@@ -25,11 +25,7 @@ snip begin
 lemma lemma0 {α β : Type} {f : ℕ → α → β} (l : List α) (h2 : l ≠ []) :
     List.getLast (List.mapIdx f l) (List.mapIdx_ne_nil_iff.mpr h2) =
     f (l.dropLast).length (List.getLast l h2) := by
-  simp_rw [List.mapIdx_eq_enum_map]
-  rw [List.getLast_eq_getElem, List.getElem_map, List.getElem_enum]
-  simp only [List.length_map, List.enum_length, Function.uncurry_apply_pair, List.length_dropLast]
-  congr
-  exact List.get_length_sub_one _
+  rw [List.getLast_mapIdx, List.length_dropLast]
 
 lemma prod_digits_le {x b : ℕ} (hb : 2 ≤ b) (xpos : 0 < x) :
     List.prod (Nat.digits b x) ≤ x := by