Update mathlib

Interval/Fixed.lean

@@ -971,19 +971,20 @@ lemma Fixed.approx_ofRat (x : ℚ) (up : Bool) :
       rw [e] at dn ⊢; clear e sn
       generalize (-s).toNat = s at dn
       simp only [Int.shiftRight_neg, Int.shiftLeft_eq_mul_pow, zpow_neg,
-        mul_inv_le_iff two_pow_pos, Nat.cast_pow, Nat.cast_ofNat, zpow_natCast] at dn ⊢
+        mul_inv_le_iff₀ (two_pow_pos (R := ℝ)), Nat.cast_pow, Nat.cast_ofNat, zpow_natCast] at dn ⊢
       nth_rw 3 [← Rat.num_div_den x]
       simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, ← mul_div_assoc,
         Int64.toInt_ofInt dn]
       induction up
-      · simp only [Bool.not_false, mem_rounds_singleton, mul_inv_le_iff two_pow_pos, ←
-          mul_div_assoc, mul_comm _ (x.num : ℝ), ite_true, ge_iff_le]
+      · simp only [Bool.not_false, mem_rounds_singleton, mul_inv_le_iff₀ (two_pow_pos (R := ℝ)), ←
+          mul_div_assoc, mul_comm _ (x.num : ℝ), ite_true]
         refine le_trans Int.rdiv_le ?_
-        simp only [Int.cast_mul, Int.cast_pow, AddGroupWithOne.intCast_ofNat, le_refl, Int.cast_ofNat]
+        field_simp
       · simp only [rounds, ← div_eq_mul_inv, mem_singleton_iff, Bool.not_true, ite_false,
           exists_eq_left, le_div_iff₀ (G₀ := ℝ) two_pow_pos, mem_setOf_eq, Bool.false_eq_true]
         refine le_trans (le_of_eq ?_) Int.le_rdiv
-        simp only [div_eq_mul_inv, Int.cast_mul, Int.cast_pow, AddGroupWithOne.intCast_ofNat]; ring_nf
+        simp only [div_eq_mul_inv, Int.cast_mul, Int.cast_pow, AddGroupWithOne.intCast_ofNat]
+        ring_nf
     · rw [ofRat, sn, cond_true] at n
       simp only [bif_eq_if, dn, decide_False, ite_false, not_true_eq_false, Bool.false_eq_true] at n
   · simp only [Bool.cond_decide, sn, cond_false, val, mem_rounds_singleton,
@@ -1052,7 +1053,7 @@ lemma Fixed.val_mem_log2 {x : Fixed s} (h : x.log2 ≠ nan) :
   by_cases x0 : x.n ≤ 0
   · simp only [x0, decide_True, bif_eq_if, ite_true, ne_eq, not_true_eq_false] at h
   · simp only [val, x0, decide_False, cond_false, mem_Ico, ← div_le_iff₀ (G₀ := ℝ) two_zpow_pos,
-      ←lt_div_iff two_zpow_pos, ←zpow_sub₀ t0] at h ⊢
+      ← lt_div_iff₀ (two_zpow_pos (𝕜 := ℝ)), ←zpow_sub₀ t0] at h ⊢
     have v := Fixed.val_add h
     simp only [val, Int64.coe_zero, zpow_zero, mul_one, ←Int.cast_add, Int.cast_inj] at v
     simp only [v]; ring_nf
@@ -1099,7 +1100,7 @@ lemma Fixed.approx_two_pow (n : Fixed 0) (up : Bool) :
         exact h.2
       have k64 : k.n.n.toNat < 64 := by omega
       have e1 : 1 % 2 ^ (64 - k.n.n.toNat) = 1 :=
-        Nat.mod_eq_of_lt (one_lt_pow (by norm_num) (by omega))
+        Nat.mod_eq_of_lt (one_lt_pow₀ (by norm_num) (by omega))
       have lt : (⟨1 <<< k.n.n⟩ : Int64).n.toNat < 2 ^ 63 := by
         simp only [UInt64.toNat_shiftLeft k64, UInt64.toNat_one, e1, one_mul]
         exact pow_lt_pow_right (by norm_num) k63

