fix(data/set_like): coe_sort_trans should have low priority (#15489)

In core Lean, `coe_sort_trans` is given default priority, meaning it takes precedence over `set_like.has_coe_to_sort`. As a consequence, sometimes a weird instance path was chosen, such as `submodule R M → Module R → Type*` rather than the direct path `submodule R M → Type*`, and I believe this can lead to diamonds (including weird universe levels), and in any case to weird defeq checks (which are made extra expensive by occurring in the type). In fact, there are quite a few `has_coe_to_sort` instances that would be useless since they are preceded by a `has_coe`, e.g. `lie_ideal`.

Lowering the priority of `coe_sort_trans` below that of `set_like.has_coe_to_sort` should ensure we use the preferred inheritance path. We did the same thing for `coe_fn_trans` in `fun_like/basic.lean`.

The consequence is that certain places that (ab)used the weird coercion paths will need to be slightly redefined to use the new path, basically inserting unification hints manually. Those paths were slightly fragile anyway so I don't think that's an important loss compared to the advantages of clarifying.

src/algebra/lie/abelian.lean

@@ -274,9 +274,9 @@ lemma lie_submodule.lie_abelian_iff_lie_self_eq_bot : is_lie_abelian I ↔ ⁅I,
 begin
   simp only [_root_.eq_bot_iff, lie_ideal_oper_eq_span, lie_submodule.lie_span_le,
     lie_submodule.bot_coe, set.subset_singleton_iff, set.mem_set_of_eq, exists_imp_distrib],
-  refine ⟨λ h z x y hz, hz.symm.trans ((lie_subalgebra.coe_bracket _ _ _).symm.trans
+  refine ⟨λ h z x y hz, hz.symm.trans (((I : lie_subalgebra R L).coe_bracket x y).symm.trans
     ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
-    λ h, ⟨λ x y, (coe_zero_iff_zero _ _).mp (h _ x y rfl)⟩⟩,
+    λ h, ⟨λ x y, ((I : lie_subalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩,
 end
 
 end ideal_operations

src/algebra/lie/ideal_operations.lean

@@ -105,7 +105,7 @@ begin
   suffices : ∀ (I J : lie_ideal R L), ⁅I, J⁆ ≤ ⁅J, I⁆, { exact le_antisymm (this I J) (this J I), },
   clear I J, intros I J,
   rw [lie_ideal_oper_eq_span, lie_span_le], rintros x ⟨y, z, h⟩, rw ← h,
-  rw [← lie_skew, ← lie_neg, ← submodule.coe_neg],
+  rw [← lie_skew, ← lie_neg, ← lie_submodule.coe_neg],
   apply lie_coe_mem_lie,
 end
 

src/algebra/lie/nilpotent.lean

@@ -535,10 +535,10 @@ begin
     split,
     { rintros ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩,
       erw [← lie_submodule.mem_coe_submodule, ih, lie_submodule.mem_coe_submodule] at hz,
-      exact ⟨⟨lie_submodule.quotient.mk y, submodule.mem_top⟩, ⟨z, hz⟩, rfl⟩, },
+      exact ⟨⟨lie_submodule.quotient.mk y, lie_submodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩, },
     { rintros ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩,
       erw [← lie_submodule.mem_coe_submodule, ← ih, lie_submodule.mem_coe_submodule] at hz,
-      exact ⟨⟨y, submodule.mem_top⟩, ⟨z, hz⟩, rfl⟩, }, },
+      exact ⟨⟨y, lie_submodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩, }, },
 end
 
 /-- Note that the below inequality can be strict. For example the ideal of strictly-upper-triangular
@@ -551,7 +551,7 @@ begin
   { simp only [lie_module.lower_central_series_succ, lie_submodule.lie_ideal_oper_eq_linear_span],
     apply submodule.span_mono,
     rintros x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩,
-    exact ⟨⟨y.val, submodule.mem_top⟩, ⟨z, ih hz⟩, rfl⟩, },
+    exact ⟨⟨y.val, lie_submodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩, },
 end
 
 /-- A central extension of nilpotent Lie algebras is nilpotent. -/
@@ -671,7 +671,7 @@ begin
   { simp, },
   { simp_rw [lower_central_series_succ, lcs_succ, lie_submodule.lie_ideal_oper_eq_linear_span',
       ← (I.lcs M k).mem_coe_submodule, ih, lie_submodule.mem_coe_submodule,
-      lie_submodule.mem_top, exists_true_left, lie_subalgebra.coe_bracket_of_module],
+      lie_submodule.mem_top, exists_true_left, (I : lie_subalgebra R L).coe_bracket_of_module],
     congr,
     ext m,
     split,

src/algebra/lie/of_associative.lean

