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

State before:
e : ENat
h : e.IsFinite
⊢ ENat.ofNat (e.toNat h) = e
Tactic:
ext x
State after:
case leNat.h
e : ENat
h : e.IsFinite
x : Nat
⊢ (ENat.ofNat (e.toNat h)).leNat x = e.leNat x

State before:
case leNat.h
e : ENat
h : e.IsFinite
x : Nat
⊢ (ENat.ofNat (e.toNat h)).leNat x = e.leNat x
Tactic:
cases hx : e.leNat x with
| true => rw [leNat_coe_eq_true_iff_le, ←leNat_iff_toNat_le, hx]
| false =>
rw [←Bool.not_eq_true] at hx ⊢
apply mt _ hx
intro hx
rw [leNat_iff_toNat_le _ h]
rwa [leNat_coe_eq_true_iff_le] at hx
State after:
no goals

State before:
case leNat.h.true
e : ENat
h : e.IsFinite
x : Nat
hx : e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true
Tactic:
rw [leNat_coe_eq_true_iff_le, ←leNat_iff_toNat_le, hx]
State after:
no goals

State before:
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : e.leNat x = false
⊢ (ENat.ofNat (e.toNat h)).leNat x = false
Tactic:
rw [←Bool.not_eq_true] at hx ⊢
State after:
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ ¬(ENat.ofNat (e.toNat h)).leNat x = true

State before:
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ ¬(ENat.ofNat (e.toNat h)).leNat x = true
Tactic:
apply mt _ hx
State after:
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true → e.leNat x = true

State before:
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true → e.leNat x = true
Tactic:
intro hx
State after:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.leNat x = true

State before:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.leNat x = true
Tactic:
rw [leNat_iff_toNat_le _ h]
State after:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.toNat h ≤ x

State before:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.toNat h ≤ x
Tactic:
rwa [leNat_coe_eq_true_iff_le] at hx
State after:
no goals