From db963f246f3f320404a884fcb0d43ec9495adb3d Mon Sep 17 00:00:00 2001
From: Yannick Seurin <yannick.seurin@gmail.com>
Date: Wed, 9 Oct 2024 22:20:17 +0200
Subject: [PATCH] use `exact` rather than `apply`

---
 MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean b/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
index ec755da5..42cf4389 100644
--- a/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
+++ b/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
@@ -604,7 +604,7 @@ theorem natAbs_norm_mod_lt (x y : GaussInt) (hy : y ≠ 0) :
     (x % y).norm.natAbs < y.norm.natAbs := by
   apply Int.ofNat_lt.1
   simp only [Int.natCast_natAbs, abs_of_nonneg, norm_nonneg]
-  apply norm_mod_lt x hy
+  exact norm_mod_lt x hy
 -- QUOTE.
 
 /- TEXT: