feat(algebra/lie/ideal_operations): add lemma `lie_ideal_oper_eq_line…

…ar_span'` (#11823)

It is useful to have this alternate form in situations where we have a hypothesis like `h : I = J` since we can then rewrite using `h` after applying this lemma.

An (admittedly brief) scan of the existing applications of `lie_ideal_oper_eq_linear_span` indicates that it's worth keeping both forms for convenience but I'm happy to dig deeper into this if requested.

src/algebra/lie/ideal_operations.lean

@@ -51,7 +51,8 @@ instance has_bracket : has_bracket (lie_ideal R L) (lie_submodule R L M) :=
 lemma lie_ideal_oper_eq_span :
   ⁅I, N⁆ = lie_span R L { m | ∃ (x : I) (n : N), ⁅(x : L), (n : M)⁆ = m } := rfl
 
-/-- See also `lie_submodule.lie_ideal_oper_eq_tensor_map_range`. -/
+/-- See also `lie_submodule.lie_ideal_oper_eq_linear_span'` and
+`lie_submodule.lie_ideal_oper_eq_tensor_map_range`. -/
 lemma lie_ideal_oper_eq_linear_span :
   (↑⁅I, N⁆ : submodule R M) = submodule.span R { m | ∃ (x : I) (n : N), ⁅(x : L), (n : M)⁆ = m } :=
 begin
@@ -72,6 +73,19 @@ begin
   { rw lie_ideal_oper_eq_span, apply submodule_span_le_lie_span, },
 end
 
+lemma lie_ideal_oper_eq_linear_span' :
+  (↑⁅I, N⁆ : submodule R M) = submodule.span R { m | ∃ (x ∈ I) (n ∈ N), ⁅x, n⁆ = m } :=
+begin
+  rw lie_ideal_oper_eq_linear_span,
+  congr,
+  ext m,
+  split,
+  { rintros ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩,
+    exact ⟨x, hx, n, hn, rfl⟩, },
+  { rintros ⟨x, hx, n, hn, rfl⟩,
+    exact ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, },
+end
+
 lemma lie_coe_mem_lie (x : I) (m : N) : ⁅(x : L), (m : M)⁆ ∈ ⁅I, N⁆ :=
 by { rw lie_ideal_oper_eq_span, apply subset_lie_span, use [x, m], }