generalize truncation lemmas

Author: justus-springer

Mathlib/RingTheory/MvPowerSeries/Trunc.lean

@@ -125,16 +125,24 @@ theorem truncFinset_map [CommSemiring S] (f : R →+* S) (p : MvPowerSeries σ R
   ext x
   by_cases x ∈ s <;> grind [coeff_map, MvPolynomial.coeff_map]
 
-theorem coeff_truncFinset_mul_truncFinset_eq_coeff_mul (hs : IsLowerSet (s : Set (σ →₀ ℕ)))
-    {x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hx : x ∈ s) :
-      (truncFinset R s f * truncFinset R s g).coeff x = coeff x (f * g) := by
+/-- A coefficient of a product of finset-truncated power series equals the coefficient of the
+untruncated product, with the two truncation finsets `s` and `t` allowed to differ. -/
+theorem coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ {t : Finset (σ →₀ ℕ)}
+    (hs : IsLowerSet (s : Set (σ →₀ ℕ))) (ht : IsLowerSet (t : Set (σ →₀ ℕ)))
+    {x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hxs : x ∈ s) (hxt : x ∈ t) :
+      (truncFinset R s f * truncFinset R t g).coeff x = coeff x (f * g) := by
   classical
   simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
   apply sum_congr rfl
   rintro ⟨i, j⟩ hij
   simp only [mem_antidiagonal] at hij
-  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
-    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
+  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hxs),
+    coeff_truncFinset_of_mem _ (ht (show j ≤ x by simp [← hij]) hxt)]
+
+theorem coeff_truncFinset_mul_truncFinset_eq_coeff_mul (hs : IsLowerSet (s : Set (σ →₀ ℕ)))
+    {x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hx : x ∈ s) :
+      (truncFinset R s f * truncFinset R s g).coeff x = coeff x (f * g) :=
+  coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ hs hs f g hx hx
 
 theorem truncFinset_truncFinset_pow (hs : IsLowerSet (s : Set (σ →₀ ℕ))) {k : ℕ} (hk : 1 ≤ k)
     (p : MvPowerSeries σ R) : truncFinset R s ((truncFinset R s p) ^ k) =
@@ -190,6 +198,21 @@ theorem trunc_one (n : σ →₀ ℕ) (hnn : n ≠ 0) : trunc R n 1 = 1 :=
 theorem trunc_C (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : trunc R n (C a) = MvPolynomial.C a :=
   truncFinset_C (by simpa using pos_of_ne_zero hnn) a
 
+/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
+product, with the two truncation levels `n₁` and `n₂` allowed to differ. -/
+theorem coeff_trunc_mul_trunc_eq_coeff_mul₂ (n₁ n₂ : σ →₀ ℕ)
+    (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h₁ : m < n₁) (h₂ : m < n₂) :
+    (trunc R n₁ f * trunc R n₂ g).coeff m = coeff m (f * g) :=
+  coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ (by intro; grind) (by intro; grind) f g
+    (by simpa) (by simpa)
+
+/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
+product. Both factors are truncated at the same level `n`. -/
+theorem coeff_trunc_mul_trunc_eq_coeff_mul (n : σ →₀ ℕ)
+    (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m < n) :
+    (trunc R n f * trunc R n g).coeff m = coeff m (f * g) :=
+  coeff_trunc_mul_trunc_eq_coeff_mul₂ n n f g h h
+
 @[simp]
 theorem trunc_C_mul (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) :
     trunc R n (C a * p) = MvPolynomial.C a * trunc R n p := by
@@ -231,11 +254,20 @@ theorem trunc'_one (n : σ →₀ ℕ) : trunc' R n 1 = 1 := truncFinset_one (by
 theorem trunc'_C (n : σ →₀ ℕ) (a : R) : trunc' R n (C a) = MvPolynomial.C a :=
   truncFinset_C (by simp) a
 
-/-- Coefficients of the truncation of a product of two multivariate power series -/
+/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
+product, with the two truncation levels `n₁` and `n₂` allowed to differ. -/
+theorem coeff_trunc'_mul_trunc'_eq_coeff_mul₂ (n₁ n₂ : σ →₀ ℕ)
+    (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h₁ : m ≤ n₁) (h₂ : m ≤ n₂) :
+    (trunc' R n₁ f * trunc' R n₂ g).coeff m = coeff m (f * g) :=
+  coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ (by intro; grind) (by intro; grind) f g
+    (by simpa) (by simpa)
+
+/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
+product. Both factors are truncated at the same level `n`. -/
 theorem coeff_trunc'_mul_trunc'_eq_coeff_mul (n : σ →₀ ℕ)
     (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m ≤ n) :
     (trunc' R n f * trunc' R n g).coeff m = coeff m (f * g) :=
-  coeff_truncFinset_mul_truncFinset_eq_coeff_mul (by intro; grind) f g (by simpa)
+  coeff_trunc'_mul_trunc'_eq_coeff_mul₂ n n f g h h
 
 @[deprecated coeff_trunc'_mul_trunc'_eq_coeff_mul (since := "2026-02-20")]
 theorem coeff_mul_eq_coeff_trunc'_mul_trunc' (n : σ →₀ ℕ) (f g : MvPowerSeries σ R) {m : σ →₀ ℕ}