Don't understand application mismatch

Stream: lean4

[Mark Santa Clara Munro]

Can someone help me understand why I get "application type mismatch mul_inv_cancel hx argument hx has type x ≠ @OfNat.ofNat R 0 (@Zero.toOfNat0 R inst✝⁵) : Prop but is expected to have type x ≠ @OfNat.ofNat R 0 (@Zero.toOfNat0 R MonoidWithZero.toZero) : Prop"

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m] [SMul R α] [Add α] [Zero α] [Mul α] [Zero R] [DivisionRing R]

-- Operation which multiplies x by Row i
def mulRow (M : Matrix m n α) (i : m) (x : R) : Matrix m n α :=
  Matrix.updateRow M i (x • M i)

--If you multiply Row i by x and then by 1/x you have the original matrix back
theorem mulRow_x_eq_1divx [Fintype m] [Fintype n] [DivisionRing α] [Semiring R] (M : Matrix m n α) (i : m) (x : R) (hx : x ≠ 0)
  : mulRow (mulRow M i x) i (x⁻¹) = M := by
  unfold mulRow
  ext k l
  by_cases h : k = i
  · subst h
    repeat rw [Matrix.updateRow_self]
    simp [smul_smul, mul_inv_cancel hx]
  · done

[Kim Morrison]

When you write [Zero R] [DivisionRing R], you are saying: "let R be a division ring, but also have a element ambiguously named 0, which need not have anything to do with the 0 that a division ring already has"

[Kim Morrison]

And then later in your proof you are getting a mismatch between these two zeros.

[Kim Morrison]

This is the inst✝⁵ vs MonoidWithZero.toZero different in the error message you've quoted.

[Kim Morrison]

Almost surely the correct fix is to delete [Zero R] .

[Mark Santa Clara Munro]

It still has not worked, any idea why?

[Kevin Buzzard]

Can you post a #mwe showing the current state of your question?

[Mark Santa Clara Munro]

That bug has gone away, I am trying to figure out the rest of the proof and will send one if something shows up, thank you!