[Merged by Bors] - chore(Algebra.Lie): do not always coerce a LieSubmodule to a Submodule to get a type

[mattrobball]

We add

instance (priority := high) coeSort : CoeSort (LieSubmodule R L M) (Type w) where
  coe N := { x : M // x ∈ N }

to avoid the coercion to a Sort being { x : M // x ∈ N.toSubmodule } and instead be N itself.

This allows removal of all adapation_notes from leanprover/lean4#5020.

Ultimately the API here should be expanded and Coe (LieSubmodule R L M) (Submodule R M)
should be minimized or removed to avoid forcing Lean to unify LieSubmodule and Submodule unnecessarily.

---

[github-actions]

PR summary c170d9258e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Lie.Subalgebra	1011	1224	+213 (+21.07%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Lie.Subalgebra	213

---

Declarations diff

+ instUniqueBot
+ instance (L' : LieSubalgebra R L) [IsArtinian R L] : IsArtinian R L'
+ instance (priority := high) coeSort : CoeSort (LieSubmodule R L M) (Type w)
+ instance (priority := mid) coeSubmodule : CoeOut (LieSubmodule R L M) (Submodule R M)
+ instance : Unique {x // x ∈ (⊥ : LieIdeal R L)}
+ instance [IsArtinian R M] (N : LieSubmodule R L M) : IsArtinian R N
+ instance [IsNoetherian R M] (N : LieSubmodule R L M) : IsNoetherian R N
+ instance [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R N
- coeSubmodule
- instCanLiftSubmoduleLieSubmodule
- instance : Module R N
- instance {S : Type*} [Semiring S] [SMul S R] [SMul Sᵐᵒᵖ R] [Module S M] [Module Sᵐᵒᵖ M]
- module'

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.

[mattrobball]

!bench

[mattrobball]

This could probably be moved downstream to avoid additional imports.

[ocfnash]

Agreed but I'm fine with the import bump if you are.

[leanprover-bot]

Here are the benchmark results for commit 0c698ba.
There were significant changes against commit 82e0419:

  Benchmark                             Metric         Change
  ===========================================================
- ~Mathlib.Algebra.Lie.Abelian          instructions    49.8%
- ~Mathlib.Algebra.Lie.Submodule        instructions    17.4%
- ~Mathlib.Algebra.Lie.TensorProduct    instructions    23.0%
- ~Mathlib.Algebra.Lie.TraceForm        instructions    12.1%
- ~Mathlib.Algebra.Lie.Weights.Basic    instructions    20.8%
- ~Mathlib.Algebra.Lie.Weights.Cartan   instructions    25.4%
- ~Mathlib.Algebra.Lie.Weights.Chain    instructions    18.6%
- ~Mathlib.Algebra.Lie.Weights.Linear   instructions    41.8%

[mattrobball]

I suspect this will reverse if the coercion from LieSubmodule to Submodule is removed (or minimized) but that is a bit of work.

[ocfnash]

I haven't forgotten about this PR, I'm just very busy but I will get to it soon.

[ocfnash]

Thanks for all this work.

bors d+

[ocfnash]

Agreed but I'm fine with the import bump if you are.

[mathlib-bors]

✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mattrobball]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style