From 7254574837c0fbff96d6589a5a6e63eb05ba4d96 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 7 May 2024 22:57:01 +0200 Subject: [PATCH] Improve modCore_eq_mod --- src/Init/Data/Nat/Div.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean index d570a32b24ee..f49aae34757c 100644 --- 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