proving tautologies

Stream: general

[Meow]

Are there some tactic in lean3 to automatically prove simple first-order logic tautologies?

[Meow]

In Isabelle there is blast, and Sledgehammer.

[Mario Carneiro]

There is an old lean 3 implementation called super that never seriously got use, which is planned for upgrading and porting to lean 4. Beyond that, the nearest alternatives are tauto and finish

[Notification Bot]

This topic was moved here from #lean4 > Pattern matching lambda body in conv by Scott Morrison

[Scott Morrison]

(@Meow, welcome to zulip! I moved your question to its own thread.)