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