From ad17506ee68ee2d2a53cf0e5c2bd84c111a70676 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Fri, 17 Nov 2023 12:00:17 -0500
Subject: [PATCH] [Imo2016P5] fill sorry from mathlib update

---
 Compfiles/Imo2016P5.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Compfiles/Imo2016P5.lean b/Compfiles/Imo2016P5.lean
index 732a7864..73a52853 100644
--- a/Compfiles/Imo2016P5.lean
+++ b/Compfiles/Imo2016P5.lean
@@ -56,7 +56,8 @@ problem imo2015_p5 :
       have h1 : 2 ∈ Finset.Icc 1 2016 := by
         simp (config := {decide := true}) only [Finset.mem_Icc]
       have h2 := h h1
-      sorry
+      simp only [Finset.mem_Icc, Finset.mem_filter] at h2
+      norm_num at h2
     · sorry
     · push_neg
       intro x