refactor: remove type annotation in remNano and secs

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Int.Linear
-public import Std.Internal.Rat
 public import Lean.Data.PersistentArray
 public import Lean.Meta.Tactic.Grind.ExprPtr
 public import Lean.Meta.Tactic.Grind.Arith.Util
@@ -19,7 +18,6 @@ public section
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 export Int.Linear (Var Poly)
-export Std.Internal (Rat)
 
 deriving instance Hashable for Poly
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/MBTC.lean

@@ -27,7 +27,7 @@ private partial def toRatValue? (a : Expr) : Option Rat :=
   else if a.isAppOfArity ``HDiv.hDiv 6 then
     (· / ·) <$> toRatValue? a.appFn!.appArg! <*> toRatValue? a.appArg!
   else if let .lit (.natVal n) := a then
-    some (Std.Internal.mkRat n 1)
+    some (mkRat n 1)
   else
     none
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean

@@ -6,17 +6,17 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Std.Internal.Rat
 public import Init.Grind.Ring.Poly
 public import Init.Grind.Ordered.Linarith
 public import Lean.Data.PersistentArray
 public import Lean.Meta.Tactic.Grind.ExprPtr
+public import Init.Data.Rat.Basic
 
 public section
 
 namespace Lean.Meta.Grind.Arith.Linear
 export Lean.Grind.Linarith (Var Poly)
-export Std.Internal (Rat)
+
 abbrev LinExpr := Lean.Grind.Linarith.Expr
 
 deriving instance Hashable for Poly

src/Lean/Meta/Tactic/Grind/Arith/ModelUtil.lean

@@ -6,13 +6,13 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Std.Internal.Rat
 public import Lean.Meta.Tactic.Grind.Types
+public import Init.Data.Rat.Basic
 
 public section
 
 namespace Lean.Meta.Grind.Arith
-open Std.Internal
+
 /-!
 Helper functions for constructing counterexamples in the `linarith` and `cutsat` modules
 -/

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Grind.Ring.Basic
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.Basic
-public import Std.Internal.Rat
+public import Init.Data.Rat.Basic
 
 public section
 
@@ -100,8 +100,6 @@ partial def gcdExt (a b : Int) : Int × Int × Int :=
     let (g, α, β) := gcdExt b (a % b)
     (g, β, α - (a / b) * β)
 
-open Std.Internal
-
 -- TODO: PArray.shrink and PArray.resize
 partial def shrink (a : PArray Rat) (sz : Nat) : PArray Rat :=
   if a.size > sz then shrink a.pop sz else a

src/Std/Internal/Rat.lean

