mathlib

5ac79a63 - feat(algebra/lie/tensor_product): prove `lie_submodule.lie_ideal_oper_eq_tensor_map_range` (#7313)

feat(algebra/lie/tensor_product): prove `lie_submodule.lie_ideal_oper_eq_tensor_map_range` (#7313) The lemma `coe_lift_lie_eq_lift_coe` also introduced here is an unrelated change but is a stronger form of `lift_lie_apply` that is worth having. See also this [Zulip remark](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60linear_map.2Erange_eq_map.60.20vs.20.60submodule.2Emap_top.60/near/235845192) concerning the proposed library note.