@@ -222,7 +222,7 @@ by simpa using N.lie_mem hm
 
 @[simp] lemma to_endomorphism_restrict_eq_to_endomorphism
   (h := N.to_endomorphism_comp_subtype_mem x) :
-  ((to_endomorphism R L M x).restrict h : N →ₗ[R] N) = to_endomorphism R L N x :=
+  ((to_endomorphism R L M x).restrict h : (N : submodule R M) →ₗ[R] N) = to_endomorphism R L N x :=
 by { ext, simp [linear_map.restrict_apply], }
 
 end lie_submodule

src/algebra/lie/subalgebra.lean

@@ -87,6 +87,9 @@ instance [has_smul R₁ R] [module R₁ L] [is_scalar_tower R₁ R L]
   (L' : lie_subalgebra R L) : is_scalar_tower R₁ R L' :=
 L'.to_submodule.is_scalar_tower
 
+instance (L' : lie_subalgebra R L) [is_noetherian R L] : is_noetherian R L' :=
+is_noetherian_submodule' ↑L'
+
 end
 
 /-- A Lie subalgebra forms a new Lie algebra. -/
@@ -401,7 +404,7 @@ by { rw eq_bot_iff, exact iff.rfl, }
 lemma subsingleton_of_bot : subsingleton (lie_subalgebra R ↥(⊥ : lie_subalgebra R L)) :=
 begin
   apply subsingleton_of_bot_eq_top,
-  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw submodule.mem_bot at hx, subst hx,
+  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw lie_subalgebra.mem_bot at hx, subst hx,
   simp only [true_iff, eq_self_iff_true, submodule.mk_eq_zero, mem_bot],
 end
 

src/algebra/lie/submodule.lean

@@ -178,6 +178,28 @@ instance : has_coe (lie_ideal R L) (lie_subalgebra R L) := ⟨λ I, lie_ideal_su
 @[norm_cast] lemma lie_ideal.coe_to_lie_subalgebra_to_submodule (I : lie_ideal R L) :
   ((I : lie_subalgebra R L) : submodule R L) = I := rfl
 
+/-- An ideal of `L` is a Lie subalgebra of `L`, so it is a Lie ring. -/
+instance lie_ideal.lie_ring (I : lie_ideal R L) : lie_ring I := lie_subalgebra.lie_ring R L ↑I
+
+/-- Transfer the `lie_algebra` instance from the coercion `lie_ideal → lie_subalgebra`. -/
+instance lie_ideal.lie_algebra (I : lie_ideal R L) : lie_algebra R I :=
+lie_subalgebra.lie_algebra R L ↑I
+
+/-- Transfer the `lie_module` instance from the coercion `lie_ideal → lie_subalgebra`. -/
+instance lie_ideal.lie_ring_module {R L : Type*} [comm_ring R] [lie_ring L] [lie_algebra R L]
+  (I : lie_ideal R L) [lie_ring_module L M] : lie_ring_module I M :=
+lie_subalgebra.lie_ring_module (I : lie_subalgebra R L)
+
+@[simp]
+theorem lie_ideal.coe_bracket_of_module {R L : Type*} [comm_ring R] [lie_ring L] [lie_algebra R L]
+  (I : lie_ideal R L) [lie_ring_module L M] (x : I) (m : M) :
+  ⁅x,m⁆ = ⁅(↑x : L),m⁆ :=
+lie_subalgebra.coe_bracket_of_module (I : lie_subalgebra R L) x m
+
+/-- Transfer the `lie_module` instance from the coercion `lie_ideal → lie_subalgebra`. -/
+instance lie_ideal.lie_module (I : lie_ideal R L) : lie_module R I M :=
+lie_subalgebra.lie_module (I : lie_subalgebra R L)
+
 end lie_ideal
 
 variables {R M}
@@ -355,7 +377,7 @@ by { rw eq_bot_iff, exact iff.rfl, }
 lemma subsingleton_of_bot : subsingleton (lie_submodule R L ↥(⊥ : lie_submodule R L M)) :=
 begin
   apply subsingleton_of_bot_eq_top,
-  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw submodule.mem_bot at hx, subst hx,
+  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw lie_submodule.mem_bot at hx, subst hx,
   simp only [true_iff, eq_self_iff_true, submodule.mk_eq_zero, lie_submodule.mem_bot],
 end
 
@@ -645,10 +667,10 @@ different (though the latter does naturally inject into the former).
 In other words, in general, ideals of `I`, regarded as a Lie algebra in its own right, are not the
 same as ideals of `L` contained in `I`. -/
 -- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_bot : subsingleton (lie_ideal R ↥(⊥ : lie_ideal R L)) :=
+lemma subsingleton_of_bot : subsingleton (lie_ideal R (⊥ : lie_ideal R L)) :=
 begin
   apply subsingleton_of_bot_eq_top,
-  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw submodule.mem_bot at hx, subst hx,
+  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw lie_submodule.mem_bot at hx, subst hx,
   simp only [true_iff, eq_self_iff_true, submodule.mk_eq_zero, lie_submodule.mem_bot],
 end
 
@@ -851,7 +873,8 @@ def incl : I →ₗ⁅R⁆ L := (I : lie_subalgebra R L).incl
 @[simp] lemma incl_coe : (I.incl : I →ₗ[R] L) = (I : submodule R L).subtype := rfl
 
 @[simp] lemma comap_incl_self : comap I.incl I = ⊤ :=
-by { rw ← lie_submodule.coe_to_submodule_eq_iff, exact submodule.comap_subtype_self _, }
+by rw [← lie_submodule.coe_to_submodule_eq_iff, lie_submodule.top_coe_submodule,
+ lie_ideal.comap_coe_submodule, lie_ideal.incl_coe, submodule.comap_subtype_self]
 
 @[simp] lemma ker_incl : I.incl.ker = ⊥ :=
 by rw [← lie_submodule.coe_to_submodule_eq_iff, I.incl.ker_coe_submodule,

src/algebra/lie/weights.lean

@@ -250,10 +250,10 @@ lemma is_nilpotent_to_endomorphism_weight_space_zero
 begin
   obtain ⟨k, hk⟩ := exists_pre_weight_space_zero_le_ker_of_is_noetherian R M x,
   use k,
-  ext ⟨m, hm : m ∈ pre_weight_space M 0⟩,
+  ext ⟨m, hm⟩,
   rw [linear_map.zero_apply, lie_submodule.coe_zero, submodule.coe_eq_zero,
     ← lie_submodule.to_endomorphism_restrict_eq_to_endomorphism, linear_map.pow_restrict,
-    ← set_like.coe_eq_coe, linear_map.restrict_apply, submodule.coe_mk, lie_submodule.coe_zero],
+    ← set_like.coe_eq_coe, linear_map.restrict_apply, submodule.coe_mk, submodule.coe_zero],
   exact hk hm,
 end
 

src/group_theory/sylow.lean

@@ -72,7 +72,13 @@ instance : subgroup_class (sylow p G) G :=
   one_mem := λ s, s.one_mem',
   inv_mem := λ s, s.inv_mem' }
 
-variables (P : sylow p G) {K : Type*} [group K] (ϕ : K →* G) {N : subgroup G}
+variables (P : sylow p G)
+
+/-- The action by a Sylow subgroup is the action by the underlying group. -/
+instance mul_action_left {α : Type*} [mul_action G α] : mul_action P α :=
+subgroup.mul_action ↑P
+
+variables {K : Type*} [group K] (ϕ : K →* G) {N : subgroup G}
 
 /-- The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup. -/
 def comap_of_ker_is_p_group (hϕ : is_p_group p ϕ.ker) (h : ↑P ≤ ϕ.range) : sylow p K :=

src/logic/basic.lean

@@ -99,6 +99,10 @@ theorem coe_fn_coe_base'
   {α β} {γ : out_param $ _} [has_coe α β] [has_coe_to_fun β (λ _, γ)]
   (x : α) : @coe_fn α _ _ x = @coe_fn β _ _ x := rfl
 
+-- This instance should have low priority, to ensure we follow the chain
+-- `set_like → has_coe_to_sort`
+attribute [instance, priority 10] coe_sort_trans
+
 theorem coe_sort_coe_trans
   {α β γ δ} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ δ]
   (x : α) : @coe_sort α _ _ x = @coe_sort β _ _ x := rfl

src/model_theory/elementary_maps.lean

@@ -314,6 +314,9 @@ instance : set_like (L.elementary_substructure M) M :=
   exact h,
 end⟩
 
+instance induced_Structure (S : L.elementary_substructure M) : L.Structure S :=
+substructure.induced_Structure
+
 @[simp] lemma is_elementary (S : L.elementary_substructure M) :
   (S : L.substructure M).is_elementary := S.is_elementary'
 

src/ring_theory/fractional_ideal.lean

@@ -141,6 +141,10 @@ end set_like
 @[simp, norm_cast] lemma coe_mk (I : submodule R P) (hI : is_fractional S I) :
   (subtype.mk I hI : submodule R P) = I := rfl
 
+/-! Transfer instances from `submodule R P` to `fractional_ideal S P`. --/
+instance (I : fractional_ideal S P) : add_comm_group I := submodule.add_comm_group ↑I
+instance (I : fractional_ideal S P) : module R I := submodule.module ↑I
+
 lemma coe_to_submodule_injective :
   function.injective (coe : fractional_ideal S P → submodule R P) :=
 subtype.coe_injective