Theorem: ENat.leNat_iff_toNat_le (GMLInit/Data/Nat/Extended/Finite.lean)

State before:
e : ENat
h : e.IsFinite
x : Nat
⊢ e.leNat x = true ↔ e.toNat h ≤ x
Tactic:
constructor
State after:
case mp
e : ENat
h : e.IsFinite
x : Nat
⊢ e.leNat x = true → e.toNat h ≤ x

case mpr
e : ENat
h : e.IsFinite
x : Nat
⊢ e.toNat h ≤ x → e.leNat x = true

State before:
case mp
e : ENat
h : e.IsFinite
x : Nat
⊢ e.leNat x = true → e.toNat h ≤ x
Tactic:
exact toNat_le_of_leNat
State after:
no goals

State before:
case mpr
e : ENat
h : e.IsFinite
x : Nat
⊢ e.toNat h ≤ x → e.leNat x = true
Tactic:
intro h
State after:
case mpr
e : ENat
h✝ : e.IsFinite
x : Nat
h : e.toNat h✝ ≤ x
⊢ e.leNat x = true

State before:
case mpr
e : ENat
h✝ : e.IsFinite
x : Nat
h : e.toNat h✝ ≤ x
⊢ e.leNat x = true
Tactic:
exact mono h (leNat_toNat ..)
State after:
no goals