[Usa2003Q1] finish 'suffices' block

dwrensha · Sep 6, 2023 · 20ded03 · 20ded03
1 parent 90afc48
commit 20ded03
Showing 1 changed file with 12 additions and 2 deletions.
diff --git a/MathPuzzles/Usa2003Q1.lean b/MathPuzzles/Usa2003Q1.lean
@@ -86,8 +86,18 @@ theorem usa2003Q1 (n : ℕ) :
       constructor
       · rw[←ha]; simp[hpm1]
       · constructor
-        · sorry-- exact hk2
-        · sorry
+        · rw[Nat.succ_eq_add_one]
+          nth_rewrite 1 [Nat.mul_comm]
+          exact hk2
+        · rw[List.all_eq_true]
+          rw[List.all_eq_true, ha] at hpm3
+          intro x hx
+          rw[List.mem_append] at hx
+          cases' hx with hx hx
+          · exact hpm3 x hx
+          · simp at hx
+            rw[hx]
+            exact decide_eq_true hk0
 
     -- This is equivalent to proving that there exists an odd digit k such that
     -- k·2ⁿ + a is divisible by 5,