@@ -1,152 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Init.NotationExtra
-public import Init.Data.ToString.Macro
-public import Init.Data.Int.DivMod.Basic
-public import Init.Data.Int.Linear
-public import Init.Data.Nat.Gcd
-
-@[expose] public section
-namespace Std
-namespace Internal
-
-/-!
-  Rational numbers for implementing decision procedures.
-  We should not confuse them with the Batteries rational numbers, also used by Mathlib.
--/
-
-structure Rat where
-  mk ::
-    num : Int
-    den : Nat := 1
-  deriving Inhabited, BEq, DecidableEq
-
-instance : ToString Rat where
-  toString a := if a.den == 1 then toString a.num else s!"{a.num}/{a.den}"
-
-instance : Repr Rat where
-  reprPrec a _ := if a.den == 1 then repr a.num else s!"({a.num} : Rat)/{a.den}"
-
-@[inline] def Rat.normalize (a : Rat) : Rat :=
-  let n := Nat.gcd a.num.natAbs a.den
-  if n == 1 then a else { num := a.num.tdiv n, den := a.den / n }
-
-def mkRat (num : Int) (den : Nat) : Rat :=
-  if den == 0 then { num := 0 } else Rat.normalize { num, den }
-
-namespace Rat
-
-protected def isInt (a : Rat) : Bool :=
-  a.den == 1
-
-protected def lt (a b : Rat) : Bool :=
-  if a.num < 0 && b.num >= 0 then
-    true
-  else if a.num == 0 then
-    b.num > 0
-  else if a.num > 0 && b.num <= 0 then
-    false
-  else
-    -- `a` and `b` must have the same sign
-   a.num * b.den < b.num * a.den
-
-protected def mul (a b : Rat) : Rat :=
-  let g1 := Nat.gcd a.den b.num.natAbs
-  let g2 := Nat.gcd a.num.natAbs b.den
-  { num := (a.num.tdiv g2)*(b.num.tdiv g1)
-    den := (b.den / g2)*(a.den / g1) }
-
-protected def inv (a : Rat) : Rat :=
-  if a.num < 0 then
-    { num := - a.den, den := a.num.natAbs }
-  else if a.num == 0 then
-    a
-  else
-    { num := a.den, den := a.num.natAbs }
-
-protected def div (a b : Rat) : Rat :=
-  Rat.mul a b.inv
-
-protected def add (a b : Rat) : Rat :=
-  let g := Nat.gcd a.den b.den
-  if g == 1 then
-    { num := a.num * b.den + b.num * a.den, den := a.den * b.den }
-  else
-    let den := (a.den / g) * b.den
-    let num := Int.ofNat (b.den / g) * a.num + Int.ofNat (a.den / g) * b.num
-    let g1  := Nat.gcd num.natAbs g
-    if g1 == 1 then
-      { num, den }
-    else
-      { num := num.tdiv g1, den := den / g1 }
-
-protected def sub (a b : Rat) : Rat :=
-  let g := Nat.gcd a.den b.den
-  if g == 1 then
-    { num := a.num * b.den - b.num * a.den, den := a.den * b.den }
-  else
-    let den := (a.den / g) * b.den
-    let num := (b.den / g) * a.num - (a.den / g) * b.num
-    let g1  := Nat.gcd num.natAbs g
-    if g1 == 1 then
-      { num, den }
-    else
-      { num := num.tdiv g1, den := den / g1 }
-
-protected def neg (a : Rat) : Rat :=
-  { a with num := - a.num }
-
-protected def floor (a : Rat) : Int :=
-  if a.den == 1 then
-    a.num
-  else
-    a.num / a.den
-
-protected def ceil (a : Rat) : Int :=
-  if a.den == 1 then
-    a.num
-  else
-    Int.Linear.cdiv a.num a.den
-
-instance : LT Rat where
-  lt a b := (Rat.lt a b) = true
-
-instance (a b : Rat) : Decidable (a < b) :=
-  inferInstanceAs (Decidable (_ = true))
-
-instance : LE Rat where
-  le a b := ¬(b < a)
-
-instance (a b : Rat) : Decidable (a ≤ b) :=
-  inferInstanceAs (Decidable (¬ _))
-
-instance : Add Rat where
-  add := Rat.add
-
-instance : Sub Rat where
-  sub := Rat.sub
-
-instance : Neg Rat where
-  neg := Rat.neg
-
-instance : Mul Rat where
-  mul := Rat.mul
-
-instance : Div Rat where
-  div a b := a * b.inv
-
-instance : OfNat Rat n where
-  ofNat := { num := n }
-
-instance : Coe Int Rat where
-  coe num := { num }
-
-end Rat
-end Internal
-end Std

src/Std/Time/Date/Basic.lean

@@ -23,28 +23,28 @@ Convert `Nanosecond.Offset` into `Day.Offset`.
 -/
 @[inline]
 def toDays (nanoseconds : Nanosecond.Offset) : Day.Offset :=
-  nanoseconds.div 86400000000000
+  nanoseconds.div 86400000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Nanosecond.Offset`.
 -/
 @[inline]
 def ofDays (days : Day.Offset) : Nanosecond.Offset :=
-  days.mul 86400000000000
+  days.mul 86400000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Nanosecond.Offset` into `Week.Offset`.
 -/
 @[inline]
 def toWeeks (nanoseconds : Nanosecond.Offset) : Week.Offset :=
-  nanoseconds.div 604800000000000
+  nanoseconds.div 604800000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Nanosecond.Offset`.
 -/
 @[inline]
 def ofWeeks (weeks : Week.Offset) : Nanosecond.Offset :=
-  weeks.mul 604800000000000
+  weeks.mul 604800000000000 |>.cast (by decide +kernel)
 
 end Offset
 end Nanosecond
@@ -57,28 +57,28 @@ Convert `Millisecond.Offset` into `Day.Offset`.
 -/
 @[inline]
 def toDays (milliseconds : Millisecond.Offset) : Day.Offset :=
-  milliseconds.div 86400000
+  milliseconds.div 86400000 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Millisecond.Offset`.
 -/
 @[inline]
 def ofDays (days : Day.Offset) : Millisecond.Offset :=
-  days.mul 86400000
+  days.mul 86400000 |>.cast (by decide +kernel)
 
 /--
 Convert `Millisecond.Offset` into `Week.Offset`.
 -/
 @[inline]
 def toWeeks (milliseconds : Millisecond.Offset) : Week.Offset :=
