Commit 2024-08-29 03:11 5b11a94a

chore: do not directly import Tactic.Cases (#16198) This entails replacing not only induction' by its unprimed variant, but also cases' by cases/rcases/obtain. This reduces the number of imports for some files.