[Usa1998P1] rfl works, apparently

Compfiles/Usa1998P1.lean

@@ -43,50 +43,6 @@ lemma mod2_abs (a : ℤ) : |a| % 2 = a % 2 := by
 lemma mod2_diff (a b : ℤ) : |a - b| % 2 = (a + b) % 2 := by
   rw [mod2_abs, Int.sub_eq_add_neg, Int.add_emod, Int.neg_emod_two, ←Int.add_emod]
 
-lemma lemma0 (n : ℕ) :
-    (∑ x in (Finset.Ioc (4 * n + 2) (4 * n.succ + 2)), (x:ℤ) % 2) % 2 = 0 := by
-  have h1 : 4 * n.succ + 2 = 4 * n + 2 + 1 + 1 + 1 + 1 := by linarith
-  rw [h1]
-  rw [Finset.sum_Ioc_succ_top (by norm_num), Finset.sum_Ioc_succ_top (by norm_num),
-      Finset.sum_Ioc_succ_top (by norm_num), Finset.sum_Ioc_succ_top (by norm_num),
-      Finset.Ioc_self, Finset.sum_empty, zero_add]
-  norm_cast
-  norm_num [Nat.add_mod, Nat.mul_mod]
-
-lemma lemma1 (n : ℕ) :
-    (∑ x in Finset.attach (Finset.Icc 1 (4 * n + 2)), ((x:ℕ):ℤ) % 2) % 2 = 1 % 2 := by
- induction' n with n ih
- · decide
- · rw [Finset.sum_attach (f := fun x ↦ (x:ℤ) %2) (s := Finset.Icc 1 (4 * n.succ + 2))]
-   rw [Finset.sum_attach (f := fun x ↦ (x:ℤ) %2) (s := Finset.Icc 1 (4 * n + 2))] at ih
-   let s1 := Finset.Icc 1 (4 * n + 2)
-   let s2 := Finset.Ioc (4 * n + 2) (4 * n.succ + 2)
-   have hd : Disjoint s1 s2 := by
-      intro a hs1 hs2 b hb
-      have hb1 := hs1 hb
-      have hb2 := hs2 hb
-      rw [Finset.mem_Icc] at hb1
-      rw [Finset.mem_Ioc] at hb2
-      linarith
-   have hu : Finset.Icc 1 (4 * Nat.succ n + 2) = Finset.disjUnion s1 s2 hd := by
-     ext a
-     constructor
-     · intro ha
-       rw [Finset.mem_disjUnion]
-       rw [Finset.mem_Icc] at ha ⊢
-       rw [Finset.mem_Ioc]
-       by_contra H
-       rw [not_or, not_and_or, not_and_or, not_le, not_le, not_lt, not_le] at H
-       obtain ⟨H1, H2⟩ := H
-       cases' H1 with H11 H12 <;> cases' H2 with H21 H22 <;> linarith
-     · intro ha
-       rw [Finset.mem_disjUnion] at ha
-       rw [Finset.mem_Icc] at ha ⊢
-       rw [Finset.mem_Ioc] at ha
-       cases' ha with ha1 ha2 <;> constructor <;> linarith
-   rw [hu, Finset.sum_disjUnion, Int.add_emod, ih, lemma0 n]
-   norm_num
-
 snip end
 
 /--
@@ -150,7 +106,7 @@ problem usa1998_p1
       by apply Fintype.sum_bijective _ hab
          · exact congr_fun rfl
     rw [h9, h10]
-    norm_num [lemma1 499]
+    rfl
 
   -- Combining these facts gives S ≡ 9 MOD 10.
   have hmn : Nat.Coprime (Int.natAbs 2) (Int.natAbs 5) := by norm_cast