use exact rather than apply

avigad · Jan 6, 2025 · db963f2 · db963f2
1 parent ac9825e
commit db963f2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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: