chore(algebra/lie/quotient): golf some instances (#14480)

src/algebra/lie/quotient.lean

@@ -59,42 +59,33 @@ instance inhabited : inhabited (M ⧸ N) := ⟨0⟩
 lie_submodule of the lie_module `N`. -/
 abbreviation mk : M → M ⧸ N := submodule.quotient.mk
 
-lemma is_quotient_mk (m : M) :
-  quotient.mk' m = (mk m : M ⧸ N) := rfl
+lemma is_quotient_mk (m : M) : quotient.mk' m = (mk m : M ⧸ N) := rfl
 
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
 is a natural linear map from `L` to the endomorphisms of `M` leaving `N` invariant. -/
 def lie_submodule_invariant : L →ₗ[R] submodule.compatible_maps N.to_submodule N.to_submodule :=
-  linear_map.cod_restrict _ (lie_module.to_endomorphism R L M) N.lie_mem
+linear_map.cod_restrict _ (lie_module.to_endomorphism R L M) N.lie_mem
 
 variables (N)
 
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
 is a natural Lie algebra morphism from `L` to the linear endomorphism of the quotient `M/N`. -/
 def action_as_endo_map : L →ₗ⁅R⁆ module.End R (M ⧸ N) :=
-{ map_lie' := λ x y, by { ext m,
-                          change mk ⁅⁅x, y⁆, m⁆ = mk (⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆),
-                          congr, apply lie_lie, },
+{ map_lie' := λ x y, submodule.linear_map_qext _ $ linear_map.ext $ λ m,
+    congr_arg mk $ lie_lie _ _ _,
   ..linear_map.comp (submodule.mapq_linear (N : submodule R M) ↑N) lie_submodule_invariant }
 
 /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there is
 a natural bracket action of `L` on the quotient `M/N`. -/
-def action_as_endo_map_bracket : has_bracket L (M ⧸ N) := ⟨λ x n, action_as_endo_map N x n⟩
+instance action_as_endo_map_bracket : has_bracket L (M ⧸ N) := ⟨λ x n, action_as_endo_map N x n⟩
 
 instance lie_quotient_lie_ring_module : lie_ring_module L (M ⧸ N) :=
-{ bracket     := λ x n, (action_as_endo_map N : L →ₗ[R] module.End R (M ⧸ N)) x n,
-  add_lie     := λ x y n, by { simp only [linear_map.map_add, linear_map.add_apply], },
-  lie_add     := λ x m n, by { simp only [linear_map.map_add, linear_map.add_apply], },
-  leibniz_lie := λ x y m, show action_as_endo_map _ _ _ = _,
-  { simp only [lie_hom.map_lie, lie_ring.of_associative_ring_bracket, sub_add_cancel,
-      lie_hom.coe_to_linear_map, linear_map.mul_apply, linear_map.sub_apply], } }
+{ bracket := has_bracket.bracket,
+  ..lie_ring_module.comp_lie_hom _ (action_as_endo_map N) }
 
 /-- The quotient of a Lie module by a Lie submodule, is a Lie module. -/
 instance lie_quotient_lie_module : lie_module R L (M ⧸ N) :=
-{ smul_lie := λ t x m, show (_ : L →ₗ[R] module.End R (M ⧸ N)) _ _ = _,
-  { simp only [linear_map.map_smul], refl, },
-  lie_smul := λ x t m, show (_ : L →ₗ[R] module.End R (M ⧸ N)) _ _ = _,
-  { simp only [linear_map.map_smul], refl, }, }
+lie_module.comp_lie_hom _ (action_as_endo_map N)
 
 instance lie_quotient_has_bracket : has_bracket (L ⧸ I) (L ⧸ I) :=
 ⟨begin