instances not found

Stream: mathlib4

[Antoine Chambert-Loir]

In #14571, I add the instance that MvPowerSeries X R has docs#NoZeroDivisors when R has, and transfer it to some cases of HahnSeries, via docs#HahnSeries.toMvPowerSeries.
However, the application of docs#MulEquiv.noZeroDivisors cannot find.

I have copied various attempts at https://github.com/leanprover-community/mathlib4/blob/20ebe700ed92951ec7b3d0e803f9531df2d8a3d5/Mathlib/RingTheory/HahnSeries/PowerSeries.lean#L192

[Antoine Chambert-Loir]

To spare you going there, I am forced to enter

/-- If R has no zero divisors, then `HahnSeries (σ →₀ ℕ) R` has no zero divisors, for finite `σ` -/
instance [NoZeroDivisors R] :
    NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) :=
  @MulEquiv.noZeroDivisors (HahnSeries (σ →₀ ℕ) R) (MvPowerSeries σ R) _ _ _
    (toMvPowerSeries : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R )

[Antoine Chambert-Loir]

because the following do not work:

* MulEquiv.noZeroDivisors (MvPowerSeries σ R) toMvPowerSeries

type mismatch
  MulEquiv.noZeroDivisors (MvPowerSeries σ R) ?m.77016
has type
  @NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) MulZeroClass.toMul MulZeroClass.toZero : Prop
but is expected to have type
  @NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) instMul instZero : Prop

* MulEquiv.noZeroDivisors (MvPowerSeries σ R) (toMvPowerSeries : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R)

type mismatch
  MulEquiv.noZeroDivisors (MvPowerSeries σ R) ?m.77396
has type
  @NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) MulZeroClass.toMul MulZeroClass.toZero : Prop
but is expected to have type
  @NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) instMul instZero : Prop

* @MulEquiv.noZeroDivisors (HahnSeries (σ →₀ ℕ) R) (MvPowerSeries σ R) _ _ _ (toMvPowerSeries)

application type mismatch
  MulEquiv.noZeroDivisors (MvPowerSeries σ R) toMvPowerSeries
argument
  toMvPowerSeries
has type
  HahnSeries (?m.76203 →₀ ℕ) ?m.76201 ≃+* MvPowerSeries ?m.76203 ?m.76201 : Type (max ?u.76200 ?u.76199)
but is expected to have type
  HahnSeries (σ →₀ ℕ) R ≃* MvPowerSeries σ R : Type (max u_2 u_3)

On the other hand, the following example works perfectly:

example (A B : Type*) [Ring A] [Ring B] [NoZeroDivisors A]  (e : B ≃+* A) :
NoZeroDivisors B := MulEquiv.noZeroDivisors A e

[Matthew Ballard]

instance [NoZeroDivisors R] : NoZeroDivisors (HahnSeries (σ →₀ ℕ) R) :=
  MulEquiv.noZeroDivisors (A := HahnSeries (σ →₀ ℕ) R) (MvPowerSeries σ R) toMvPowerSeries.toMulEquiv

It tries hard to coerce a RingEquiv into a MulEquiv but can't quite do it with the metavariables from the implicit arguments.