Zulip Chat Archive
Stream: lean4
Topic: tactics similar to byContradiction
Klama (Jul 12 2024 at 12:20):
Is there any tactics similar to byContradiction in Lean4?
Johan Commelin (Jul 12 2024 at 12:24):
Several: by_contra or contrapose (both also have a ! variant)
Johan Commelin (Jul 12 2024 at 12:24):
Aah, you might need mathlib for some of these
Last updated: May 02 2025 at 03:31 UTC