IdemSemiring + OfNat

Stream: mathlib4

[Julian Berman]

Should either of these exist (and if so should they be simp lemmas?) I managed to confuse myself nicely yesterday by continuing to write (3 : Ideal R) instead of Ideal.span {3}, and not understanding why nothing behaved as I expected. Maybe the simp lemma would have made me realize I was writing nonsense.

import Mathlib.RingTheory.Ideal.Operations

@[simp]
lemma cast_eq_one {R : Type*} [i : IdemSemiring R] {n : ℕ} [hn : n.AtLeastTwo] : (n : R) = 1 := by
  induction n, hn.prop.le using Nat.le_induction with
  | base => rw [Nat.cast_ofNat, ← add_idem (1 : R), one_add_one_eq_two.symm]
  | succ a b c => simp_all only [Nat.cast_add, Nat.cast_one, add_idem (1 : R)]

@[simp]
lemma ofNat_eq_top {R : Type*} [CommSemiring R] {n : ℕ} [hn : n.AtLeastTwo] : (OfNat.ofNat n : Ideal R) = ⊤ := by
  simp [show (OfNat.ofNat n : Ideal R) = 1 from cast_eq_one]

example {R : Type*} [CommSemiring R] : (3 : Ideal R) = ⊤ := by simp

[Ruben Van de Velde]

No opinion on the details, but yes, it seems like a good idea for these to exist, at least

[Eric Wieser]

I think the second one will never fire because of the lack of no_index, but with it fires on every single expression. So it should be no_index but not simp

[Eric Wieser]

I don't think you need AtLeastTwo on the first one

[Julian Berman]

#20244 is my attempt. Eric let me know if for whatever reason you want me to wait for your ofNat() PR.