remove redundant proofs

Author: tobiasgrosser

src/Init/Data/BitVec/Lemmas.lean

@@ -1982,7 +1982,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
 
 @[simp, bv_toNat] theorem toInt_sub {x y : BitVec w} :
   (x - y).toInt = (x.toInt - y.toInt).bmod (2^w) := by
-  simp [toInt_eq_toNat_bmod, Int.natCast_sub (2 ^ w) y.toNat (by omega)]
+  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
 
 -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
 -- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes

src/Init/Data/Int/Lemmas.lean

@@ -68,20 +68,6 @@ def eq_add_one_iff_neg_eq_negSucc {m n : Nat} : m = n + 1 ↔ -↑m = -[n+1] :=
 
 @[norm_cast] theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
 
-@[local simp] theorem ofNat_sub_ofNat (m n : Nat) (h : n ≤ m) : (↑m - ↑n : Int) = ↑(m - n) := by
-  simp only [instHSub, Sub.sub, Int.sub, instHAdd, Add.add, Int.add]
-  split
-  case h_1 _ _ _ nb _ hb =>
-    symm at hb
-    cases n <;> simp_all [(@ofNat_inj nb 0).mp]
-  case h_2 _ _ na _ ha hb =>
-    have h' := eq_add_one_iff_neg_eq_negSucc.mpr hb
-    have h'' := (@ofNat_inj m na).mp ha
-    rw [h', h''] at h
-    simp [subNatNat_of_sub h, ofNat_inj, h', h'']
-  · simp_all
-  · simp_all
-
 theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj
 
 theorem ofNat_ne_zero : ((n : Nat) : Int) ≠ 0 ↔ n ≠ 0 := not_congr ofNat_eq_zero
@@ -554,12 +540,6 @@ theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
   -- so it still makes sense to tag the lemmas with `@[simp]`.
   simp
 
-@[simp] theorem natCast_sub (a b : Nat) (h : b ≤ a) :
-    ((a - b : Nat) : Int) = (a : Int) - (b : Int) := by
-  simp [h]
-  -- Note this only works because of local simp attributes in this file,
-  -- so it still makes sense to tag the lemmas with `@[simp]`.
-
 @[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
   simp
 

src/Init/Omega/Int.lean

@@ -94,9 +94,13 @@ 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
-    simp [h]
+    have t := Int.ofNat_sub h
+    simp at t
+    exact ⟨h, t⟩
   · right
-    simp [Int.ofNat_sub_eq_zero, Nat.not_le.mp, h]
+    have t := Nat.not_le.mp h
+    simp [Int.ofNat_sub_eq_zero h]
+    exact t
 
 theorem ofNat_congr {a b : Nat} (h : a = b) : (a : Int) = (b : Int) := congrArg _ h