Centralize two privately duplicated lemmas

RealRooted/Basic/RootLists.lean

@@ -39,6 +39,15 @@ def ListAlternates : List ℝ → List ℝ → Prop
   | s :: ss, r :: rs => s ≤ r ∧ ListInterlaces ss (r :: rs)
   | _, _ => False
 
+/-- Differ-by-one interleaving with the first right root dropped is same-degree interleaving. -/
+lemma listAlternates_of_listInterlaces_cons :
+    ∀ {ss rs : List ℝ} {r : ℝ}, ListInterlaces ss (r :: rs) → ListAlternates ss rs
+  | [], [], _, _ => by simp [ListAlternates]
+  | s :: ss, r₂ :: rs, r, h => by
+      simpa [ListInterlaces, ListAlternates] using h.2
+  | [], _ :: _, _, h => by simp [ListInterlaces] at h
+  | _ :: _, [], _, h => by simp [ListInterlaces] at h
+
 /-- If a list is sorted, then its tail interlaces into it. -/
 lemma listInterlaces_tail_of_pairwise :
     ∀ rs : List ℝ, rs.Pairwise (· ≤ ·) → ListInterlaces rs.tail rs

RealRooted/BorceaBranden/FiniteOrderWeylPreserver.lean

@@ -264,16 +264,6 @@ private theorem pderiv_spectatorProduct_zero {σ : Type*} [Fintype σ]
   intro i hi
   exact (Finset.mem_erase.mp hi).1
 
-private theorem iteratedPDerivAt_mul_of_pderiv_zero {σ : Type*}
-    (q : σ) (j : ℕ) (a b : MvPolynomial σ ℂ)
-    (hb : MvPolynomial.pderiv q b = 0) :
-    iteratedPDerivAt q j (a * b) = iteratedPDerivAt q j a * b := by
-  induction j with
-  | zero => rfl
-  | succ j ih =>
-      rw [iteratedPDerivAt, ih, MvPolynomial.pderiv_mul, hb, mul_zero,
-        add_zero, iteratedPDerivAt]
-
 private theorem algebraicSymbol_iteratedPDerivAtDegreeBox_explicit
     {σ : Type*} [Fintype σ] [DecidableEq σ]
     (q : σ) (j n : ℕ) (κ : σ → ℕ)

RealRooted/FiniteFreeAdditive/Stability.lean

@@ -396,16 +396,6 @@ private theorem pderiv_spectatorProduct_zero_real
         simp
   exact hprod (Finset.univ.erase q) fun i hi => (Finset.mem_erase.mp hi).1
 
-private theorem iteratedPDerivAt_mul_of_pderiv_zero_real {σ : Type*}
-    (q : σ) (j : ℕ) (a b : MvPolynomial σ ℝ)
-    (hb : MvPolynomial.pderiv q b = 0) :
-    iteratedPDerivAt q j (a * b) = iteratedPDerivAt q j a * b := by
-  induction j with
-  | zero => rfl
-  | succ j ih =>
-      rw [iteratedPDerivAt, ih, MvPolynomial.pderiv_mul, hb, mul_zero,
-        add_zero, iteratedPDerivAt]
-
 private theorem algebraicSymbol_iteratedPDerivAtDegreeBoxReal_explicit
     {σ : Type*} [Fintype σ] [DecidableEq σ]
     (q : σ) (j D : ℕ) (κ : σ → ℕ) (hκ : κ q = D) :
@@ -417,7 +407,7 @@ private theorem algebraicSymbol_iteratedPDerivAtDegreeBoxReal_explicit
           (MvPolynomial.X (Sum.inl i) + MvPolynomial.X (Sum.inr i)) ^ κ i := by
   rw [algebraicSymbol_iteratedPDerivAtDegreeBoxReal,
     algebraicSymbol_realDegreeBoxInclusion q D κ hκ,
-    iteratedPDerivAt_mul_of_pderiv_zero_real]
+    iteratedPDerivAt_mul_of_pderiv_zero]
   · rw [iteratedPDerivAt_linearForm_pow_real (Sum.inl q) (Sum.inr q)
       Sum.inl_ne_inr j D]
   · exact pderiv_spectatorProduct_zero_real q κ

RealRooted/Interlacing/QuadraticRemainderCriterion.lean

@@ -819,15 +819,6 @@ theorem normalizedQuadraticFamily_interlaces_mul_X_add_one_of_le
     simp [normalizedQuadraticFamily_natDegree]
   simpa only [map_neg, map_one, neg_neg, sub_neg_eq_add] using hfactor.toInterlaces hdeg
 
-private lemma listAlternates_of_listInterlaces_cons :
-    ∀ {ss rs : List ℝ} {r : ℝ},
-      ListInterlaces ss (r :: rs) → ListAlternates ss rs
-  | [], [], _, _ => by simp [ListAlternates]
-  | s :: ss, r₂ :: rs, r, h => by
-      simpa [ListInterlaces, ListAlternates] using h.2
-  | [], _ :: _, _, h => by simp [ListInterlaces] at h
-  | _ :: _, [], _, h => by simp [ListInterlaces] at h
-
 private lemma strictInterl_of_interlaces_mul_X_add_one
     {f g : ℝ[X]} (h : Interlaces f ((X + C 1) * g))
     (hg₀ : g ≠ 0) (hgs : g.Splits)

RealRooted/LiebSokalOperator.lean

@@ -38,6 +38,16 @@ theorem iteratedPDerivAt_eq_pow
     change MvPolynomial.pderiv i (((MvPolynomial.pderiv i).toLinearMap ^ n) P) = _
     simp only [ih, iteratedPDerivAt]
 
+/-- Iterated partial derivatives in `i` commute with multiplication by a factor that is constant
+in `i`. -/
+theorem iteratedPDerivAt_mul_of_pderiv_zero {R sigma : Type*} [CommSemiring R]
+    (i : sigma) (n : ℕ) (a b : MvPolynomial sigma R) (hb : MvPolynomial.pderiv i b = 0) :
+    iteratedPDerivAt i n (a * b) = iteratedPDerivAt i n a * b := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+      rw [iteratedPDerivAt, ih, MvPolynomial.pderiv_mul, hb, mul_zero, add_zero, iteratedPDerivAt]
+
 /-- A fixed enumeration of a finite variable type, used to define iterated
 partial differentiation without imposing an order on the variable type. -/
 def differentialVariableOrder (sigma : Type*) [Fintype sigma] : List sigma :=

RealRooted/PolynomialValueEulerNumerator/Interlacing.lean

@@ -164,15 +164,6 @@ private lemma listAlternates_map_cayleyRoot :
   | [], _ :: _, h, _, _ => by simp [ListAlternates] at h
   | _ :: _, [], h, _, _ => by simp [ListAlternates] at h
 
-private lemma listAlternates_of_listInterlaces_cons :
-    ∀ {ss rs : List ℝ} {r : ℝ},
-      ListInterlaces ss (r :: rs) → ListAlternates ss rs
-  | [], [], _, _ => by simp [ListAlternates]
-  | s :: ss, r₂ :: rs, r, h => by
-      simpa [ListInterlaces, ListAlternates] using h.2
-  | [], _ :: _, _, h => by simp [ListInterlaces] at h
-  | _ :: _, [], _, h => by simp [ListInterlaces] at h
-
 private lemma all_ge_head_of_pairwise {r : ℝ} {rs : List ℝ}
     (h : (r :: rs).Pairwise (· ≤ ·)) :
     ∀ x ∈ r :: rs, r ≤ x := by