From 72b6f4d52872eb328109eca0062a79dfbdb991b6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Mar 2022 11:21:37 -0700
Subject: [PATCH] chore: avoid unnecessary `h :`s

---
 src/Init/Data/Nat/Div.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 3dc3165300..d8afde47f1 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -14,7 +14,7 @@ private def div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
 
 @[extern "lean_nat_div"]
 protected def div (x y : @& Nat) : Nat :=
-  if h : 0 < y ∧ y ≤ x then
+  if 0 < y ∧ y ≤ x then
     Nat.div (x - y) y + 1
   else
     0
@@ -23,8 +23,9 @@ decreasing_by apply div_rec_lemma; assumption
 instance : Div Nat := ⟨Nat.div⟩
 
 theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
-  simp [Nat.div] -- hack to force eq theorem to be generated. We don't have `conv` yet.
-  apply Nat.div._eq_1
+  show Nat.div x y = _
+  rw [Nat.div]
+  rfl
 
 theorem div.inductionOn.{u}
       {motive : Nat → Nat → Sort u}
@@ -40,7 +41,7 @@ decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
 protected def mod (x y : @& Nat) : Nat :=
-  if h : 0 < y ∧ y ≤ x then
+  if 0 < y ∧ y ≤ x then
     Nat.mod (x - y) y
   else
     x
@@ -49,8 +50,9 @@ decreasing_by apply div_rec_lemma; assumption
 instance : Mod Nat := ⟨Nat.mod⟩
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
-  simp [Nat.mod] -- hack to force eq theorem to be generated. We don't have `conv` yet.
-  apply Nat.mod._eq_1
+  show Nat.mod x y = _
+  rw [Nat.mod]
+  rfl
 
 theorem mod.inductionOn.{u}
       {motive : Nat → Nat → Sort u}