Consider adding the failed example relevant to the bad diamond issue in Chapter7 §1

[onriv]

Hi! At the almost end the first section of Chatper 7, the content about fixing the diamond problem for the two instances:

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
  smul := fun r s ↦ r*s
  zero_smul := zero_mul
  one_smul := one_mul
  mul_smul := mul_assoc₃
  add_smul := Ring₃.right_distrib
  smul_add := Ring₃.left_distrib

instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
  smul := zsmul₁
  zero_smul := sorry
  one_smul := sorry
  mul_smul := sorry
  add_smul := sorry
  smul_add := sorry

is by defining AddMonoid₄ with a default nsmul, and overriding it for the type ℤ.

The current version contains a example to explain how this work:

instance : AddMonoid₄ ℤ where
  add := (· + ·)
  add_assoc₃ := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  nsmul := fun n m ↦ (n : ℤ) * m
  nsmul_zero := Int.zero_mul
  nsmul_succ := fun n m ↦ show (n + 1 : ℤ) * m = m + n * m
    by rw [Int.add_mul, Int.add_comm, Int.one_mul]

example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl

But the "failed version" for AddMonoid₃ seems missed:

instance myBadSMul {M : Type} [AddMonoid₃ M] : SMul ℕ M := ⟨nsmul₁⟩

-- This failed, it cannot be proved via `rfl`
example (n : ℕ) (m : ℤ) : SMul.smul (self := myBadSMul) n m = n * m := rfl

Please consider adding it to Chapter7. Thank you very much. 😊
And there is a discussion about it on zulip too