Improve modCore_eq_mod

leanprover · May 7, 2024 · 7254574 · 7254574
1 parent d2017ce
commit 7254574
Showing 1 changed file with 3 additions and 9 deletions.
diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
@@ -100,15 +100,9 @@ protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
   | 0, y =>
     rw [Nat.modCore]
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
-  | 1, 0 =>
-    rw [Nat.modCore]
-    exact if_neg fun ⟨hlt, _⟩ => Nat.lt_irrefl _ hlt
-  | 1, 1 =>
-    rw [Nat.modCore]
-    exact if_pos ⟨Nat.one_pos, Nat.le_refl _⟩
-  | 1, (y+2) =>
-    rw [Nat.modCore]
-    exact if_neg fun ⟨_, hle⟩ => Nat.not_succ_le_zero _ (Nat.le_of_succ_le_succ hle)
+  | 1, 0 => rw [Nat.modCore]; rfl
+  | 1, 1 => rw [Nat.modCore, Nat.modCore]; rfl
+  | 1, (y+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