-  milliseconds.div 604800000
+  milliseconds.div 604800000 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Millisecond.Offset`.
 -/
 @[inline]
 def ofWeeks (weeks : Week.Offset) : Millisecond.Offset :=
-  weeks.mul 604800000
+  weeks.mul 604800000 |>.cast (by decide +kernel)
 
 end Offset
 end Millisecond
@@ -91,28 +91,28 @@ Convert `Second.Offset` into `Day.Offset`.
 -/
 @[inline]
 def toDays (seconds : Second.Offset) : Day.Offset :=
-  seconds.div 86400
+  seconds.div 86400 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Second.Offset`.
 -/
 @[inline]
 def ofDays (days : Day.Offset) : Second.Offset :=
-  days.mul 86400
+  days.mul 86400 |>.cast (by decide +kernel)
 
 /--
 Convert `Second.Offset` into `Week.Offset`.
 -/
 @[inline]
 def toWeeks (seconds : Second.Offset) : Week.Offset :=
-  seconds.div 604800
+  seconds.div 604800 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Second.Offset`.
 -/
 @[inline]
 def ofWeeks (weeks : Week.Offset) : Second.Offset :=
-  weeks.mul 604800
+  weeks.mul 604800 |>.cast (by decide +kernel)
 
 end Offset
 end Second
@@ -125,28 +125,28 @@ Convert `Minute.Offset` into `Day.Offset`.
 -/
 @[inline]
 def toDays (minutes : Minute.Offset) : Day.Offset :=
-  minutes.div 1440
+  minutes.div 1440 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Minute.Offset`.
 -/
 @[inline]
 def ofDays (days : Day.Offset) : Minute.Offset :=
-  days.mul 1440
+  days.mul 1440 |>.cast (by decide +kernel)
 
 /--
 Convert `Minute.Offset` into `Week.Offset`.
 -/
 @[inline]
 def toWeeks (minutes : Minute.Offset) : Week.Offset :=
-  minutes.div 10080
+  minutes.div 10080 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Minute.Offset`.
 -/
 @[inline]
 def ofWeeks (weeks : Week.Offset) : Minute.Offset :=
-  weeks.mul 10080
+  weeks.mul 10080 |>.cast (by decide +kernel)
 
 end Offset
 end Minute
@@ -159,28 +159,28 @@ Convert `Hour.Offset` into `Day.Offset`.
 -/
 @[inline]
 def toDays (hours : Hour.Offset) : Day.Offset :=
-  hours.div 24
+  hours.div 24 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Hour.Offset`.
 -/
 @[inline]
 def ofDays (days : Day.Offset) : Hour.Offset :=
-  days.mul 24
+  days.mul 24 |>.cast (by decide +kernel)
 
 /--
 Convert `Hour.Offset` into `Week.Offset`.
 -/
 @[inline]
 def toWeeks (hours : Hour.Offset) : Week.Offset :=
-  hours.div 168
+  hours.div 168 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Hour.Offset`.
 -/
 @[inline]
 def ofWeeks (weeks : Week.Offset) : Hour.Offset :=
-  weeks.mul 168
+  weeks.mul 168 |>.cast (by decide +kernel)
 
 end Offset
 end Hour

src/Std/Time/Date/PlainDate.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Std.Time.Internal
 public import Std.Time.Date.Basic
-public import Std.Internal.Rat
 import all Std.Time.Date.Unit.Month
 import all Std.Time.Date.Unit.Year
 

src/Std/Time/Date/Unit/Basic.lean

@@ -33,7 +33,7 @@ Convert `Week.Offset` into `Day.Offset`.
 -/
 @[inline]
 def ofWeeks (week : Week.Offset) : Day.Offset :=
-  week.mul 7
+  week.mul 7 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Week.Offset`.

src/Std/Time/Date/Unit/Day.lean

@@ -174,70 +174,70 @@ Convert `Day.Offset` into `Nanosecond.Offset`.
 -/
 @[inline]
 def toNanoseconds (days : Day.Offset) : Nanosecond.Offset :=
-  days.mul 86400000000000
+  days.mul 86400000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Nanosecond.Offset` into `Day.Offset`.
 -/
 @[inline]
 def ofNanoseconds (ns : Nanosecond.Offset) : Day.Offset :=
-  ns.ediv 86400000000000
+  ns.ediv 86400000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Millisecond.Offset`.
 -/
 @[inline]
 def toMilliseconds (days : Day.Offset) : Millisecond.Offset :=
