trying out a `simp` lemma

Stream: new members

[Damiano Testa]

Dear All,

what constitutes a good test for trying out a simp lemma? I list below what comes to mind: is there any other "standard" test that you would do?

• Check that #lint is happy.
• Make sure that CI is successful with the simp tag.
• Check that the statement of the new simp lemma can be proven by simp only after you tag the lemma with simp.
• Modify the statement a bit, in such a way that simp "should prove it" and check that it does.
• Ask on Zulip?

I have ticked all of the above, except that I am still waiting on CI to finish.

Anything else?

Thanks!

[Damiano Testa]

The reason for asking is I would like to tag the lemmas below with simp and Scott suggested to "try it out"!

import algebra.module.basic
import algebra.algebra.basic

@[simp] lemma nat.smul_one_eq_coe {R : Type*} [semiring R] [semimodule ℕ R] (m : ℕ) :
  m • (1 : R) = ↑m :=
by rw [←nsmul_eq_smul, nsmul_eq_mul, mul_one]

@[simp] lemma int.smul_one_eq_coe {R : Type*} [ring R] [semimodule ℤ R] (m : ℤ) :
  m • (1 : R) = ↑m :=
by rw [← gsmul_eq_smul, gsmul_eq_mul, mul_one]

@[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra ℚ A] (m : ℚ) :
  m • (1 : A) = ↑m :=
by rw [algebra.smul_def, mul_one, ring_hom.eq_rat_cast]

[Damiano Testa]

PR #7166

CI was successful with the simp tag for the three lemmas!

[Scott Morrison]

[Scott Morrison]

(Also, this would be better in general than in new members)