Theorem: Time.of_to (Runtime/Time.lean)

State before:
value : Nat
unit : Time.Unit
⊢ to (of value unit) unit = value
Tactic:
simp [of, to, Unit.nsRatio]
State after:
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

State before:
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
Tactic:
cases unit <;> simp only [Nat.mul_div_cancel]
State after:
no goals