-  days.mul 86400000
+  days.mul 86400000 |>.cast (by decide +kernel)
 
 /--
 Convert `Millisecond.Offset` into `Day.Offset`.
 -/
 @[inline]
 def ofMilliseconds (ms : Millisecond.Offset) : Day.Offset :=
-  ms.ediv 86400000
+  ms.ediv 86400000 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Second.Offset`.
 -/
 @[inline]
 def toSeconds (days : Day.Offset) : Second.Offset :=
-  days.mul 86400
+  days.mul 86400 |>.cast (by decide +kernel)
 
 /--
 Convert `Second.Offset` into `Day.Offset`.
 -/
 @[inline]
 def ofSeconds (secs : Second.Offset) : Day.Offset :=
-  secs.ediv 86400
+  secs.ediv 86400 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (days : Day.Offset) : Minute.Offset :=
-  days.mul 1440
+  days.mul 1440 |>.cast (by decide +kernel)
 
 /--
 Convert `Minute.Offset` into `Day.Offset`.
 -/
 @[inline]
 def ofMinutes (minutes : Minute.Offset) : Day.Offset :=
-  minutes.ediv 1440
+  minutes.ediv 1440 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Hour.Offset`.
 -/
 @[inline]
 def toHours (days : Day.Offset) : Hour.Offset :=
-  days.mul 24
+  days.mul 24 |>.cast (by decide +kernel)
 
 /--
 Convert `Hour.Offset` into `Day.Offset`.
 -/
 @[inline]
 def ofHours (hours : Hour.Offset) : Day.Offset :=
-  hours.ediv 24
+  hours.ediv 24 |>.cast (by decide +kernel)
 
 end Offset
 end Day

src/Std/Time/Date/Unit/Month.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Date.Unit.Day
 
 public section
@@ -228,24 +227,21 @@ Transforms `Month.Ordinal` into `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (leap : Bool) (month : Ordinal) : Minute.Offset :=
-  toSeconds leap month
-  |>.ediv 60
+  toSeconds leap month |>.toMinutes
 
 /--
 Transforms `Month.Ordinal` into `Hour.Offset`.
 -/
 @[inline]
 def toHours (leap : Bool) (month : Ordinal) : Hour.Offset :=
-  toMinutes leap month
-  |>.ediv 60
+  toMinutes leap month |>.toHours
 
 /--
 Transforms `Month.Ordinal` into `Day.Offset`.
 -/
 @[inline]
 def toDays (leap : Bool) (month : Ordinal) : Day.Offset :=
-  toSeconds leap month
-  |>.convert
+  toSeconds leap month |>.convert
 
 /--
 Size in days of each month if the year is not a leap year.

src/Std/Time/Date/Unit/Week.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Date.Unit.Day
 
 public section
@@ -133,77 +132,77 @@ Convert `Week.Offset` into `Millisecond.Offset`.
 -/
 @[inline]
 def toMilliseconds (weeks : Week.Offset) : Millisecond.Offset :=
-  weeks.mul 604800000
+  weeks.mul 604800000 |>.cast (by decide +kernel)
 
 /--
 Convert `Millisecond.Offset` into `Week.Offset`.
 -/
 @[inline]
 def ofMilliseconds (millis : Millisecond.Offset) : Week.Offset :=
-  millis.ediv 604800000
+  millis.ediv 604800000 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Nanosecond.Offset`.
 -/
 @[inline]
 def toNanoseconds (weeks : Week.Offset) : Nanosecond.Offset :=
-  weeks.mul 604800000000000
+  weeks.mul 604800000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Nanosecond.Offset` into `Week.Offset`.
 -/
 @[inline]
 def ofNanoseconds (nanos : Nanosecond.Offset) : Week.Offset :=
-  nanos.ediv 604800000000000
+  nanos.ediv 604800000000000 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Second.Offset`.
 -/
 @[inline]
 def toSeconds (weeks : Week.Offset) : Second.Offset :=
-  weeks.mul 604800
+  weeks.mul 604800 |>.cast (by decide +kernel)
 
 /--
 Convert `Second.Offset` into `Week.Offset`.
 -/
 @[inline]
 def ofSeconds (secs : Second.Offset) : Week.Offset :=
