Search code examples
debuggingmaththeorem-provinglean

Trace tauto, finish

Is there a way to trace tauto, finish tactics (or others that don't fall into simp) in Lean? E.g.

example (P Q : Prop) : a → b ↔ ¬a ∨ b := by tauto

I'd like to see the neccesary rewritings or theorems that are applied to the terms to prove the goal, in order to use them explicitly in more complex situations.

Solution 
  • import tactic

theorem foo (a b : Prop) : a → b ↔ ¬a ∨ b := by tauto!

#print foo

    shows you the term that the tactic created. But high-powered tactics are not designed to produce readable terms, so your mileage may vary.