Interval/Int64.lean

@@ -878,7 +878,7 @@ lemma Int64.isNeg_one_shift {s : UInt64} (s64 : s.toNat < 64) :
     decide_eq_decide]
   rw [Nat.mod_eq_of_lt, one_mul, pow_le_pow_iff_right (by omega)]
   · constructor; intro; omega; intro; omega
-  · exact one_lt_pow (by norm_num) (by omega)
+  · exact one_lt_pow₀ (by norm_num) (by omega)
 
 /-- `ℤ` conversion for `UInt64` powers of two -/
 lemma Int64.coe_one_shift {s : UInt64} (s63 : s.toNat < 63) :
@@ -887,7 +887,7 @@ lemma Int64.coe_one_shift {s : UInt64} (s63 : s.toNat < 63) :
   have e : (1 <<< s : UInt64).toNat = 2^s.toNat := by
     simp only [UInt64.toNat_shiftLeft', UInt64.toNat_one, Nat.mod_eq_of_lt s64, ne_eq,
       pow_eq_zero_iff', OfNat.ofNat_ne_zero, false_and, not_false_eq_true, mul_eq_right₀]
-    exact Nat.mod_eq_of_lt (one_lt_pow (by norm_num) (by omega))
+    exact Nat.mod_eq_of_lt (one_lt_pow₀ (by norm_num) (by omega))
   simp only [toInt, e, Nat.cast_pow, Nat.cast_ofNat, isNeg_one_shift s64, s63.ne, decide_False,
     bif_eq_if, ite_false, CharP.cast_eq_zero, sub_zero, Bool.false_eq_true]
 
@@ -901,7 +901,7 @@ lemma Int64.coe_neg_one_shift {s : UInt64} (s63 : s.toNat < 63) :
   rw [Nat.mod_eq_of_lt]
   · simp only [one_mul, gt_iff_lt, zero_lt_two, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true,
       pow_right_inj, s63.ne]
-  · exact one_lt_pow (by norm_num) (by omega)
+  · exact one_lt_pow₀ (by norm_num) (by omega)
 
 /-- Negated `ℤ` conversion for `UInt64` values -/
 lemma Int64.coe_eq_toNat_of_lt {n : UInt64} (h : n.toNat < 2^63) :

Interval/UInt128.lean

@@ -955,7 +955,7 @@ lemma UInt128.toNat_hi_shiftRightRound_le_hi {y : UInt64} {s : UInt64} {up : Boo
     Nat.cast_ofNat, Int.cast_mul, Int.cast_ofNat, Int.cast_pow, Int.cast_natCast, Nat.cast_add,
     Int.cast_add]
   trans y.toNat * 2^64 + 1
-  · exact add_le_add_right (div_le_self (by positivity) (one_le_pow_of_one_le (by norm_num) _)) _
+  · exact add_le_add_right (div_le_self (by positivity) (one_le_pow₀ (by norm_num))) _
   · have e : (2^64 : ℝ) = (2^64 : ℕ) := by norm_num
     simp only [e, ←Nat.cast_mul, ←Nat.cast_add_one, ←Nat.cast_add, Nat.cast_le]
     norm_num

Interval/UInt64.lean

@@ -627,7 +627,7 @@ lemma UInt64.toNat_shiftRightRound' {x : UInt64} {s : UInt64} {up : Bool} :
       Nat.div_one, ceilDiv_one]
     · rw [Nat.ceilDiv_eq_add_pred_div, Nat.add_sub_assoc]
       · simp only [ite_true]
-      · exact one_le_pow_of_one_le (by norm_num) _
+      · exact one_le_pow₀ (by norm_num)
 
 /-- `UInt64.shiftRightRound` only makes things smaller -/
 lemma UInt64.shiftRightRound_le_self {x : UInt64} {s : UInt64} {up : Bool} :

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
+   "rev": "f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4660dcd5b4234594c7ebf2bcfb56f19c6bf156f3",
+   "rev": "0c13e18343c06775d5f2121a433f70392b7e2caa",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",