Documentation

Mathlib.Tactic.ENatToNat

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.
source
theorem Mathlib.Tactic.ENatToNat.not_lt_top (x : ℕ∞) :
¬⊤ < x
source
theorem Mathlib.Tactic.ENatToNat.coe_add (m n : ℕ) :
↑m + ↑n = ↑(m + n)
source
theorem Mathlib.Tactic.ENatToNat.coe_sub (m n : ℕ) :
↑m - ↑n = ↑(m - n)
source
theorem Mathlib.Tactic.ENatToNat.coe_mul (m n : ℕ) :
↑m * ↑n = ↑(m * n)
source
theorem Mathlib.Tactic.ENatToNat.coe_ofNat (n : ℕ) [n.AtLeastTwo] :
OfNat.ofNat n = ↑(OfNat.ofNat n)
source
theorem Mathlib.Tactic.ENatToNat.coe_zero :
0 = ↑0
source
theorem Mathlib.Tactic.ENatToNat.coe_one :
1 = ↑1
source
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.

Equations
Instances For
    source
    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.

    Equations
    Instances For