Not sure what is wrong, can't find expression that is there

Stream: lean4

[Mark Santa Clara Munro]

This might be a type error I'm not sure. I tried to include as little of the [Monoid R] and such things as possible to make it work, which tends to be a source of my problems. I was using Type* for everything, but saw that that might not always be the best and tried some other things, does this have to do with universes at all? The issue is on the last line of the code, everything else seems to be working.

import Mathlib
variable {m n : Type} {α R : Type} {β : Type}
variable [DecidableEq m]

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

lemma mul_left_inv_noncomm [GroupWithZero β] (a : β) (h : a ≠ 0) : a⁻¹ * a = 1 := by
  nth_rewrite 2 [← inv_inv a]
  rw [mul_inv_cancel]
  simp
  exact h

--If you multiply Row i by x and then by 1/x you have the original matrix back
theorem mulRow_x_eq_1divx [Monoid R] [MulAction R α] [GroupWithZero R] [Fintype m] (M : Matrix m n α) (i : m) (x : R)
  : mulRow (mulRow M i x) i (x⁻¹) = M := by
  unfold mulRow
  ext k l
  by_cases h : k = i
  · rw [h]
    repeat rw [Matrix.updateRow_self]
    simp
    rw [smul_smul (x⁻¹) x (M i l)]
    rw [mul_left_inv_noncomm x]

[Yury G. Kudryashov]

mul_left_inv_noncomm is exactly inv_mul_cancel. In the last theorem you have 2 structures on R: Monoid and GroupWithZero. There is nothing forcing * induced by these structures to be the same.

[Yury G. Kudryashov]

You should just assume [GroupWithZero R] instead of Monoid R.

[Mark Santa Clara Munro]

thank you so much, it worked