RCLike.ofReal and smul

Stream: new members

[Yuyuan (Lance) Ouyang]

I need help understanding why the last lines of the code below leads to error

typeclass instance problem is stuck, it is often due to metavariables
  HSMul ?m.5471 (K × K) (K × K)

Thanks!

import Mathlib

variable {K: Type*} [RCLike K]
example (a b : K) (ha : a = 0) : a • (b, (1 : K)) = (0 : K × K) := by
  rw [ha, zero_smul]
example (a : ℝ) (b : K) (ha : a = 0) : (RCLike.ofReal a) * b = 0 := by
  rw [ha]; simp only [map_zero, zero_mul]
example (a b : ℝ) (ha : a = 0) : a • (RCLike.ofReal b, 1) = (0 : K × K) := by
  rw [ha, zero_smul]
example (a : ℝ) (b : K) (ha : a = 0) : (RCLike.ofReal a) • (b, (1 : K)) = (0 : K × K) := by
  sorry

[Riccardo Brasca]

Lean doesn't understand that RCLike.ofReal a is in K. Writing (RCLike.ofReal a : K) fixes it.

[Riccardo Brasca]

Essentially it has no way of understanding which external multiplication are you referring to.

[Yuyuan (Lance) Ouyang]

Riccardo Brasca said:

Lean doesn't understand that RCLike.ofReal a is in K. Writing (RCLike.ofReal a : K) fixes it.

That was really quick. Thanks!

[Riccardo Brasca]

Errors in Lean are usually hard to read, but this one was OK.

typeclass instance problem is stuck, it is often due to metavariables
  HSMul ?m.5574 (K × K) (K × K)

[Riccardo Brasca]

typeclass instance problem is stuck means "there is a variable I am not able to guess"

[Riccardo Brasca]

and in the next line you see it is the first variable of HSMul (because it is called ?m.5574), so it is the first variable of dodcs#HSmul, that is the first type in an external multiplication.

[Riccardo Brasca]

Now, usually, Lean guess it because you give it a term to be used in the multiplication, and in your example the term is RCLike.ofReal a. If you look at docs#RCLike.ofReal you see that K is implicit, meaning that we don't specify it and we let Lean guess it (we decided to do so because it usually works). In this specific case it's impossible, hence the error.

[Yuyuan (Lance) Ouyang]

Riccardo Brasca said:

Now, usually, Lean guess it because you give it a term to be used in the multiplication, and in your example the term is RCLike.ofReal a. If you look at docs#RCLike.ofReal you see that K is implicit, meaning that we don't specify it and we let Lean guess it (we decided to do so because it usually works). In this specific case it's impossible, hence the error.

I see. Thanks for the detailed explanation!