theorem LieIdeal.coe_bracket {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : ↥I) : ↑⁅x, y⁆ = ⁅↑x, ↑y⁆