confusing error

Stream: new members

[Abhijit A J]

Hi! This is my first message on this Zulip group, and I do not know where I should post this. So, here goes nothing:
I was playing around with modules to understand this notion of "bad diamonds" better, but I got an error that I cannot understand properly

variable {R S : Type} [CommRing R] [CommRing S]

instance moduleMorphism (f : R →+* S) : Module R S where
  smul := fun r s => (f r) * s
  one_smul := by
    intro b
    --nth_rw 2 [← one_mul b]
    show (f 1) * b = b
    rw[f.map_one, one_mul]
  mul_smul := by
    intro x y s
    -- have : y • s = (f y) * s :=  sorry
    sorry
  smul_zero := sorry
  smul_add := sorry
  add_smul := sorry
  zero_smul := sorry

the last 'have' which I have commented gives me the error:

failed to synthesize
  HSMul R S ?m.50447

I am confused why Lean has no problem using the '\smul' in its goal, but when I write it, it cannot find an instance. How do I get around such a problem?

[Aaron Liu]

You should define the smul first

[Aaron Liu]

then define the module later

[Aaron Liu]

that way the smul will exist when you use it in the proofs

[Abhijit A J]

Oh, okay. Thanks. I shall do that.

But, I am still still confused as to why I got this error here, but no problem in the one_smul proof. As in, why did Lean not have any problem recognising:

1 • b = (f 1) * b

in that proof.

[Aaron Liu]

because this part was elaborated elsewhere

[Kyle Miller]

It's taking the actual expression for one_smul from the class definition and plugging in the newly defined smul expression.

It's too bad that it doesn't make an smul instance available... We went back and forth on whether when you're defining a structure the instances being defined should be made available as you go. There are some good reasons not to, but for an instance it's clearly painful.

[Weiyi Wang]

Another advantage of defining SMul (or in general, any operator definition before the extra algebra structure) is that you can immediately follow it up with elementary simp lemmas, which in turn can be used in the algebra structure instance

[Abhijit A J]

@Kyle Miller Thanks, that's really helpful. So, if I understand it correctly, Lean understands that

r  • s = (f r) * s

But, if I type that down in my code, Lean goes looking for a SMul/HSMul instance which I have not defined - is that correct?

[Abhijit A J]

@Weiyi Wang Thanks. That makes complete sense

[Kyle Miller]

Yes, that's correct @Abhijit A J.

Here's illustration that adding the instance yourself makes elaboration work:

import Mathlib

variable {R S : Type} [CommRing R] [CommRing S]

instance moduleMorphism (f : R →+* S) : Module R S where
  smul := fun r s => (f r) * s
  one_smul := by
    intro b
    let : SMul R S := { smul := fun r s => (f r) * s }
    -- the `let` lets this `have` elaborate
    have : (1 : R) • b = b := by
      show (f 1) * b = b
      rw[f.map_one, one_mul]
    exact this
  mul_smul := by
    intro x y s
    -- have : y • s = (f y) * s :=  sorry
    sorry
  smul_zero := sorry
  smul_add := sorry
  add_smul := sorry
  zero_smul := sorry

[Abhijit A J]

@Kyle Miller Thanks a lot. This was very helpful! :)