Find why something depends on which axioms

This code is by Kyle Miller from https://is.gd/Ug5sXu

Importing this file provides a comment #axiom_blame that creates output like this:

#axiom_blame interpolation

'interpolation' depends on axioms:

* Quot.sound: interpolation → Interpolant → Vocab → Finset → Finset.mk → Multiset.Nodup → Multiset.Nodup._proof_1 → List.Perm.nodup_iff → List.Perm.pairwise_iff → List.pairwise_middle → List.pairwise_append → forall_congr → funext → Quot.sound

* Classical.choice: interpolation → Interpolant → Finset.instPartialOrder → Finset.instSetLike → Finset.instSetLike._proof_1 → Multiset.Nodup.ext → List.perm_ext_iff_of_nodup → Classical.propDecidable → Classical.choice

* propext: interpolation → Interpolant → Vocab → Finset → Finset.mk → Multiset.Nodup → Multiset.Nodup._proof_1 → propext
Theorem.lean:54:0

structure CollectAxiomBlame.State : Type

• visited : Lean.NameSet
• axioms : Lean.NameMap (List Lean.Name)

@[reducible, inline]

abbrev CollectAxiomBlame.M (α : Type) : Type

Equations

• CollectAxiomBlame.M = ReaderT Lean.Environment (StateM CollectAxiomBlame.State)

partial def CollectAxiomBlame.collect (src : List Lean.Name) (c : Lean.Name) : M Unit

def «command#axiom_blame_» : Lean.ParserDescr

Equations

• «command#axiom_blame_» = Lean.ParserDescr.node `«command#axiom_blame_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#axiom_blame ") (Lean.ParserDescr.const `ident))