Commit 2024-09-24 21:52 652d1bd7

chore(Algebra.Lie): do not always coerce a LieSubmodule to a Submodule to get a type (#16509) 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.