chore: make two proofs robust (#11983)

Proofs by `simp` with many `-lemmas` are very fragile, and indeed this one broke on `nightly-testing`.

Replaces with clearer proofs that use the relevant results already established, rather than fighting with `simp`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Data/Rat/Lemmas.lean

@@ -278,10 +278,12 @@ theorem inv_coe_nat_den_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a
 
 @[simp]
 theorem inv_coe_int_num (a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a := by
-  induction a using Int.induction_on <;>
-    simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out,
-      -Nat.cast_succ, inv_coe_nat_num_of_pos, -Int.cast_negSucc, @eq_comm ℤ 1,
-      Int.sign_eq_one_of_pos, ofInt_eq_cast]
+  rcases lt_trichotomy a 0 with lt | rfl | gt
+  · obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩
+    simp at lt
+    simp [Rat.inv_neg, inv_coe_int_num_of_pos lt, (Int.sign_eq_one_iff_pos _).mpr lt]
+  · rfl
+  · simp [inv_coe_int_num_of_pos gt, (Int.sign_eq_one_iff_pos _).mpr gt]
 #align rat.inv_coe_int_num Rat.inv_coe_int_num
 
 @[simp]
@@ -295,9 +297,15 @@ theorem inv_ofNat_num (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℚ)
 
 @[simp]
 theorem inv_coe_int_den (a : ℤ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a.natAbs := by
-  induction a using Int.induction_on <;>
-    simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out,
-      -Nat.cast_succ, inv_coe_nat_den_of_pos, -Int.cast_negSucc, ofInt_eq_cast]
+  rw [← Int.ofNat_inj]
+  rcases lt_trichotomy a 0 with lt | rfl | gt
+  · obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩
+    simp at lt
+    rw [if_neg (by omega)]
+    simp [Rat.inv_neg, inv_coe_int_den_of_pos lt, abs_of_pos lt]
+  · rfl
+  · rw [if_neg (by omega)]
+    simp [inv_coe_int_den_of_pos gt, abs_of_pos gt]
 #align rat.inv_coe_int_denom Rat.inv_coe_int_den
 
 @[simp]