Linter - Unused Lemmas

Stream: new members

[Tomaz Mascarenhas]

Hi, I have a project with one main theorem and many others. I need to identify which theorems were actually used in the proof of the main theorem (i.e. which ones will make the main theorem break removed). Is there a linter for that?

[Michael Rothgang]

This idea has come up in the past --- I'm not aware of any tooling to help you with this, sadly. It would be nice to have it!

[Evan Wang]

If I’m understanding the tool you are looking for correctly, this thread might be relevant, though I don't think there is a one shot tool for the requested task:
Extracting proof dependencies

[Evan Wang]

import Mathlib
import ImportGraph.RequiredModules

open Lean

#eval show CoreM Unit from do
  let n : Name := `Nat.add_comm
  let deps ← n.transitivelyUsedConstants
  let depsNat := deps.toArray.filter (fun d => (`Nat).isPrefixOf d)
  IO.println s!"Nat-prefixed transitive deps of {n}: {depsNat}"

This outputs

Nat-prefixed transitive deps of Nat.add_comm: #[Nat.brecOn.go, Nat.rec, Nat.brecOn, Nat.below, Nat, Nat.zero, Nat.add.match_1, Nat.zero_add, Nat.succ_add, Nat.succ, Nat.add, Nat.casesOn, Nat.add_comm]

Should be what you are looking for