diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index 6c4c1b4c34ca..0d3ea8e9e89b 100644
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -94,12 +94,9 @@ theorem ofNat_sub_dichotomy {a b : Nat} :
     b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 := by
   by_cases h : b ≤ a
   · left
-    have := Int.ofNat_sub h
     simp [h]
   · right
-    have t := Nat.not_le.mp h
-    simp [Int.ofNat_sub_eq_zero h]
-    exact t
+    simp [Int.ofNat_sub_eq_zero, Nat.not_le.mp, h]
 
 theorem ofNat_congr {a b : Nat} (h : a = b) : (a : Int) = (b : Int) := congrArg _ h