fix(Mathlib/Algebra/Lie/DirectSum): remove unused R argument from lemmas (#8388)

This made them not actually work as a `simp` lemma.

Also extracts a common result that can be used to prove `single_add` for `DFinsupp` and `Finsupp`, and a new `Finsupp.single_mul` lemma.

Author: eric-wieser

Mathlib/Algebra/Lie/DirectSum.lean

@@ -126,6 +126,28 @@ theorem bracket_apply (x y : ⨁ i, L i) (i : ι) : ⁅x, y⁆ i = ⁅x i, y i
   zipWith_apply _ _ x y i
 #align direct_sum.bracket_apply DirectSum.bracket_apply
 
+theorem lie_of_same [DecidableEq ι] {i : ι} (x y : L i) :
+    ⁅of L i x, of L i y⁆ = of L i ⁅x, y⁆ :=
+  DFinsupp.zipWith_single_single _ _ _ _
+#align direct_sum.lie_of_of_eq DirectSum.lie_of_same
+
+theorem lie_of_of_ne [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) :
+    ⁅of L i x, of L j y⁆ = 0 := by
+  refine DFinsupp.ext fun k => ?_
+  rw [bracket_apply]
+  obtain rfl | hik := Decidable.eq_or_ne i k
+  · rw [of_eq_of_ne _ _ _ _ hij.symm, lie_zero, zero_apply]
+  · rw [of_eq_of_ne _ _ _ _ hik, zero_lie, zero_apply]
+#align direct_sum.lie_of_of_ne DirectSum.lie_of_of_ne
+
+@[simp]
+theorem lie_of [DecidableEq ι] {i j : ι} (x : L i) (y : L j) :
+    ⁅of L i x, of L j y⁆ = if hij : i = j then of L i ⁅x, hij.symm.recOn y⁆ else 0 := by
+  obtain rfl | hij := Decidable.eq_or_ne i j
+  · simp only [lie_of_same L x y, dif_pos]
+  · simp only [lie_of_of_ne L hij x y, hij, dif_neg]
+#align direct_sum.lie_of DirectSum.lie_of
+
 instance lieAlgebra : LieAlgebra R (⨁ i, L i) :=
   { (inferInstance : Module R _) with
     lie_smul := fun c x y => by
@@ -174,37 +196,6 @@ theorem lieAlgebra_ext {x y : ⨁ i, L i}
   DFinsupp.ext h
 #align direct_sum.lie_algebra_ext DirectSum.lieAlgebra_ext
 
-theorem lie_of_of_ne [DecidableEq ι] {i j : ι} (hij : j ≠ i) (x : L i) (y : L j) :
-    ⁅of L i x, of L j y⁆ = 0 := by
-  apply lieAlgebra_ext R ι L; intro k
-  rw [LieHom.map_lie]
-  simp only [of, singleAddHom, AddMonoidHom.coe_mk, ZeroHom.coe_mk, lieAlgebraComponent_apply,
-    component, lapply, LinearMap.coe_mk, AddHom.coe_mk, single_apply, LieHom.map_zero]
-  -- The next four lines were not needed before leanprover/lean4#2644
-  erw [AddMonoidHom.coe_mk, AddHom.coe_mk, ZeroHom.coe_mk]
-  rotate_left
-  intros; erw [single_add]
-  erw [single_apply, single_apply]
-  by_cases hik : i = k
-  · simp only [dif_neg, not_false_iff, lie_zero, hik.symm, hij]
-  · simp only [dif_neg, not_false_iff, zero_lie, hik]
-#align direct_sum.lie_of_of_ne DirectSum.lie_of_of_ne
-
-theorem lie_of_of_eq [DecidableEq ι] {i j : ι} (hij : j = i) (x : L i) (y : L j) :
-    ⁅of L i x, of L j y⁆ = of L i ⁅x, hij.recOn y⁆ := by
-  have : of L j y = of L i (hij.recOn y) := Eq.rec (Eq.refl _) hij
-  rw [this, ← lieAlgebraOf_apply R ι L i ⁅x, hij.recOn y⁆, LieHom.map_lie, lieAlgebraOf_apply,
-    lieAlgebraOf_apply]
-#align direct_sum.lie_of_of_eq DirectSum.lie_of_of_eq
-
-@[simp]
-theorem lie_of [DecidableEq ι] {i j : ι} (x : L i) (y : L j) :
-    ⁅of L i x, of L j y⁆ = if hij : j = i then lieAlgebraOf R ι L i ⁅x, hij.recOn y⁆ else 0 := by
-  by_cases hij : j = i
-  · simp only [lie_of_of_eq R ι L hij x y, hij, dif_pos, not_false_iff, lieAlgebraOf_apply]
-  · simp only [lie_of_of_ne R ι L hij x y, hij, dif_neg, not_false_iff]
-#align direct_sum.lie_of DirectSum.lie_of
-
 variable {R L ι}
 
 /-- Given a family of Lie algebras `L i`, together with a family of morphisms of Lie algebras
@@ -236,16 +227,14 @@ def toLieAlgebra [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'
         simp only [LinearMap.map_neg, neg_inj, ← LieAlgebra.ad_apply R]
         rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
         congr; clear x; ext j x; exact this j i x y
-      -- Tidy up and use `lie_of`.
       intro i j y x
-      simp only [lie_of R, lieAlgebraOf_apply, LieHom.coe_toLinearMap, toAddMonoid_of,
-        coe_toModule_eq_coe_toAddMonoid, LinearMap.toAddMonoidHom_coe]
+      simp only [coe_toModule_eq_coe_toAddMonoid, toAddMonoid_of]
       -- And finish with trivial case analysis.
-      rcases eq_or_ne i j with (h | h)
-      · have h' : f j (h.recOn y) = f i y := Eq.rec (Eq.refl _) h
-        simp only [h, h', LieHom.coe_toLinearMap, dif_pos, LieHom.map_lie, toAddMonoid_of,
-          LinearMap.toAddMonoidHom_coe]
-      · simp only [h, hf j i h.symm x y, dif_neg, not_false_iff, AddMonoidHom.map_zero] }
+      obtain rfl | hij := Decidable.eq_or_ne i j
+      · simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
+          LieHom.map_lie]
+      · simp_rw [lie_of_of_ne _ hij.symm, map_zero,  LinearMap.toAddMonoidHom_coe,
+          LieHom.coe_toLinearMap, hf j i hij.symm x y] }
 #align direct_sum.to_lie_algebra DirectSum.toLieAlgebra
 
 end Algebras

