fix

Author: kim-em

src/Init/Data/Dyadic/Inv.lean

@@ -27,7 +27,7 @@ def invAtPrec (x : Dyadic) (prec : Int) : Dyadic :=
 /-- For a positive dyadic `x`, `invAtPrec x prec * x ≤ 1`. -/
 theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
     invAtPrec x prec * x ≤ 1 := by
-  rw [le_iff_toRat]
+  rw [← toRat_le_toRat_iff]
   rw [toRat_mul]
   rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
   unfold invAtPrec
@@ -39,19 +39,19 @@ theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
     simp only
     have h_le : ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat ≤ (ofOdd n k hn).toRat.inv := Rat.toRat_toDyadic_le
     have h_pos : 0 ≤ (ofOdd n k hn).toRat := by
-      rw [lt_iff_toRat, toRat_zero] at hx
+      rw [← toRat_lt_toRat_iff, toRat_zero] at hx
       exact Rat.le_of_lt hx
     calc ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat * (ofOdd n k hn).toRat
         ≤ (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := Rat.mul_le_mul_of_nonneg_right h_le h_pos
       _ = 1 := by
         apply Rat.inv_mul_cancel
-        rw [lt_iff_toRat, toRat_zero] at hx
+        rw [← toRat_lt_toRat_iff, toRat_zero] at hx
         exact Rat.ne_of_gt hx
 
 /-- For a positive dyadic `x`, `1 < (invAtPrec x prec + 2^(-prec)) * x`. -/
 theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
     1 < (invAtPrec x prec + ofIntWithPrec 1 prec) * x := by
-  rw [lt_iff_toRat]
+  rw [← toRat_lt_toRat_iff]
   rw [toRat_mul]
   rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
   unfold invAtPrec
@@ -64,12 +64,12 @@ theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
     have h_le : (ofOdd n k hn).toRat.inv < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat :=
       Rat.lt_toRat_toDyadic_add
     have h_pos : 0 < (ofOdd n k hn).toRat := by
-      rwa [lt_iff_toRat, toRat_zero] at hx
+      rwa [← toRat_lt_toRat_iff, toRat_zero] at hx
     calc
       1 = (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := by
         symm
         apply Rat.inv_mul_cancel
-        rw [lt_iff_toRat, toRat_zero] at hx
+        rw [← toRat_lt_toRat_iff, toRat_zero] at hx
         exact Rat.ne_of_gt hx
       _ < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat * (ofOdd n k hn).toRat :=
            Rat.mul_lt_mul_of_pos_right h_le h_pos