chore: deprime induction for localizations and quotients

[Parcly-Taxel]

All these removed instances of induction' generate only one subgoal. In some cases obtain can be used.

The relevant instances were identified by adding the following to Mathlib.Tactic.Cases

diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..08c06520879 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
         g.assign result.elimApp
         let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
           (generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+        let body ← inferType targets[0]!
+        let names : Array Format := if withArg.1.getArgs.size > 1 then
+          (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+        let gens : Array Format := if genArg.1.getArgs.size > 1 then
+          (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+        let inductor : Format := if usingArg.1.getArgs.size > 1 then
+          Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+        if subgoals.toList.length ≤ 1 then
+          logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+            {subgoals.toList.length}"
         setGoals <| (subgoals ++ result.others).toList ++ gs
 
 /-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving

and then examining the output.

[github-actions]

PR summary 7deb334c5f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Coming here from PR triage: it looks like there is disagreement with some of these changes. (Some of this might be blocked on core improvements, other on zulip discussion - or the author reverting the controversial changes.)

[Parcly-Taxel]

Coming here from PR triage: it looks like there is disagreement with some of these changes. (Some of this might be blocked on core improvements, other on zulip discussion - or the author reverting the controversial changes.)

Resolved, using the new induction syntax.

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.