This adds Kyle Miller's elaborators for `Type*` and `Sort*` which provide implicit universe variables.

It also includes a few tests.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

This adds Kyle Miller's elaborators for `Type*` and `Sort*` which provide implicit universe variables.

It also includes a few tests.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

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.

This adds Kyle Miller's elaborators for `Type*` and `Sort*` which provide implicit universe variables.

It also includes a few tests.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

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.

We clean up heart beat bumps after #6474.

We clean up heart beat bumps after #6474.

We clean up heart beat bumps after #6474.

We clean up heart beat bumps after #6474.