From 02c0907c9bbd181977c37218e94c2b344e3d190f Mon Sep 17 00:00:00 2001
From: Adrien Champion <adrien.champion@protonmail.com>
Date: Mon, 8 Jul 2024 11:33:47 +0200
Subject: [PATCH] chore: proved `Rat.eq_neg_of_add_eq_zero_left`

---
 Smt/Reconstruct/Rat/Core.lean | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean
index d442abc0..bce94b2a 100644
--- a/Smt/Reconstruct/Rat/Core.lean
+++ b/Smt/Reconstruct/Rat/Core.lean
@@ -66,6 +66,8 @@ protected theorem eq_mkRat : ∀ a : Rat, a = mkRat a.num a.den := fun a => by
 @[simp]
 theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by
   congr
+  apply Nat.coprime_zero_left d |>.mp w
+
 
 theorem eq_iff_mul_eq_mul {p q : Rat} : p = q ↔ p.num * q.den = q.num * p.den := by
   conv =>
@@ -109,7 +111,7 @@ protected theorem lt_asymm {x y : Rat} : x < y → ¬ y < x := by
     rw [h]
   | inr h =>
     split at h
-    case inl xnum_0 =>
+    case isTrue xnum_0 =>
       simp [Int.not_lt_of_lt_rev h, xnum_0, h]
     case inr xnum_ne_0 =>
       let ⟨h, h'⟩ := h
@@ -357,18 +359,15 @@ protected theorem sub_self : x - x = 0 :=
 protected theorem add_neg_self : x + -x = 0 :=
   Rat.sub_eq_add_neg x x ▸ Rat.sub_self
 
--- #TODO use `eq_iff_mul_eq_mul`
 protected theorem eq_neg_of_add_eq_zero_left : x + y = 0 → x = - y :=
-  numDenCasesOn'' x fun nx dx h_dx h_red =>
-  numDenCasesOn'' y fun ny dy h_dy h_red' => by
-    simp only [Rat.neg_divInt, Rat.add_def]
+  numDenCasesOn'' x fun nx dx h_dx h_dx_red =>
+  numDenCasesOn'' y fun ny dy h_dy h_dy_red => by
+    simp only [Rat.neg_divInt, Rat.add_def, Neg.neg]
+    simp only [Rat.neg, normalize_eq_zero]
+    simp only [eq_iff_mul_eq_mul, ← Int.neg_mul_eq_neg_mul]
     intro h
-    simp [Neg.neg] ; simp [Rat.neg]
-    simp only [Rat.normalize_eq_zero] at h
-    let h_dpos : 0 < ↑dx := Int.natCast_pos.mpr (Nat.pos_iff_ne_zero.mpr h_dx)
-    let h_dpos' : 0 < ↑dy := Int.natCast_pos.mpr (Nat.pos_iff_ne_zero.mpr h_dy)
-    let h' := Int.neg_eq_of_add_eq_zero h
-    sorry
+    apply Int.eq_neg_of_eq_neg
+    exact Int.neg_eq_of_add_eq_zero h |>.symm
 
 protected theorem le_iff_sub_nonneg (x y : Rat) : x ≤ y ↔ 0 ≤ y - x :=
   numDenCasesOn'' x fun nx dx h_dx _ =>
@@ -399,10 +398,10 @@ protected theorem le_iff_sub_nonneg (x y : Rat) : x ≤ y ↔ 0 ≤ y - x :=
     else
       simp [h]
       split
-      case inl nb_0 =>
+      case isTrue nb_0 =>
         simp [nb_0, Rat.sub_eq_add_neg, Rat.zero_add, Rat.nonneg_sub_iff_nonpos, ← Rat.num_nonpos]
         exact Int.not_lt
-      case inr nb_nz =>
+      case isFalse nb_nz =>
         simp only [Rat.sub_def, normalize_eq, ← Rat.num_nonneg]
         if ny_pos : 0 < ny then
           simp [ny_pos]