diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean index ee12d886e9..303e0b8ea5 100644 --- a/Batteries/Data/Array/Lemmas.lean +++ b/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 -/ diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean index f96651d34c..2032b23ecd 100644 --- a/Batteries/Data/Rat/Basic.lean +++ b/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 ..) diff --git a/Batteries/Data/Rat/Lemmas.lean b/Batteries/Data/Rat/Lemmas.lean index 77b911ec94..b3c2d49915 100644 --- a/Batteries/Data/Rat/Lemmas.lean +++ b/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 ..)]