Mathlib/Data/DFinsupp/Basic.lean

@@ -746,6 +746,21 @@ theorem equivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : β i) :
   simp only [← single_eq_pi_single, equivFunOnFintype_symm_coe]
 #align dfinsupp.equiv_fun_on_fintype_symm_single DFinsupp.equivFunOnFintype_symm_single
 
+section SingleAndZipWith
+
+variable [∀ i, Zero (β₁ i)] [∀ i, Zero (β₂ i)]
+@[simp]
+theorem zipWith_single_single (f : ∀ i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0)
+    {i} (b₁ : β₁ i) (b₂ : β₂ i) :
+      zipWith f hf (single i b₁) (single i b₂) = single i (f i b₁ b₂) := by
+  ext j
+  rw [zipWith_apply]
+  obtain rfl | hij := Decidable.eq_or_ne i j
+  · rw [single_eq_same, single_eq_same, single_eq_same]
+  · rw [single_eq_of_ne hij, single_eq_of_ne hij, single_eq_of_ne hij, hf]
+
+end SingleAndZipWith
+
 /-- Redefine `f i` to be `0`. -/
 def erase (i : ι) (x : Π₀ i, β i) : Π₀ i, β i :=
   ⟨fun j ↦ if j = i then 0 else x.1 j,
@@ -885,11 +900,7 @@ variable [∀ i, AddZeroClass (β i)]
 
 @[simp]
 theorem single_add (i : ι) (b₁ b₂ : β i) : single i (b₁ + b₂) = single i b₁ + single i b₂ :=
-  ext fun i' => by
-    by_cases h : i = i'
-    · subst h
-      simp only [add_apply, single_eq_same]
-    · simp only [add_apply, single_eq_of_ne h, zero_add]
+  (zipWith_single_single (fun _ => (· + ·)) _ b₁ b₂).symm
 #align dfinsupp.single_add DFinsupp.single_add
 
 @[simp]

Mathlib/Data/Finsupp/Defs.lean

@@ -955,6 +955,15 @@ theorem support_zipWith [D : DecidableEq α] {f : M → N → P} {hf : f 0 0 = 0
   rw [Subsingleton.elim D] <;> exact support_onFinset_subset
 #align finsupp.support_zip_with Finsupp.support_zipWith
 
+@[simp]
+theorem zipWith_single_single (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) :
+    zipWith f hf (single a m) (single a n) = single a (f m n) := by
+  ext a'
+  rw [zipWith_apply]
+  obtain rfl | ha' := eq_or_ne a a'
+  · rw [single_eq_same, single_eq_same, single_eq_same]
+  · rw [single_eq_of_ne ha', single_eq_of_ne ha', single_eq_of_ne ha', hf]
+
 end ZipWith
 
 /-! ### Additive monoid structure on `α →₀ M` -/
@@ -996,10 +1005,7 @@ theorem support_add_eq [DecidableEq α] {g₁ g₂ : α →₀ M} (h : Disjoint
 
 @[simp]
 theorem single_add (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
-  ext fun a' => by
-    by_cases h : a = a'
-    · rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same]
-    · rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add]
+  (zipWith_single_single _ _ _ _ _).symm
 #align finsupp.single_add Finsupp.single_add
 
 instance addZeroClass : AddZeroClass (α →₀ M) :=

Mathlib/Data/Finsupp/Pointwise.lean

@@ -49,6 +49,10 @@ theorem mul_apply {g₁ g₂ : α →₀ β} {a : α} : (g₁ * g₂) a = g₁ a
   rfl
 #align finsupp.mul_apply Finsupp.mul_apply
 
+@[simp]
+theorem single_mul (a : α) (b₁ b₂ : β) : single a (b₁ * b₂) = single a b₁ * single a b₂ :=
+  (zipWith_single_single _ _ _ _ _).symm
+
 theorem support_mul [DecidableEq α] {g₁ g₂ : α →₀ β} :
     (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support := by
   intro a h