cases unit <;> simp only [Nat.mul_div_cancel]
value : Nat
unit : Time.Unit
⊢ ((value *
        match unit with
        | Unit.ns => 1
        | Unit.μs => 1000
        | Unit.ms => 1000 * 1000
        | Unit.s => 1000 * 1000 * 1000
        | Unit.mins => 1000 * 1000 * 1000 * 60
        | Unit.hours => 1000 * 1000 * 1000 * 60 * 60
        | Unit.days => 1000 * 1000 * 1000 * 60 * 60 * 24
        | Unit.weeks => 1000 * 1000 * 1000 * 60 * 60 * 24 * 7) /
      match unit with
      | Unit.ns => 1
      | Unit.μs => 1000
      | Unit.ms => 1000 * 1000
      | Unit.s => 1000 * 1000 * 1000
      | Unit.mins => 1000 * 1000 * 1000 * 60
      | Unit.hours => 1000 * 1000 * 1000 * 60 * 60
      | Unit.days => 1000 * 1000 * 1000 * 60 * 60 * 24
      | Unit.weeks => 1000 * 1000 * 1000 * 60 * 60 * 24 * 7) =
    value
no goals