chore: move #help to Batteries (batteries#969)

[fgdorais]

---

Once batteries#969 is merged:

• Edit lakefile to point batteries back to main
• Run lake update batteries
• Merge

[github-actions]

PR summary 5ca07e27b7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.HelpCmd	18	0	-18 (-100.00%)
Mathlib.Tactic.Common	243	241	-2 (-0.82%)
Mathlib.Tactic	2279	2277	-2 (-0.09%)

Import changes for all files

Files	Import difference
There are 4322 files with changed transitive imports taking up over 182682 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

- foo

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[fgdorais]

@kim-em We added #help to batteries but we forgot to delete it from Mathlib. This PR completes the task.