Type checker slows down

Stream: lean4

[Jeremy Salwen]

I am having a weird behavior with Lean 4 in VSCode. As I am writing more theorems, the type checking becomes extremely slow (i.e. the Lean InfoView takes 5-10 seconds to update). I actually have narrowed it down to a specific point in the file where I can edit one theorem and the tactic state updates immediately, but when I update the next theorem, it takes many seconds to respond. Nothing to me stands out about either of these theorems that would make them unusual or slow to check.

Here is the first theorem (github link in context):

theorem List.getD_singleton {n : Nat} (elem: α): List.getD [elem] n elem = elem := by
  unfold getD get? Option.getD
  simp only [cons.injEq, and_imp, forall_apply_eq_imp_iff', forall_eq']
  cases n
  . simp only
  . simp only [get?]

And here is the next theorem, where the lean infoview suddenly becomes slow to update (github link in context):

theorem Nat.toDigitsCore_shift' (b:ℕ) (n:ℕ) (P: b>1): ∀i:ℕ, (Nat.toDigits b n).reverse.getD (i+1) '0' = (Nat.toDigits b (n/b)).reverse.getD i '0':= by
   -- editing here is extremely slow.

[Jeremy Salwen]

I have experimented a bit more, it seems to be "conv" that is causing the extreme slowdown?

[Jeremy Salwen]

Here is an MWE:

import Mathlib.Tactic.LibrarySearch
import Lean

theorem Nat.toDigitsCore_slow (b:ℕ) (n:ℕ) (P: b>1): ∀i:ℕ, (Nat.toDigits b n).reverse.getD (i+1) '0' = (Nat.toDigits b (n/b)).reverse.getD i '0':= by
  intro i

  conv =>
    left
    unfold toDigits toDigitsCore
  sorry


theorem Nat.toDigitsCore_fast (b:ℕ) (n:ℕ) (P: b>1): ∀i:ℕ, (Nat.toDigits b n).reverse.getD (i+1) '0' = (Nat.toDigits b (n/b)).reverse.getD i '0':= by
  intro i

  rw [toDigits, toDigitsCore]
  sorry

Checking the "conv" version is extremely slow, using "rw" is instant.