そのモジュールで使用されているタクティクのリストを取得する

I don't have time to look at this in detail, but the unused tactic linter extracts tactics from commands. A very crude copy-paste-modify of the code there, produces this:

import Mathlib

open Lean in
def headString (s : Syntax) : String :=
  (s.getHead?.getD default).getSubstring?.getD "" |>.toString.trim

open Lean Elab Command Mathlib.Linter.UnusedTactic in
elab "tacs " cmd:command : command => do
  elabCommand cmd
  let env ← getEnv
  let cats := (Parser.parserExtension.getState env).categories
  -- These lookups may fail when the linter is run in a fresh, empty environment
  let some tactics := Parser.ParserCategory.kinds <$> cats.find? `tactic
    | return
  let some convs := Parser.ParserCategory.kinds <$> cats.find? `conv
    | return
  let go : M Unit :=
    getTactics ∅ (fun k => tactics.contains k || convs.contains k) cmd
  let (_, map) ← go.run {}
  let allTacs := map.toList
  logInfo <| .joinSep (allTacs.map (fun s => m!"{(headString s.2, s.2)}")) m!"\n\n"

tacs
example (u v : ℝ) : min (Int.fract u) (Int.fract (-u)) ≤ Int.fract (u + v) + Int.fract v := by
  by_contra! h
  rw [ lt_inf_iff, Int.fract_neg ] at h
  · obtain ⟨ _ | _, hz ⟩ := Int.fract_add u v
      <;> simp at hz
      <;> linarith [ Int.fract_nonneg ( u + v ), Int.fract_nonneg u, Int.fract_nonneg v ]
  · linarith [ Int.fract_nonneg ( u + v ), Int.fract_nonneg v ]

Start with the unused tactic linter and its getTactics entry point, then read the Parser parser-extension state used to find tactic and conv categories. Compare the requested module-level behavior with the provided tacs prototype and determine how the collected syntax is exposed. Done means the module's used tactics can be listed reliably, including the relevant tactic and conversion commands.