instance UniversalEnvelopingAlgebra.instIsTwoSidedSpanImageCoeLieHomιCoeLieIdeal_ado {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : (Ideal.span (⇑(ι R) '' ↑I)).IsTwoSided