-  secs.ediv 604800
+  secs.ediv 604800 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (weeks : Week.Offset) : Minute.Offset :=
-  weeks.mul 10080
+  weeks.mul 10080 |>.cast (by decide +kernel)
 
 /--
 Convert `Minute.Offset` into `Week.Offset`.
 -/
 @[inline]
 def ofMinutes (minutes : Minute.Offset) : Week.Offset :=
-  minutes.ediv 10080
+  minutes.ediv 10080 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Hour.Offset`.
 -/
 @[inline]
 def toHours (weeks : Week.Offset) : Hour.Offset :=
-  weeks.mul 168
+  weeks.mul 168 |>.cast (by decide +kernel)
 
 /--
 Convert `Hour.Offset` into `Week.Offset`.
 -/
 @[inline]
 def ofHours (hours : Hour.Offset) : Week.Offset :=
-  hours.ediv 168
+  hours.ediv 168 |>.cast (by decide +kernel)
 
 /--
 Convert `Week.Offset` into `Day.Offset`.
 -/
 @[inline]
 def toDays (weeks : Week.Offset) : Day.Offset :=
-  weeks.mul 7
+  weeks.mul 7 |>.cast (by decide +kernel)
 
 /--
 Convert `Day.Offset` into `Week.Offset`.

src/Std/Time/Date/Unit/Weekday.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Date.Unit.Day
 
 public section

src/Std/Time/Date/Unit/Year.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Time.Internal
-public import Std.Internal.Rat
 public import Std.Time.Date.Unit.Day
 public import Std.Time.Date.Unit.Month
 

src/Std/Time/Date/ValidDate.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Date.Unit.Day
 public import all Std.Time.Date.Unit.Month
 

src/Std/Time/DateTime/PlainDateTime.lean

@@ -72,8 +72,17 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
   let daysPer4Y := 365 * 4 + 1
 
   let nanos := stamp.toNanosecondsSinceUnixEpoch
-  let secs : Second.Offset := nanos.ediv 1000000000
-  let daysSinceEpoch : Day.Offset := secs.tdiv 86400
+
+  let secs : Second.Offset := nanos.toSeconds
+  let remNano := Bounded.LE.byMod nanos.val 1000000000 (by decide)
+
+  let (remNano, secs) :=
+    if h : remNano.val < 0 then
+      (remNano.truncateTop (Int.le_sub_one_of_lt h) |>.add 1000000000 |>.expandBottom (by decide), secs - 1)
+    else
+      (remNano.truncateBottom (Int.not_lt.mp h), secs)
+
+  let daysSinceEpoch : Day.Offset := secs.toDays
   let boundedDaysSinceEpoch := daysSinceEpoch
 
   let mut rawDays := boundedDaysSinceEpoch - leapYearEpoch

src/Std/Time/DateTime/Timestamp.lean

@@ -80,14 +80,14 @@ Converts a `Timestamp` to minutes as `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (tm : Timestamp) : Minute.Offset :=
-  tm.val.second.ediv 60
+  tm.val.second.toMinutes
 
 /--
 Converts a `Timestamp` to days as `Day.Offset`.
 -/
 @[inline]
 def toDays (tm : Timestamp) : Day.Offset :=
-  tm.val.second.ediv 86400
+  tm.val.second.toDays
 
 /--
 Creates a `Timestamp` from a `Second.Offset` since the Unix epoch.

src/Std/Time/Duration.lean

@@ -99,7 +99,8 @@ def ofSeconds (s : Second.Offset) : Duration := by
 Creates a new `Duration` out of `Nanosecond.Offset`.
 -/
 def ofNanoseconds (s : Nanosecond.Offset) : Duration := by
-  refine ⟨s.tdiv 1000000000, Bounded.LE.byMod s.val 1000000000 (by decide), ?_⟩
+  -- TODO: we should be using `s.toSeconds` here, but the proof below depends on this form.
+  refine ⟨s.tdiv 1000000000 |>.cast (by decide +kernel), Bounded.LE.byMod s.val 1000000000 (by decide), ?_⟩
 
   cases Int.le_total s.val 0
   next n => exact Or.inr (And.intro (tdiv_neg n (by decide)) (mod_nonpos 1000000000 n (by decide)))
@@ -119,7 +120,7 @@ Creates a new `Duration` out of `Millisecond.Offset`.
 -/
 @[inline]
 def ofMillisecond (s : Millisecond.Offset) : Duration :=
-  ofNanoseconds (s.mul 1000000)
+  ofNanoseconds (s.toNanoseconds)
 
 /--
 Checks if the duration is zero seconds and zero nanoseconds.
