From 0cc4c918008d64269460bdba41fbcd3df8445af6 Mon Sep 17 00:00:00 2001 From: Giles Shaw <62542365+gilesgshaw@users.noreply.github.com> Date: Tue, 22 Jul 2025 14:21:48 +0100 Subject: [PATCH] fix: change the proof of Nat.zero_mod to rfl (#9391) This PR replaces the proof of the simplification lemma `Nat.zero_mod` with `rfl` since it is, by design, a definitional equality. This solves an issue whereby the lemma could not be used by the simplifier when in 'dsimp' mode. Closes #9389 --------- Co-authored-by: Joachim Breitner --- src/Init/Data/Nat/Div/Basic.lean | 7 +------ tests/lean/run/9389.lean | 2 ++ 2 files changed, 3 insertions(+), 6 deletions(-) create mode 100644 tests/lean/run/9389.lean diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean index fbcd12c071..ff836ae506 100644 --- a/src/Init/Data/Nat/Div/Basic.lean +++ b/src/Init/Data/Nat/Div/Basic.lean @@ -350,12 +350,7 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by theorem mod_lt_of_lt {a b c : Nat} (h : a < c) : a % b < c := Nat.lt_of_le_of_lt (Nat.mod_le _ _) h -@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by - rw [mod_eq] - have : ¬ (0 < b ∧ b = 0) := by - intro ⟨h₁, h₂⟩ - simp_all - simp [this] +@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := rfl @[simp] theorem mod_self (n : Nat) : n % n = 0 := by rw [mod_eq_sub_mod (Nat.le_refl _), Nat.sub_self, zero_mod] diff --git a/tests/lean/run/9389.lean b/tests/lean/run/9389.lean new file mode 100644 index 0000000000..e405556aab --- /dev/null +++ b/tests/lean/run/9389.lean @@ -0,0 +1,2 @@ +/-! Tests that `zero_mod` is `@[defeq]` -/ +example (n : Nat) : 0 % n = 0 := by dsimp