R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ IsLieAbelian { x // x ∈ ↑I } ↔ ∀ (y : L) (x : { x // x ∈ I }) (x_1 : { x // x ∈ I }), ⁅↑x, ↑x_1⁆ = y → y = 0
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ IsLieAbelian { x // x ∈ ↑I } ↔ ⁅I, I⁆ = ⊥
simp only [_root_.eq_bot_iff, lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le,
  LieSubmodule.bot_coe, Set.subset_singleton_iff, Set.mem_setOf_eq, exists_imp]
no goals
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ IsLieAbelian { x // x ∈ ↑I } ↔ ∀ (y : L) (x : { x // x ∈ I }) (x_1 : { x // x ∈ I }), ⁅↑x, ↑x_1⁆ = y → y = 0
refine'
  ⟨fun h z x y hz =>
    hz.symm.trans
      (((I : LieSubalgebra R L).coe_bracket x y).symm.trans
        ((coe_zero_iff_zero _ _).mpr (by apply h.trivial))),
    fun h => ⟨fun x y => ((I : LieSubalgebra R L).coe_zero_iff_zero _).mp (h _ x y rfl)⟩⟩
no goals
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
h : IsLieAbelian { x // x ∈ ↑I }
z : L
x : { x // x ∈ I }
y : { x // x ∈ I }
hz : ⁅↑x, ↑y⁆ = z
⊢ ⁅x, y⁆ = 0
apply h.trivial