Commit 2026-09-17 17:14 2acaf8b6

View on Github →

feat(Tactic): general tactic to translate (E)NNReal, ENat, PNat goals to Real and Nat (#43254) Introduce the basify tactic, which translates goals about types with extended or truncated arithmetic (PNat, ENat, NNReal, ENNReal) into equivalent goals about the underlying type (Nat, Real), where automation works better. The tactic is extensible:

  • @[basify_elim] adds support for a new type;
  • @[basify_op] adds support for a new operation;
  • @[basify_simp] adds rewrite lemmas for clearing the degenerate branches It subsumes pnat_to_nat and enat_to_nat (#43422).

Estimated changes

modified theorem OfNat.ofNat_ne_zero
modified theorem one_ne_zero
modified theorem ENNReal.coe_add
modified theorem ENNReal.coe_eq_zero
modified theorem ENNReal.coe_inj
modified theorem ENNReal.coe_le_coe
modified theorem ENNReal.coe_lt_coe
modified theorem ENNReal.coe_lt_top
modified theorem ENNReal.coe_mul
modified theorem ENNReal.coe_one
modified theorem ENNReal.coe_pow
modified theorem ENNReal.coe_toReal
modified theorem ENNReal.coe_zero
modified theorem ENNReal.toReal_top
modified theorem ENNReal.top_ne_coe
modified theorem ENNReal.div_top
modified theorem ENNReal.inv_top
modified theorem ENNReal.coe_sub
modified theorem ENNReal.mul_top
modified theorem ENNReal.sub_top
modified theorem ENNReal.top_mul
modified theorem ENNReal.top_pow
modified theorem ENNReal.top_sub_coe
modified theorem NNReal.coe_inj
modified theorem NNReal.coe_le_coe
modified theorem NNReal.coe_lt_coe
modified theorem NNReal.coe_one
modified theorem NNReal.coe_zero
modified theorem ENat.sub_top
modified theorem ENat.mul_top
modified theorem ENat.natCast_mul
modified theorem ENat.top_mul
added def PNat.recToPNat
added def bar
added def foo