diff --git a/Mathlib/Algebra/Lie/Ideal.lean b/Mathlib/Algebra/Lie/Ideal.lean
index c7bdf292d59f00..6fd2210fcd1161 100644
--- a/Mathlib/Algebra/Lie/Ideal.lean
+++ b/Mathlib/Algebra/Lie/Ideal.lean
@@ -72,6 +72,12 @@ theorem LieIdeal.toLieSubalgebra_toSubmodule (I : LieIdeal R L) :
     ((I : LieSubalgebra R L) : Submodule R L) = LieSubmodule.toSubmodule I :=
   rfl
 
+instance LieIdeal.bracket {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L]
+    (I : LieIdeal R L) [Bracket L M] : Bracket I M where
+  bracket x m := ⁅(x : L), m⁆
+
+instance (priority := 2000) (I : LieIdeal R L) : Bracket I I := inferInstance
+
 /-- An ideal of `L` is a Lie subalgebra of `L`, so it is a Lie ring. -/
 instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I :=
   inferInstanceAs <| LieRing I.toLieSubalgebra