Commit 2023-11-08 15:51 8e84de5e

View on Github →

chore(PartENat): golf and improve ofNat support (#8002) This PR adds simp lemmas for OfNat.ofNat n : PartENat, 0 : PartENat, and 1 : PartENat in every place where there was a simp lemma for ((n : ℕ) : PartENat). This is necessary for simp confluence in the presence of lemmas such as Nat.cast_ofNat. In addition, instances for CharZero and ZeroLEOneClass are provided so that the lemmas from Data/Nat/Cast/Order.lean will apply, golfing some proofs.

Estimated changes

deleted theorem PartENat.coe_coeHom
modified theorem PartENat.coe_le_coe
modified theorem PartENat.coe_lt_coe
added theorem PartENat.dom_ofNat
added theorem PartENat.dom_one
added theorem PartENat.dom_zero
added theorem PartENat.get_ofNat'
added theorem PartENat.ofNat_lt_top
added theorem PartENat.ofNat_ne_top
added theorem PartENat.one_lt_top
added theorem PartENat.one_ne_top
modified theorem PartENat.toWithTop_natCast'
added theorem PartENat.toWithTop_one
added theorem PartENat.zero_lt_top
added theorem PartENat.zero_ne_top