Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

Necessary because of:
#6528
#6499

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

These work on the command line and therefore didn't fail in CI (as `lake env lean blah.lean` doesn't pick up the extra lean args?) but as soon as you open one of these files in vscode you get a sea of red errors.

I tried to fix a couple in a minimal way, if there was just for example one universe level missing, for most files the "fix" for now is just reenabling autoimplicits for the file.
This revealed a couple of tests that were incorrectly using an implicit type when they thought they were using Nat.
Two files had issues, that we may want to follow up on  `test/superscript.lean` which failed even with autoimplicits turned on when using an autoimplicit superscript variable (unsure if this was intentional).
And the `ToExpr` deriving handler seems to rely on autoimplicits somehow to work properly in the presence of universe, if an explicit universe variable is added there is still an error.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.

These work on the command line and therefore didn't fail in CI (as `lake env lean blah.lean` doesn't pick up the extra lean args?) but as soon as you open one of these files in vscode you get a sea of red errors.

I tried to fix a couple in a minimal way, if there was just for example one universe level missing, for most files the "fix" for now is just reenabling autoimplicits for the file.
This revealed a couple of tests that were incorrectly using an implicit type when they thought they were using Nat.
Two files had issues, that we may want to follow up on  `test/superscript.lean` which failed even with autoimplicits turned on when using an autoimplicit superscript variable (unsure if this was intentional).
And the `ToExpr` deriving handler seems to rely on autoimplicits somehow to work properly in the presence of universe, if an explicit universe variable is added there is still an error.

Autoimplicits are [highly controversial](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil/near/355142480) and also [defeat the performance-improving work](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/autoimplicit.20and.20Type*/near/383878932) in #6474.

The intent of this PR is to make `autoImplicit` opt-in on a per-file basis, by disabling it in the lakefile and enabling it again with `set_option autoImplicit true` in the few files that rely on it.

That also keeps this PR small, as opposed to attempting to "fix" files to not need it any more.

I claim that many of the uses of `autoImplicit` in these files are accidental; situations such as:

* Assuming `variables` are in scope, but pasting the lemma in the wrong section
* Pasting in a lemma from a scratch file without checking to see if the variable names are consistent with the rest of the file
* Making a copy-paste error between lemmas and forgetting to add an explicit arguments.

Having `set_option autoImplicit false` as the default prevents these types of mistake being made in the 90% of files where `autoImplicit`s are not used at all, and causes them to be caught by CI during review.

I think there were various points during the port where we encouraged porters to delete the `universes u v` lines; I think having autoparams for universe variables only would cover a lot of the cases we actually use them, while avoiding any real shortcomings.

[A Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143) (after combining overlapping votes accordingly) was in favor of this change with `5:5:18` as the `no:dontcare:yes` vote ratio.

While this PR was being reviewed, a handful of files gained some more likely-accidental autoImplicits. In these places, `set_option autoImplicit true` has been placed locally within a section, rather than at the top of the file.