@@ -171,14 +172,14 @@ Converts a `Duration` to a `Minute.Offset`
 -/
 @[inline]
 def toMinutes (tm : Duration) : Minute.Offset :=
-  tm.second.tdiv 60
+  tm.second.toMinutes
 
 /--
 Converts a `Duration` to a `Day.Offset`
 -/
 @[inline]
 def toDays (tm : Duration) : Day.Offset :=
-  tm.second.tdiv 86400
+  tm.second.toDays
 
 /--
 Normalizes `Second.Offset` and `NanoSecond.span` in order to build a new `Duration` out of it.
@@ -248,7 +249,7 @@ Adds a `Minute.Offset` to a `Duration`
 -/
 @[inline]
 def addMinutes (t : Duration) (m : Minute.Offset) : Duration :=
-  let seconds := m.mul 60
+  let seconds := m.toSeconds
   t.addSeconds seconds
 
 /--
@@ -256,7 +257,7 @@ Subtracts a `Minute.Offset` from a `Duration`
 -/
 @[inline]
 def subMinutes (t : Duration) (m : Minute.Offset) : Duration :=
-  let seconds := m.mul 60
+  let seconds := m.toSeconds
   t.subSeconds seconds
 
 /--
@@ -264,7 +265,7 @@ Adds an `Hour.Offset` to a `Duration`
 -/
 @[inline]
 def addHours (t : Duration) (h : Hour.Offset) : Duration :=
-  let seconds := h.mul 3600
+  let seconds := h.toSeconds
   t.addSeconds seconds
 
 /--
@@ -272,7 +273,7 @@ Subtracts an `Hour.Offset` from a `Duration`
 -/
 @[inline]
 def subHours (t : Duration) (h : Hour.Offset) : Duration :=
-  let seconds := h.mul 3600
+  let seconds := h.toSeconds
   t.subSeconds seconds
 
 /--
@@ -280,7 +281,7 @@ Adds a `Day.Offset` to a `Duration`
 -/
 @[inline]
 def addDays (t : Duration) (d : Day.Offset) : Duration :=
-  let seconds := d.mul 86400
+  let seconds := d.toSeconds
   t.addSeconds seconds
 
 /--
@@ -288,7 +289,7 @@ Subtracts a `Day.Offset` from a `Duration`
 -/
 @[inline]
 def subDays (t : Duration) (d : Day.Offset) : Duration :=
-  let seconds := d.mul 86400
+  let seconds := d.toSeconds
   t.subSeconds seconds
 
 /--
@@ -296,7 +297,7 @@ Adds a `Week.Offset` to a `Duration`
 -/
 @[inline]
 def addWeeks (t : Duration) (w : Week.Offset) : Duration :=
-  let seconds := w.mul 604800
+  let seconds := w.toSeconds
   t.addSeconds seconds
 
 /--
@@ -304,7 +305,7 @@ Subtracts a `Week.Offset` from a `Duration`
 -/
 @[inline]
 def subWeeks (t : Duration) (w : Week.Offset) : Duration :=
-  let seconds := w.mul 604800
+  let seconds := w.toSeconds
   t.subSeconds seconds
 
 instance : HAdd Duration Day.Offset Duration where

src/Std/Time/Internal/UnitVal.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Order.Ord
-public import Std.Internal.Rat
+public import Init.Data.Rat.Basic
 
 @[expose] public section
 
@@ -147,6 +147,9 @@ instance : Neg (UnitVal α) where neg x := ⟨-x.val⟩
 
 instance : ToString (UnitVal n) where toString n := toString n.val
 
+/-- Cast a UnitVal through an equality in the rational numbers. -/
+def cast (_ : a = b) (x : UnitVal a) : UnitVal b :=
+  .ofInt (x.val)
 
 end UnitVal
 end Internal

src/Std/Time/Time/Unit/Basic.lean

@@ -36,21 +36,21 @@ Converts a `Nanosecond.Offset` to a `Millisecond.Offset`.
 -/
 @[inline]
 def toMilliseconds (offset : Nanosecond.Offset) : Millisecond.Offset :=
