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: Dec 20 2025 at 21:32 UTC