feat: golf IMO 1964 q1 (#5314)

`gcongr` lets modular arithmetic calculations go faster.  I've been pretty cavalier about deleting auxiliary lemmas from the old solution which weren't needed in the new; this is ok [per Scott](#5317 (comment)).

Archive/Imo/Imo1964Q1.lean

@@ -10,6 +10,7 @@ Authors: Kevin Buzzard
 -/
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Data.Nat.ModEq
+import Mathlib.Tactic.Ring
 
 /-!
 # IMO 1964 Q1
@@ -32,22 +33,12 @@ open Nat
 
 namespace Imo1964Q1
 
-theorem two_pow_three_mul_mod_seven (m : ℕ) : 2 ^ (3 * m) ≡ 1 [MOD 7] := by
-  rw [pow_mul]
-  have h : 8 ≡ 1 [MOD 7] := modEq_of_dvd (by use -1; norm_num)
-  convert h.pow _
-  simp
-#align imo1964_q1.two_pow_three_mul_mod_seven Imo1964Q1.two_pow_three_mul_mod_seven
-
-theorem two_pow_three_mul_add_one_mod_seven (m : ℕ) : 2 ^ (3 * m + 1) ≡ 2 [MOD 7] := by
-  rw [pow_add]
-  exact (two_pow_three_mul_mod_seven m).mul_right _
-#align imo1964_q1.two_pow_three_mul_add_one_mod_seven Imo1964Q1.two_pow_three_mul_add_one_mod_seven
-
-theorem two_pow_three_mul_add_two_mod_seven (m : ℕ) : 2 ^ (3 * m + 2) ≡ 4 [MOD 7] := by
-  rw [pow_add]
-  exact (two_pow_three_mul_mod_seven m).mul_right _
-#align imo1964_q1.two_pow_three_mul_add_two_mod_seven Imo1964Q1.two_pow_three_mul_add_two_mod_seven
+theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] :=
+  let t := n % 3
+  calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod]
+    _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul]
+    _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; norm_num
+    _ = 2 ^ t := by ring
 
 /-!
 ## The question
@@ -58,53 +49,27 @@ def ProblemPredicate (n : ℕ) : Prop :=
   7 ∣ 2 ^ n - 1
 #align imo1964_q1.problem_predicate Imo1964Q1.ProblemPredicate
 
