Commit 2026-07-17 11:15 d4519b39

View on Github →

chore(Data/ENat): replace coe with natCast in lemma names (#41140) ... following the naming convention

Estimated changes

deleted theorem ENat.addLECancellable_coe
deleted theorem ENat.add_one_le_coe_iff
deleted theorem ENat.coe_add
deleted theorem ENat.coe_add_one_le_iff
deleted theorem ENat.coe_inj
deleted theorem ENat.coe_le_coe
deleted theorem ENat.coe_lift
deleted theorem ENat.coe_lt_add_one_iff
deleted theorem ENat.coe_lt_coe
deleted theorem ENat.coe_lt_top
deleted theorem ENat.coe_mul
deleted theorem ENat.coe_ne_top
deleted theorem ENat.coe_one
deleted theorem ENat.coe_sub
deleted theorem ENat.coe_toNat_eq_self
deleted theorem ENat.coe_toNat_le_self
deleted theorem ENat.coe_zero
deleted theorem ENat.le_coe_iff
added theorem ENat.le_natCast_iff
deleted theorem ENat.lift_coe
added theorem ENat.lift_natCast
modified theorem ENat.lift_one
modified theorem ENat.lift_zero
deleted theorem ENat.lt_coe_add_one_iff
deleted theorem ENat.map_coe
added theorem ENat.map_natCast
added theorem ENat.natCast_add
added theorem ENat.natCast_inj
added theorem ENat.natCast_lift
added theorem ENat.natCast_lt_top
added theorem ENat.natCast_mul
added theorem ENat.natCast_ne_top
added theorem ENat.natCast_one
added theorem ENat.natCast_sub
added theorem ENat.natCast_zero
deleted theorem ENat.some_eq_coe
added theorem ENat.some_eq_natCast
deleted theorem ENat.succ_coe
added theorem ENat.succ_natCast
deleted theorem ENat.toNat_coe
deleted theorem ENat.toNat_eq_iff_eq_coe
deleted theorem ENat.toNat_le_of_le_coe
added theorem ENat.toNat_natCast
deleted theorem ENat.top_ne_coe
added theorem ENat.top_ne_natCast
deleted theorem ENat.top_sub_coe
added theorem ENat.top_sub_natCast
deleted theorem ENat.recTopCoe_coe
added theorem ENat.recTopCoe_natCast
deleted theorem ENat.coe_iInf
deleted theorem ENat.coe_iSup
deleted theorem ENat.coe_sInf
deleted theorem ENat.coe_sSup
deleted theorem ENat.iInf_coe_eq_top
deleted theorem ENat.iInf_coe_lt_top
deleted theorem ENat.iInf_coe_ne_top
deleted theorem ENat.iInf_eq_coe_iff
deleted theorem ENat.iSup_coe_eq_top
deleted theorem ENat.iSup_coe_lt_top
deleted theorem ENat.iSup_coe_ne_top
added theorem ENat.natCast_iInf
added theorem ENat.natCast_iSup
added theorem ENat.natCast_sInf
added theorem ENat.natCast_sSup
modified theorem Set.ncard_le_encard