From 62d40c87b76151deabbc3f56089e590fbb8605cc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Dec 2023 10:29:29 +0000 Subject: [PATCH] fix: do not abuse `Set.Ioo` as a predicate (#9027) --- Mathlib/Data/Polynomial/UnitTrinomial.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Polynomial/UnitTrinomial.lean b/Mathlib/Data/Polynomial/UnitTrinomial.lean index 0fdef6a5d9c70..21734b51042c9 100644 --- a/Mathlib/Data/Polynomial/UnitTrinomial.lean +++ b/Mathlib/Data/Polynomial/UnitTrinomial.lean @@ -222,7 +222,7 @@ namespace IsUnitTrinomial theorem irreducible_aux1 {k m n : ℕ} (hkm : k < m) (hmn : m < n) (u v w : Units ℤ) (hp : p = trinomial k m n (u : ℤ) v w) : C (v : ℤ) * (C (u : ℤ) * X ^ (m + n) + C (w : ℤ) * X ^ (n - m + k + n)) = - ⟨Finsupp.filter (Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp⟩ := by + ⟨Finsupp.filter (· ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp⟩ := by have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le] rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero] simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial, @@ -257,7 +257,7 @@ theorem irreducible_aux1 {k m n : ℕ} (hkm : k < m) (hmn : m < n) (u v w : Unit theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n) (u v w : Units ℤ) (hp : p = trinomial k m n (u : ℤ) v w) (hq : q = trinomial k m' n (u : ℤ) v w) (h : p * p.mirror = q * q.mirror) : q = p ∨ q = p.mirror := by - let f : ℤ[X] → ℤ[X] := fun p => ⟨Finsupp.filter (Set.Ioo (k + n) (n + n)) p.toFinsupp⟩ + let f : ℤ[X] → ℤ[X] := fun p => ⟨Finsupp.filter (· ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp⟩ replace h := congr_arg f h replace h := (irreducible_aux1 hkm hmn u v w hp).trans h replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm