Lean4
instance lieQuotientLieRing : LieRing (L ⧸ I)
where
add_lie := by
intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
repeat'
first
| rw [is_quotient_mk]
| rw [← mk_bracket]
| rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
apply congr_arg; apply add_lie
lie_add := by
intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
repeat'
first
| rw [is_quotient_mk]
| rw [← mk_bracket]
| rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
apply congr_arg; apply lie_add
lie_self := by
intro x'; refine Quotient.inductionOn' x' ?_; intro x
rw [is_quotient_mk, ← mk_bracket]
apply congr_arg; apply lie_self
leibniz_lie := by
intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
repeat'
first
| rw [is_quotient_mk]
| rw [← mk_bracket]
| rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
apply congr_arg; apply leibniz_lie
