#show_unused doesn't account for simp lemma's proven by rfl

[pimotte]

import Batteries

def nul : Nat := 0

@[simp]
theorem lemma1 : nul = 0 := rfl

theorem uses_lemma1 : nul = 0 := by 
  simp

#show_unused uses_lemma1

In the above code sample, lemma1 is detected as unused, but removing lemma1 breaks the proof of uses_lemma1.