refactor: migrate to dependent induction lemmas

[j-loreaux]

---

[github-actions]

PR summary 309fd33d76

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

-- closure_induction'
--++ closure_induction
--++ closure_induction₂

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.

[eric-wieser]

I'm curious if you can drop the (subset_closure hz) here; I think it can be found by unification?

[eric-wieser]

Suggested change

	(mul_left : ∀ x hx y hy z hz , p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
	(mul_right : ∀ x hx y hy z hz , p z x hz hx → p z y hz hy → p z (x * y) hz (mul_mem hx hy))
	(mul_left : ∀ x hx y hy z hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
	(mul_right : ∀ x hx y hy z hz, p z x hz hx → p z y hz hy → p z (x * y) hz (mul_mem hx hy))

[b-mehta]

It's great that we add these dependent induction lemmas, but I think it's sometimes nice to also have access to the non-dependent ones, since they're sometimes easier to work with. For example, when it's necessary to specify the motive to a dependent induction in the case where the application is not dependent, you often end up with things looking syntactically really confusing. I'd personally slightly prefer keeping the old ones around, under other names. But if it turns out that adjusting mathlib to your change is easy enough, then it's probably fine...

[eric-wieser]

You should never have to specify the motive explicitly though? Usually when you do, this is because:

• The induction principle was not dependent, and should have been
• The induction principle has the arguments in the wrong order
• elab_as_elim is missing from the theorem
• You tried to use apply with an elab_as_elim