enat_to_nat

This file implements the enat_to_nat tactic that shifts ENats in the context to Nat.

Implementation details

The implementation follows these steps:

1. Apply the cases tactic to each ENat variable, producing two goals: one where the variable is ⊤, and one where it is a finite natural number.
2. Simplify arithmetic expressions involving infinities, making (in)equalities either trivial or free of infinities. This step uses the enat_to_nat_top simp set.
3. Translate the remaining goals from ENat to Nat using the enat_to_nat_coe simp set.

theorem Mathlib.Tactic.ENatToNat.not_lt_top (x : ℕ∞) : ¬⊤ < x

theorem Mathlib.Tactic.ENatToNat.coe_add (m n : ℕ) : ↑m + ↑n = ↑(m + n)

theorem Mathlib.Tactic.ENatToNat.coe_sub (m n : ℕ) : ↑m - ↑n = ↑(m - n)

theorem Mathlib.Tactic.ENatToNat.coe_mul (m n : ℕ) : ↑m * ↑n = ↑(m * n)

theorem Mathlib.Tactic.ENatToNat.coe_ofNat (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = ↑(OfNat.ofNat n)

theorem Mathlib.Tactic.ENatToNat.coe_zero : 0 = ↑0

theorem Mathlib.Tactic.ENatToNat.coe_one : 1 = ↑1

def Mathlib.Tactic.ENatToNat.tacticCases_first_enat : Lean.ParserDescr

Finds the first ENat in the context and applies the cases tactic to it. Then simplifies expressions involving ⊤ using the enat_to_nat_top simp set.

def Mathlib.Tactic.ENatToNat.tacticEnat_to_nat : Lean.ParserDescr

enat_to_nat shifts all ENats in the context to Nat, rewriting propositions about them. A typical use case is enat_to_nat; omega.