Zulip Chat Archive
Stream: new members
Topic: Equivalent of `inversion` tactic?
McCoy R. Becker (Dec 28 2023 at 07:27):
Is there an inversion-like hammer for destructuring inductive datatypes in Lean's library of tactics?
Kevin Buzzard (Dec 28 2023 at 12:02):
cases?
Last updated: May 02 2025 at 03:31 UTC