refactor: make 1 % n reduce without well-founded recursion

src/Init/Data/Int/DivModLemmas.lean

@@ -178,7 +178,7 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
 
 @[simp] theorem mod_zero : ∀ a : Int, mod a 0 = a
   | ofNat _ => congrArg ofNat <| Nat.mod_zero _
-  | -[_+1] => rfl
+  | -[_+1] => congrArg (fun n => -ofNat n) <| Nat.mod_zero _
 
 @[simp] theorem zero_fmod (b : Int) : fmod 0 b = 0 := by cases b <;> rfl
 
@@ -225,7 +225,9 @@ theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
   | ofNat m, -[n+1] => by
     show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
     rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
-  | -[_+1], 0 => rfl
+  | -[m+1], 0 => by
+    show -(↑((succ m) % 0) : Int) + 0 * -↑(succ m / 0) = -↑(succ m)
+    rw [Nat.mod_zero, Int.zero_mul, Int.add_zero]
   | -[m+1], ofNat n => by
     show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
     rw [Int.mul_neg, ← Int.neg_add]

src/Init/Data/Nat/Div.lean

@@ -82,22 +82,28 @@ decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
 protected def mod : @& Nat → @& Nat → Nat
-  /- This case is not needed mathematically as the case below is equal to it; however, it makes
-  `0 % n = 0` true definitionally rather than just propositionally.
-  This property is desirable for `Fin n`, as it means `(ofNat 0 : Fin n).val = 0` by definition.
-  Primarily, this is valuable because mathlib in Lean3 assumed this was true definitionally, and so
-  keeping this definitional equality makes mathlib easier to port to mathlib4. -/
+  /- These four cases are not needed mathematically, they are just special cases of the
+  general case. However, it makes `0 % n = 0` etc. true definitionally rather than just
+  propositionally.
+  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
+  definition. This was true in lean3 and it simplified things for mathlib if it remains true. -/
   | 0, _ => 0
-  | x@(_ + 1), y => Nat.modCore x y
+  | 1, 0 => 0
+  | 1, 1 => 0
+  | 1, (_+2) => 1
+  | x@(_ + 2), y => Nat.modCore x y
 
 instance instMod : Mod Nat := ⟨Nat.mod⟩
 
 protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
-  cases x with
-  | zero =>
+  match x, y with
+  | 0, y =>
     rw [Nat.modCore]
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
-  | succ x => rfl
+  | 1, 0 => rw [Nat.modCore]; rfl
+  | 1, 1 => rw [Nat.modCore, Nat.modCore]; rfl
+  | 1, (_+2) => rw [Nat.modCore]; rfl
+  | (_ + 2), _ => rfl
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
   rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]