diff --git a/RealRooted/BorceaBranden/FiniteSymbolReciprocal.lean b/RealRooted/BorceaBranden/FiniteSymbolReciprocal.lean
index e8d97db8..6c6d9caf 100644
--- a/RealRooted/BorceaBranden/FiniteSymbolReciprocal.lean
+++ b/RealRooted/BorceaBranden/FiniteSymbolReciprocal.lean
@@ -96,7 +96,7 @@ private theorem rightComplementMonomial_one
         (sumInrEmbedding tau sigma) (Finset.univ \ m.1.support)
 
 private theorem degreeOf_rightComplementMonomial_one_le
-    {sigma tau : Type*} [Fintype sigma] [DecidableEq sigma]
+    {sigma tau : Type*} [Fintype sigma]
     (m : {m : sigma →₀ ℕ // ∀ i, m i ≤ 1}) :
     ∀ i : sigma,
       (rightComplementMonomial (R := ℂ) (τ := tau)
@@ -123,7 +123,7 @@ private theorem degreeOf_rename_inl_le_zero
   by_contra hdi
   have hmem : Sum.inr i ∈
       (rename (Sum.inl : tau → Sum tau sigma) A).vars := by
-    rw [mem_vars]
+    rw [mem_vars_iff_mem_support]
     exact ⟨d, hd, Finsupp.mem_support_iff.mpr hdi⟩
   obtain ⟨j, hj, hji⟩ := mem_vars_rename Sum.inl A hmem
   exact Sum.inl_ne_inr hji
@@ -174,7 +174,7 @@ private theorem signedMultiaffineReciprocalRight_target_mul
     ring
 
 private theorem normalized_reciprocal_rightComplementMonomial_one
-    {sigma tau : Type*} [Fintype sigma] [DecidableEq sigma]
+    {sigma tau : Type*} [Fintype sigma]
     (m : {m : sigma →₀ ℕ // ∀ i, m i ≤ 1}) :
     C ((-1 : ℂ) ^ Fintype.card sigma) *
         signedMultiaffineReciprocalRight
diff --git a/RealRooted/PosCombo.lean b/RealRooted/PosCombo.lean
index 679d6cac..73d4e537 100644
--- a/RealRooted/PosCombo.lean
+++ b/RealRooted/PosCombo.lean
@@ -739,7 +739,8 @@ theorem of_aissenSchoenbergWhitney_right_pencil
       C a * (f + C z * g) = C a * f + C b * g := by
     grind
   rw [← hscale]
-  exact ⟨mul_ne_zero (by grind) (hne hz), .mul (.C _) <| (aissenSchoenbergWhitneyForward (hpf hz)).1⟩
+  exact ⟨mul_ne_zero (by grind) (hne hz),
+    .mul (.C _) <| (aissenSchoenbergWhitneyForward (hpf hz)).1⟩
 
 /--
 TNN-named version of `of_aissenSchoenbergWhitney_right_pencil`.
diff --git a/RealRooted/SameDegreeCubicSecondRootFromAnalytic.lean b/RealRooted/SameDegreeCubicSecondRootFromAnalytic.lean
index df05ee04..ee358b65 100644
--- a/RealRooted/SameDegreeCubicSecondRootFromAnalytic.lean
+++ b/RealRooted/SameDegreeCubicSecondRootFromAnalytic.lean
@@ -67,8 +67,7 @@ private theorem card_filter_lt_triple (a b c x : ℝ) :
 Chudnovsky--Seymour root-count theorem. -/
 theorem cubicSecondRootBound_from_analytic : CubicSecondRootBoundStatement := by
   classical
-  intro f g hf_pos hg_pos hf hg hfdeg hgdeg hpc
-  intro a b c p q r hab hbc hpq hqr hfroots hgroots
+  intro f g hf_pos hg_pos hf hg hfdeg hgdeg hpc a b c p q r hab hbc hpq hqr hfroots hgroots
   have hdeg : g.natDegree = f.natDegree := by
     simp [hfdeg, hgdeg]
   by_cases hno : ∀ z, f.IsRoot z → ¬ g.IsRoot z
diff --git a/RealRooted/Tactic/VeroneseSection.lean b/RealRooted/Tactic/VeroneseSection.lean
index edaf7057..8ce8292c 100644
--- a/RealRooted/Tactic/VeroneseSection.lean
+++ b/RealRooted/Tactic/VeroneseSection.lean
@@ -46,7 +46,8 @@ theorem veroneseSectionPolynomial_sequence_zero_or_splits_of_nonneg
     ∀ n : Nat,
       veroneseSectionPolynomial (r n) (k n) (P n) = 0 ∨
         (veroneseSectionPolynomial (r n) (k n) (P n)).Splits := fun n =>
-  veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg (hnn n) (hsplits n) (hr n) (hk n)
+  veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg
+    (hnn n) (hsplits n) (hr n) (hk n)
 
 theorem prec0_veroneseSectionPolynomial_sequence_of_prec
     {r k : Nat → Nat} {P Q : Nat → ℝ[X]}
@@ -337,7 +338,8 @@ macro_rules
         k_lt_r := $hk:term) =>
       `(tactic|
         exact
-          RealRooted.veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg $hpnn $hsplits $hr $hk)
+          RealRooted.veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg
+            $hpnn $hsplits $hr $hk)
   | `(tactic|
       rr_veronese_section_prec0 using
         prec_to_full := $hPrecToFull:term,
@@ -434,7 +436,8 @@ macro_rules
         k_lt_r := $hk:term) =>
       `(tactic|
         exact
-          RealRooted.veroneseSectionPolynomial_sequence_zero_or_splits_of_nonneg $hpnn $hsplits $hr $hk)
+          RealRooted.veroneseSectionPolynomial_sequence_zero_or_splits_of_nonneg
+            $hpnn $hsplits $hr $hk)
   | `(tactic|
       rr_veronese_section_sequence_prec0 using
         prec_to_full := $hPrecToFull:term,
diff --git a/RealRooted/VeroneseSection.lean b/RealRooted/VeroneseSection.lean
index d352eac7..f021df8e 100644
--- a/RealRooted/VeroneseSection.lean
+++ b/RealRooted/VeroneseSection.lean
@@ -1659,7 +1659,8 @@ theorem splits_veroneseSectionPolynomial_of_pf {p : ℝ[X]}
     veroneseSectionPolynomial r k p = 0 ∨
       (veroneseSectionPolynomial r k p).Splits :=
   Or.inr
-    (aissenSchoenbergWhitneyForward (IsPolyaFreqSeq_veroneseSectionPolynomial_coeff (p := p) hp hr hk)).1
+    (aissenSchoenbergWhitneyForward
+      (IsPolyaFreqSeq_veroneseSectionPolynomial_coeff (p := p) hp hr hk)).1
 
 /-- Zero-aware real-rootedness of Veronese sections from the forward ASW
 theorem and a PF certificate for the original polynomial. -/
@@ -1689,7 +1690,8 @@ theorem splits_veroneseSectionPolynomial_of_splits_nonneg {p : ℝ[X]}
     veroneseSectionPolynomial r k p = 0 ∨
       (veroneseSectionPolynomial r k p).Splits :=
   Or.inr
-    (aissenSchoenbergWhitneyForward (IsPolyaFreqSeq_veroneseSectionPolynomial_of_realRooted_nonneg hpnn hprr hr hk)).1
+    (aissenSchoenbergWhitneyForward
+      (IsPolyaFreqSeq_veroneseSectionPolynomial_of_realRooted_nonneg hpnn hprr hr hk)).1
 
 /-- Zero-aware real-rootedness of Veronese sections of real-rooted
 nonnegative-coefficient polynomials, assuming both directions of ASW. -/