-  offset.div 1000000
+  offset.div 1000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Millisecond.Offset` to a `Nanosecond.Offset`.
 -/
 @[inline]
 def ofMilliseconds (offset : Millisecond.Offset) : Nanosecond.Offset :=
-  offset.mul 1000000
+  offset.mul 1000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Nanosecond.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def toSeconds (offset : Nanosecond.Offset) : Second.Offset :=
-  offset.div 1000000000
+  offset.div 1000000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Second.Offset` to a `Nanosecond.Offset`.
@@ -64,28 +64,28 @@ Converts a `Nanosecond.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (offset : Nanosecond.Offset) : Minute.Offset :=
-  offset.div 60000000000
+  offset.div 60000000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Minute.Offset` to a `Nanosecond.Offset`.
 -/
 @[inline]
 def ofMinutes (offset : Minute.Offset) : Nanosecond.Offset :=
-  offset.mul 60000000000
+  offset.mul 60000000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Nanosecond.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def toHours (offset : Nanosecond.Offset) : Hour.Offset :=
-  offset.div 3600000000000
+  offset.div 3600000000000 |>.cast (by decide +kernel)
 
 /--
 Converts an `Hour.Offset` to a `Nanosecond.Offset`.
 -/
 @[inline]
 def ofHours (offset : Hour.Offset) : Nanosecond.Offset :=
-  offset.mul 3600000000000
+  offset.mul 3600000000000 |>.cast (by decide +kernel)
 
 end Nanosecond.Offset
 
@@ -96,21 +96,21 @@ Converts a `Millisecond.Offset` to a `Nanosecond.Offset`.
 -/
 @[inline]
 def toNanoseconds (offset : Millisecond.Offset) : Nanosecond.Offset :=
-  offset.mul 1000000
+  offset.mul 1000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Nanosecond.Offset` to a `Millisecond.Offset`.
 -/
 @[inline]
 def ofNanoseconds (offset : Nanosecond.Offset) : Millisecond.Offset :=
-  offset.div 1000000
+  offset.toMilliseconds
 
 /--
 Converts a `Millisecond.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def toSeconds (offset : Millisecond.Offset) : Second.Offset :=
-  offset.div 1000
+  offset.div 1000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Second.Offset` to a `Millisecond.Offset`.
@@ -124,28 +124,28 @@ Converts a `Millisecond.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (offset : Millisecond.Offset) : Minute.Offset :=
-  offset.div 60000
+  offset.div 60000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Minute.Offset` to a `Millisecond.Offset`.
 -/
 @[inline]
 def ofMinutes (offset : Minute.Offset) : Millisecond.Offset :=
-  offset.mul 60000
+  offset.mul 60000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Millisecond.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def toHours (offset : Millisecond.Offset) : Hour.Offset :=
-  offset.div 3600000
+  offset.div 3600000 |>.cast (by decide +kernel)
 
 /--
 Converts an `Hour.Offset` to a `Millisecond.Offset`.
 -/
 @[inline]
 def ofHours (offset : Hour.Offset) : Millisecond.Offset :=
-  offset.mul 3600000
+  offset.mul 3600000 |>.cast (by decide +kernel)
 
 end Millisecond.Offset
 
@@ -163,7 +163,7 @@ Converts a `Nanosecond.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def ofNanoseconds (offset : Nanosecond.Offset) : Second.Offset :=
-  offset.div 1000000000
+  offset.toSeconds
 
 /--
 Converts a `Second.Offset` to a `Millisecond.Offset`.
@@ -177,35 +177,35 @@ Converts a `Millisecond.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def ofMilliseconds (offset : Millisecond.Offset) : Second.Offset :=
-  offset.div 1000
+  offset.toSeconds
 
 /--
 Converts a `Second.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (offset : Second.Offset) : Minute.Offset :=
-  offset.div 60
+  offset.div 60 |>.cast (by decide +kernel)
 
 /--
 Converts a `Minute.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def ofMinutes (offset : Minute.Offset) : Second.Offset :=
-  offset.mul 60
+  offset.mul 60 |>.cast (by decide +kernel)
 
 /--
 Converts a `Second.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def toHours (offset : Second.Offset) : Hour.Offset :=
-  offset.div 3600
+  offset.div 3600 |>.cast (by decide +kernel)
 
 /--
 Converts an `Hour.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def ofHours (offset : Hour.Offset) : Second.Offset :=
-  offset.mul 3600
+  offset.mul 3600 |>.cast (by decide +kernel)
 
 end Second.Offset
 
@@ -216,56 +216,56 @@ Converts a `Minute.Offset` to a `Nanosecond.Offset`.
 -/
 @[inline]
 def toNanoseconds (offset : Minute.Offset) : Nanosecond.Offset :=
-  offset.mul 60000000000
+  offset.mul 60000000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Nanosecond.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def ofNanoseconds (offset : Nanosecond.Offset) : Minute.Offset :=
-  offset.div 60000000000
+  offset.toMinutes
 
 /--
 Converts a `Minute.Offset` to a `Millisecond.Offset`.
 -/
 @[inline]
 def toMilliseconds (offset : Minute.Offset) : Millisecond.Offset :=
-  offset.mul 60000
+  offset.mul 60000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Millisecond.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def ofMilliseconds (offset : Millisecond.Offset) : Minute.Offset :=
-  offset.div 60000
+  offset.toMinutes
 
 /--
 Converts a `Minute.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def toSeconds (offset : Minute.Offset) : Second.Offset :=
