fix

src/Init/Data/Dyadic/Basic.lean

@@ -682,9 +682,11 @@ instance : LE Dyadic where
 instance : DecidableLT Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
 instance : DecidableLE Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
 
-theorem lt_iff_toRat {x y : Dyadic} : x < y ↔ x.toRat < y.toRat := blt_iff_toRat
+@[simp]
+theorem toRat_lt_toRat_iff {x y : Dyadic} : x.toRat < y.toRat ↔ x < y := blt_iff_toRat.symm
 
-theorem le_iff_toRat {x y : Dyadic} : x ≤ y ↔ x.toRat ≤ y.toRat := ble_iff_toRat
+@[simp]
+theorem toRat_le_toRat_iff {x y : Dyadic} : x.toRat ≤ y.toRat ↔ x ≤ y := ble_iff_toRat.symm
 
 @[simp]
 protected theorem not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x := by
@@ -696,20 +698,20 @@ protected theorem not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x := by
 
 @[simp]
 protected theorem le_refl (x : Dyadic) : x ≤ x := by
-  rw [le_iff_toRat]
+  rw [← toRat_le_toRat_iff]
   exact Rat.le_refl
 
 protected theorem le_trans {x y z : Dyadic} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := by
-  rw [le_iff_toRat] at h h' ⊢
+  rw [← toRat_le_toRat_iff] at h h' ⊢
   exact Rat.le_trans h h'
 
 protected theorem le_antisymm {x y : Dyadic} (h : x ≤ y) (h' : y ≤ x) : x = y := by
-  rw [le_iff_toRat] at h h'
+  rw [← toRat_le_toRat_iff] at h h'
   rw [← toRat_inj]
   exact Rat.le_antisymm h h'
 
 protected theorem le_total (x y : Dyadic) : x ≤ y ∨ y ≤ x := by
-  rw [le_iff_toRat, le_iff_toRat]
+  rw [← toRat_le_toRat_iff, ← toRat_le_toRat_iff]
   exact Rat.le_total
 
 instance : Std.LawfulOrderLT Dyadic where

src/Init/Data/Dyadic/Instances.lean

@@ -52,8 +52,8 @@ instance : NoNatZeroDivisors Dyadic where
 
 instance : OrderedRing Dyadic where
   zero_lt_one := by decide
-  add_le_left_iff _ := by simp [le_iff_toRat, Rat.add_le_add_right]
-  mul_lt_mul_of_pos_left {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_left
-  mul_lt_mul_of_pos_right {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_right
+  add_le_left_iff _ := by simp [← toRat_le_toRat_iff, Rat.add_le_add_right]
+  mul_lt_mul_of_pos_left {_ _ _} := by simpa [← toRat_lt_toRat_iff] using Rat.mul_lt_mul_of_pos_left
+  mul_lt_mul_of_pos_right {_ _ _} := by simpa [← toRat_lt_toRat_iff] using Rat.mul_lt_mul_of_pos_right
 
 end Dyadic

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

src/Init/Data/Dyadic/Round.lean

@@ -28,7 +28,7 @@ theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
     match h : k - prec with
     | .ofNat l =>
       dsimp
-      rw [ofOdd_eq_ofIntWithPrec, le_iff_toRat]
+      rw [ofOdd_eq_ofIntWithPrec, ← toRat_le_toRat_iff]
       replace h : k = Int.ofNat l + prec := by omega
       subst h
       simp only [toRat_ofIntWithPrec_eq_mul_two_pow]