Sebastian Ullrich makes Lean's type class resolution cache persist across commands