-  offset.mul 60
+  offset.mul 60 |>.cast (by decide +kernel)
 
 /--
 Converts a `Second.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def ofSeconds (offset : Second.Offset) : Minute.Offset :=
-  offset.div 60
+  offset.toMinutes
 
 /--
 Converts a `Minute.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def toHours (offset : Minute.Offset) : Hour.Offset :=
-  offset.div 60
+  offset.div 60 |>.cast (by decide +kernel)
 
 /--
 Converts an `Hour.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def ofHours (offset : Hour.Offset) : Minute.Offset :=
-  offset.mul 60
+  offset.mul 60 |>.cast (by decide +kernel)
 
 end Minute.Offset
 
@@ -276,56 +276,56 @@ Converts an `Hour.Offset` to a `Nanosecond.Offset`.
 -/
 @[inline]
 def toNanoseconds (offset : Hour.Offset) : Nanosecond.Offset :=
-  offset.mul 3600000000000
+  offset.mul 3600000000000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Nanosecond.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def ofNanoseconds (offset : Nanosecond.Offset) : Hour.Offset :=
-  offset.div 3600000000000
+  offset.toHours
 
 /--
 Converts an `Hour.Offset` to a `Millisecond.Offset`.
 -/
 @[inline]
 def toMilliseconds (offset : Hour.Offset) : Millisecond.Offset :=
-  offset.mul 3600000
+  offset.mul 3600000 |>.cast (by decide +kernel)
 
 /--
 Converts a `Millisecond.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def ofMilliseconds (offset : Millisecond.Offset) : Hour.Offset :=
-  offset.div 3600000
+  offset.toHours
 
 /--
 Converts an `Hour.Offset` to a `Second.Offset`.
 -/
 @[inline]
 def toSeconds (offset : Hour.Offset) : Second.Offset :=
-  offset.mul 3600
+  offset.mul 3600 |>.cast (by decide +kernel)
 
 /--
 Converts a `Second.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def ofSeconds (offset : Second.Offset) : Hour.Offset :=
-  offset.div 3600
+  offset.toHours
 
 /--
 Converts an `Hour.Offset` to a `Minute.Offset`.
 -/
 @[inline]
 def toMinutes (offset : Hour.Offset) : Minute.Offset :=
-  offset.mul 60
+  offset.mul 60 |>.cast (by decide +kernel)
 
 /--
 Converts a `Minute.Offset` to an `Hour.Offset`.
 -/
 @[inline]
 def ofMinutes (offset : Minute.Offset) : Hour.Offset :=
-  offset.div 60
+  offset.toHours
 
 end Hour.Offset
 

src/Std/Time/Time/Unit/Hour.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Internal
 public import Std.Time.Time.Unit.Minute
 public import Std.Time.Time.Unit.Second

src/Std/Time/Time/Unit/Millisecond.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Internal
 public import Std.Time.Time.Unit.Nanosecond
 

src/Std/Time/Time/Unit/Minute.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Internal
 public import Std.Time.Time.Unit.Second
 

src/Std/Time/Time/Unit/Nanosecond.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Internal
 
 public section

src/Std/Time/Time/Unit/Second.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Rat
 public import Std.Time.Time.Unit.Nanosecond
 
 @[expose] public section

src/Std/Time/Zoned/Offset.lean

@@ -59,7 +59,7 @@ and minute components are separated by a colon (e.g., "+01:00" or "+0100").
 -/
 def toIsoString (offset : Offset) (colon : Bool) : String :=
   let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second)
-  let hour : Hour.Offset := time.ediv 3600
+  let hour : Hour.Offset := time.toHours
   let minute := Int.ediv (Int.tmod time.val 3600) 60
   let hourStr := if hour.val < 10 then s!"0{hour.val}" else toString hour.val
   let minuteStr := if minute < 10 then s!"0{minute}" else toString minute