From 5f1189ac2d09d61824930c187e5f904692abab38 Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Wed, 6 May 2026 19:08:27 +0200 Subject: [PATCH] chore(Algebra/Polynomial/Module): workaround for backward.inferInstanceAs This PR, like #38990, works around a `backward.inferInstanceAs` compatibility flag introduced by identifying `PolynomialModule` with `Finsupp` in our definitions. We introduce a new dsimp lemma `funLike_eq` that transfers the `FunLike` instances, and now we can use `PolynomialModule`'s `FunLike` instance, instead of the custom `CoeFun` instance. This is not a great approach, but it seems the least painful for the short term. The alternative would be to strictly enforce the defeq barrier between `PolynomialModule` and `Finsupp`, which would mean a substantial rewrite of this corner of Mathlib. We can't make `PolynomialModule` an `@[implicit_reducible]`, because we need different multiplication on it than `Finsupp` has. --- Mathlib/Algebra/Polynomial/Module/Basic.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Module/Basic.lean b/Mathlib/Algebra/Polynomial/Module/Basic.lean index b2961d0fc98a3b..db3de74f1a1582 100644 --- a/Mathlib/Algebra/Polynomial/Module/Basic.lean +++ b/Mathlib/Algebra/Polynomial/Module/Basic.lean @@ -42,14 +42,17 @@ for the full discussion. def PolynomialModule (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] := ℕ →₀ M deriving Inhabited, FunLike, AddCommGroup -set_option backward.inferInstanceAs.wrap.data false in -deriving instance CoeFun for PolynomialModule - variable (R : Type*) {M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) variable {S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] namespace PolynomialModule +/-- Workaround to defeq problems: if we interpret a `PolynomialModule` as a `Finsupp`, also transfer +the `DFunLike` instance. -/ +@[simp] +theorem funLike_eq (x : PolynomialModule R M) : + DFunLike.coe (self := Finsupp.instFunLike) x = x := rfl + /-- This is required to have the `IsScalarTower S R M` instance to avoid diamonds. -/ instance : Module S (PolynomialModule R M) := inferInstanceAs <| Module S (ℕ →₀ M) @@ -174,8 +177,8 @@ def equivPolynomialSelf : PolynomialModule R R ≃ₗ[R[X]] R[X] := | add _ _ hp hq => rw [smul_add, map_add, map_add, mul_add, hp, hq] | single n a => ext i - simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, smul_single_apply, - smul_eq_mul, coeff_ofFinsupp, single_apply, mul_ite, mul_zero] + simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, funLike_eq, smul_single_apply, + smul_eq_mul, coeff_ofFinsupp, funLike_eq, single_apply, mul_ite, mul_zero] split_ifs with hn · rw [Finset.sum_eq_single (i - n, n)] · simp only [ite_true]