-theorem aux (n : ℕ) : ProblemPredicate n ↔ 2 ^ n ≡ 1 [MOD 7] := by
-  rw [Nat.ModEq.comm]
-  apply (modEq_iff_dvd' _).symm
-  apply Nat.one_le_pow'
-#align imo1964_q1.aux Imo1964Q1.aux
-
 theorem imo1964_q1a (n : ℕ) (hn : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
-  rw [aux]
-  constructor
-  · intro h
-    let t := n % 3
-    rw [show n = 3 * (n / 3) + t from (Nat.div_add_mod n 3).symm] at h
-    have ht : t < 3 := Nat.mod_lt _ (by decide)
-    interval_cases hr : t <;> simp only [hr] at h
-    · exact Nat.dvd_of_mod_eq_zero hr
-    · exfalso
-      have nonsense := (two_pow_three_mul_add_one_mod_seven _).symm.trans h
-      rw [modEq_iff_dvd] at nonsense
-      norm_num at nonsense
-    · exfalso
-      have nonsense := (two_pow_three_mul_add_two_mod_seven _).symm.trans h
-      rw [modEq_iff_dvd] at nonsense
-      norm_num at nonsense
-  · rintro ⟨m, rfl⟩
-    apply two_pow_three_mul_mod_seven
+  let t := n % 3
+  have : t < 3 := Nat.mod_lt _ (by decide)
+  calc 7 ∣ 2 ^ n - 1 ↔ 2 ^ n ≡ 1 [MOD 7] := by
+        rw [Nat.ModEq.comm, Nat.modEq_iff_dvd']
+        apply Nat.one_le_pow'
+    _ ↔ 2 ^ t ≡ 1 [MOD 7] := ⟨(two_pow_mod_seven n).symm.trans, (two_pow_mod_seven n).trans⟩
+    _ ↔ t = 0 := by interval_cases t <;> decide
+    _ ↔ 3 ∣ n := by rw [dvd_iff_mod_eq_zero]
 #align imo1964_q1.imo1964_q1a Imo1964Q1.imo1964_q1a
 
 end Imo1964Q1
 
 open Imo1964Q1
 
 theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by
+  intro h
   let t := n % 3
-  rw [← modEq_zero_iff_dvd, show n = 3 * (n / 3) + t from (Nat.div_add_mod n 3).symm]
-  have ht : t < 3 := Nat.mod_lt _ (by decide)
-  interval_cases hr : t <;> simp only [hr]
-  · rw [add_zero]
-    intro h
-    have := h.symm.trans ((two_pow_three_mul_mod_seven _).add_right _)
-    rw [modEq_iff_dvd] at this
-    norm_num at this
-  · intro h
-    have := h.symm.trans ((two_pow_three_mul_add_one_mod_seven _).add_right _)
-    rw [modEq_iff_dvd] at this
-    norm_num at this
-  · intro h
-    have := h.symm.trans ((two_pow_three_mul_add_two_mod_seven _).add_right _)
-    rw [modEq_iff_dvd] at this
-    norm_num at this
+  have : t < 3 := Nat.mod_lt _ (by decide)
+  have H : 2 ^ t + 1 ≡ 0 [MOD 7]
+  · calc 2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
+      _ ≡ 0 [MOD 7] := h.modEq_zero_nat
+  interval_cases t <;> norm_num at H
 #align imo1964_q1b imo1964_q1b

Mathlib/Data/Nat/ModEq.lean

@@ -11,6 +11,7 @@ Authors: Mario Carneiro
 import Mathlib.Data.Int.GCD
 import Mathlib.Data.Int.Order.Lemmas
 import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.GCongr.Core
 
 /-!
 # Congruences modulo a natural number
@@ -114,6 +115,7 @@ protected theorem mul_left' (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [M
   unfold ModEq at *; rw [mul_mod_mul_left, mul_mod_mul_left, h]
 #align nat.modeq.mul_left' Nat.ModEq.mul_left'
 
+@[gcongr]
 protected theorem mul_left (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD n] :=
   (h.mul_left' _).of_dvd (dvd_mul_left _ _)
 #align nat.modeq.mul_left Nat.ModEq.mul_left
@@ -122,14 +124,17 @@ protected theorem mul_right' (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [
   rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left' c
 #align nat.modeq.mul_right' Nat.ModEq.mul_right'
 
+@[gcongr]
 protected theorem mul_right (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n] := by
   rw [mul_comm a, mul_comm b]; exact h.mul_left c
 #align nat.modeq.mul_right Nat.ModEq.mul_right
 
+@[gcongr]
 protected theorem mul (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a * c ≡ b * d [MOD n] :=
   (h₂.mul_left _).trans (h₁.mul_right _)
 #align nat.modeq.mul Nat.ModEq.mul
 
+@[gcongr]
 protected theorem pow (m : ℕ) (h : a ≡ b [MOD n]) : a ^ m ≡ b ^ m [MOD n] := by
   induction m with
   | zero => rfl
@@ -138,15 +143,18 @@ protected theorem pow (m : ℕ) (h : a ≡ b [MOD n]) : a ^ m ≡ b ^ m [MOD n]
     exact hd.mul h
 #align nat.modeq.pow Nat.ModEq.pow
 
+@[gcongr]
 protected theorem add (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n] := by
   rw [modEq_iff_dvd, Int.ofNat_add, Int.ofNat_add, add_sub_add_comm]
   exact dvd_add h₁.dvd h₂.dvd
 #align nat.modeq.add Nat.ModEq.add
 
+@[gcongr]
 protected theorem add_left (c : ℕ) (h : a ≡ b [MOD n]) : c + a ≡ c + b [MOD n] :=
   ModEq.rfl.add h
 #align nat.modeq.add_left Nat.ModEq.add_left
 
+@[gcongr]
 protected theorem add_right (c : ℕ) (h : a ≡ b [MOD n]) : a + c ≡ b + c [MOD n] :=
   h.add ModEq.rfl
 #align nat.modeq.add_right Nat.ModEq.add_right