induction/cases code action

Stream: mathlib4

[Floris van Doorn]

I noticed that the induction/cases code action that suggests a pattern is not imported anymore in most of Mathlib. This is annoying, and I think we should have it in at least Mathlib.Tactic (but probably also in something like Mathlib.Tactic.Common)

import Mathlib.Tactic
-- import Batteries.CodeAction.Misc

example (n : ℕ) : n = n := by
  induction n -- no code action (the code action exists with `import Mathlib`)

Note: I don't know that the minimal import is to get it. The code action seems to be defined in Batteries.CodeAction.Misc but importing that doesn't seem to work.

[Floris van Doorn]

The minimal import seems to be

import Batteries.CodeAction.Basic
import Batteries.CodeAction.Misc

[Floris van Doorn]

#34261

[Snir Broshi]

Mathlib/Lean/Meta.lean used to contain public import Batteries.CodeAction before the shake tool was run in #32731. Won't this new import also get removed by the shake tool?
The same happened to #lint, and required a -- shake: keep comment

[Shreyas Srinivas]

Maybe you should have a Mathlib.Initimport in every file which imports this action

[Shreyas Srinivas]

This seems to be the case in Cslib. Not importing it throws a test error

[Snir Broshi]

Shreyas Srinivas said:

Maybe you should have a Mathlib.Initimport in every file which imports this action

This is already the case in mathlib, and CI will fail if there's a file that doesn't (transitively) import it