Trigger CI for leanprover/lean4#5309

Batteries/Data/Array/Lemmas.lean

@@ -153,8 +153,6 @@ theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
 
 /-! ### mem -/
 
-alias not_mem_empty := not_mem_nil
-
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
 /-! ### append -/

Batteries/Data/Rat/Basic.lean

@@ -45,23 +45,23 @@ Auxiliary definition for `Rat.normalize`. Constructs `num / den` as a rational n
 dividing both `num` and `den` by `g` (which is the gcd of the two) if it is not 1.
 -/
 @[inline] def Rat.maybeNormalize (num : Int) (den g : Nat)
-    (den_nz : den / g ≠ 0) (reduced : (num.div g).natAbs.Coprime (den / g)) : Rat :=
+    (den_nz : den / g ≠ 0) (reduced : (num.tdiv g).natAbs.Coprime (den / g)) : Rat :=
   if hg : g = 1 then
     { num, den
       den_nz := by simp [hg] at den_nz; exact den_nz
       reduced := by simp [hg, Int.natAbs_ofNat] at reduced; exact reduced }
-  else { num := num.div g, den := den / g, den_nz, reduced }
+  else { num := num.tdiv g, den := den / g, den_nz, reduced }
 
 theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den ≠ 0)
     (e : g = num.natAbs.gcd den) : den / g ≠ 0 :=
   e ▸ Nat.ne_of_gt (Nat.div_gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
 
 theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den ≠ 0)
-    (e : g = num.natAbs.gcd den) : (num.div g).natAbs.Coprime (den / g) :=
-  have : Int.natAbs (num.div ↑g) = num.natAbs / g := by
+    (e : g = num.natAbs.gcd den) : (num.tdiv g).natAbs.Coprime (den / g) :=
+  have : Int.natAbs (num.tdiv ↑g) = num.natAbs / g := by
     match num, num.eq_nat_or_neg with
     | _, ⟨_, .inl rfl⟩ => rfl
-    | _, ⟨_, .inr rfl⟩ => rw [Int.neg_div, Int.natAbs_neg, Int.natAbs_neg]; rfl
+    | _, ⟨_, .inr rfl⟩ => rw [Int.neg_tdiv, Int.natAbs_neg, Int.natAbs_neg]; rfl
   this ▸ e ▸ Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero den_nz))
 
 /--
@@ -141,12 +141,12 @@ want to unfold it. Use `Rat.mul_def` instead.) -/
 @[irreducible] protected def mul (a b : Rat) : Rat :=
   let g1 := Nat.gcd a.num.natAbs b.den
   let g2 := Nat.gcd b.num.natAbs a.den
-  { num := (a.num.div g1) * (b.num.div g2)
+  { num := (a.num.tdiv g1) * (b.num.tdiv g2)
     den := (a.den / g2) * (b.den / g1)
     den_nz := Nat.ne_of_gt <| Nat.mul_pos
       (Nat.div_gcd_pos_of_pos_right _ a.den_pos) (Nat.div_gcd_pos_of_pos_right _ b.den_pos)
     reduced := by
-      simp only [Int.natAbs_mul, Int.natAbs_div, Nat.coprime_mul_iff_left]
+      simp only [Int.natAbs_mul, Int.natAbs_tdiv, Nat.coprime_mul_iff_left]
       refine ⟨Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩, Nat.coprime_mul_iff_right.2 ⟨?_, ?_⟩⟩
       · exact a.reduced.coprime_div_left (Nat.gcd_dvd_left ..)
           |>.coprime_div_right (Nat.gcd_dvd_right ..)

Batteries/Data/Rat/Lemmas.lean

@@ -23,14 +23,14 @@ theorem ext : {p q : Rat} → p.num = q.num → p.den = q.den → p = q
 
 @[simp] theorem maybeNormalize_eq {num den g} (den_nz reduced) :
     maybeNormalize num den g den_nz reduced =
-    { num := num.div g, den := den / g, den_nz, reduced } := by
+    { num := num.tdiv g, den := den / g, den_nz, reduced } := by
   unfold maybeNormalize; split
   · subst g; simp
   · rfl
 
 theorem normalize.reduced' {num : Int} {den g : Nat} (den_nz : den ≠ 0)
     (e : g = num.natAbs.gcd den) : (num / g).natAbs.Coprime (den / g) := by
-  rw [← Int.div_eq_ediv_of_dvd (e ▸ Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
+  rw [← Int.tdiv_eq_ediv_of_dvd (e ▸ Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
   exact normalize.reduced den_nz e
 
 theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
@@ -39,10 +39,10 @@ theorem normalize_eq {num den} (den_nz) : normalize num den den_nz =
       den_nz := normalize.den_nz den_nz rfl
       reduced := normalize.reduced' den_nz rfl } := by
   simp only [normalize, maybeNormalize_eq,
-    Int.div_eq_ediv_of_dvd (Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
+    Int.tdiv_eq_ediv_of_dvd (Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]
 
 @[simp] theorem normalize_zero (nz) : normalize 0 d nz = 0 := by
-  simp [normalize, Int.zero_div, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl
+  simp [normalize, Int.zero_tdiv, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl
 
 theorem mk_eq_normalize (num den nz c) : ⟨num, den, nz, c⟩ = normalize num den nz := by
   simp [normalize_eq, c.gcd_eq_one]
@@ -76,7 +76,7 @@ theorem normalize_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
 theorem maybeNormalize_eq_normalize {num : Int} {den g : Nat} (den_nz reduced)
     (hn : ↑g ∣ num) (hd : g ∣ den) :
     maybeNormalize num den g den_nz reduced = normalize num den (mt (by simp [·]) den_nz) := by
-  simp only [maybeNormalize_eq, mk_eq_normalize, Int.div_eq_ediv_of_dvd hn]
+  simp only [maybeNormalize_eq, mk_eq_normalize, Int.tdiv_eq_ediv_of_dvd hn]
   have : g ≠ 0 := mt (by simp [·]) den_nz
   rw [← normalize_mul_right _ this, Int.ediv_mul_cancel hn]
   congr 1; exact Nat.div_mul_cancel hd
@@ -267,9 +267,9 @@ theorem mul_def (a b : Rat) :
   have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz
   have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz
   rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]; congr 1
-  · rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.div ..),
-      Int.div_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
-      Int.div_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
+  · rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.tdiv ..),
+      Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
+      Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
   · rw [← Nat.mul_assoc, Nat.mul_right_comm, Nat.mul_right_comm (_/_),
       Nat.div_mul_cancel (Nat.gcd_dvd_right ..), Nat.mul_assoc,
       Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]