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

State before:
time₁ time₂ : Time
x✝ : time₁.ns = time₂.ns
⊢ time₁ = time₂
Tactic:
cases time₁
State after:
case _private.Runtime.Time.0.Time.mk
time₂ : Time
ns✝ : Nat
x✝ : { ns := ns✝ }.ns = time₂.ns
⊢ { ns := ns✝ } = time₂

State before:
case _private.Runtime.Time.0.Time.mk
time₂ : Time
ns✝ : Nat
x✝ : { ns := ns✝ }.ns = time₂.ns
⊢ { ns := ns✝ } = time₂
Tactic:
simp_all
State after:
no goals