Don't know how to solve issue

Stream: lean4

[Mark Santa Clara Munro]

I get the error message: typeclass instance problem is stuck, it is often due to metavariables

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m] [SMul R α] [Add α] [Zero α] [Mul α]
-- Operation which add x times Row j to Row i
def addMultipleRow (M : Matrix m n α) (i : m) (j : m) (x : R): Matrix m n α :=
  Matrix.updateRow M i (M i + x • M j)

-- If you add a multiple of Row j into Row i, then i will be the original i plus the multiple of Row j
lemma addMultipleRowi (M : Matrix m n α) (i : m) (j : m)
 : addMultipleRow M i j x i = M i + x • M j := by
 rw [addMultipleRow]

[Paul Rowe]

I don't think x is in the scope of your lemma. Notice that it's an argument to your def above. If you add it to your lemma too, I think it gets unstuck.

[Eric Wieser]

With set_option autoImplicit false Lean would tell you exactly what Paul says

[Mark Santa Clara Munro]

Thank you! I don't know how I missed that

[Paul Rowe]

Eric's suggestion of set_option autoImplicit false helps save a lot of these situations. When it's set to true, Lean is much more willing to try to figure out what the type of implicit variables are. While this can make things look more streamlined, it's much harder to track down these issues.

[James Sully]

I'm assuming but not sure, does that turn off this feature? Ah, yes it says so on that page