diamond with strange resolution

Stream: mathlib4

[Kevin Buzzard]

import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Ideal.QuotientOperations
import Mathlib.RingTheory.Ideal.Maps
import Mathlib.Algebra.Polynomial.Basic
--import Mathlib -- uncomment to fix proof

open Polynomial

theorem extracted_1 {B : Type} [CommRing B] {G : Type} [Group G] [Finite G]
    [MulSemiringAction G B] (σ : G) (b : B) :
    σ • ∏ᶠ (τ : G), (X - C (τ • b)) = ∏ᶠ (τ : G), σ • (X - C (τ • b)) := smul_finprod _

The import resolves the diamond

SMulZeroClass.toSMul = MulAction.toSMul

so presumably there's a non-defeq diamond in mathlib somewhere around here?

[Kevin Buzzard]

Aah! #min_imports tells me that the problem is in Mathlib.Algebra.Polynomial.GroupRingAction so now it's much easier to debug! Thanks @Damiano Testa !

[Eric Wieser]

theorem extracted_1 {B : Type} [CommRing B] {G : Type} [Group G] [Finite G]
    [MulSemiringAction G B] (σ : G) (b : B) :
    σ • ∏ᶠ (τ : G), (X - C (τ • b)) = ∏ᶠ (τ : G), σ • (X - C (τ • b)) := by
  convert smul_finprod (α := G) _

makes it clear that the problem is that an instance can't be found

[Eric Wieser]

That is, the diamond is between some_instance_that_exists and ?convert_3, which obviously won't be defeq until the instance is found and the ?convert_3 metavar assigned

[Eric Wieser]

theorem extracted_1 {B : Type} [CommRing B] {G : Type} [Group G] [Finite G]
    [MulSemiringAction G B] (σ : G) (b : B) :
    σ • ∏ᶠ (τ : G), (X - C (τ • b)) = ∏ᶠ (τ : G), σ • (X - C (τ • b)) := by
  exact smul_finprod (ι := G) (α := G) (β := B[X]) _

makes it more obvious

[Kevin Buzzard]

I see -- so there's no diamond, and I'm again just a victim of under-importing.

[Damiano Testa]

I'm glad that #min_imports was useful, but I am not to credit for that! I have worked on the linter version of the command that uses tactic and syntax information, but the infrastructure for the Expr side was already there.