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

State before:
x : Nat
⊢ (ENat.ofNat x).toNat ⋯ = x
Tactic:
apply Nat.le_antisymm
State after:
case h₁
x : Nat
⊢ (ENat.ofNat x).toNat ⋯ ≤ x

case h₂
x : Nat
⊢ x ≤ (ENat.ofNat x).toNat ⋯

State before:
case h₁
x : Nat
⊢ (ENat.ofNat x).toNat ⋯ ≤ x
Tactic:
rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le]
State after:
case h₁
x : Nat
⊢ x ≤ x

State before:
case h₁
x : Nat
⊢ x ≤ x
Tactic:
exact Nat.le_refl ..
State after:
no goals

State before:
case h₂
x : Nat
⊢ x ≤ (ENat.ofNat x).toNat ⋯
Tactic:
cases x with
| zero => exact Nat.zero_le _
| succ x =>
  apply Nat.succ_le_of_lt
  apply Nat.not_le.1
  intro (h : _ ≤ x)
  rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le] at h
  apply Nat.not_lt.2 h
  exact Nat.lt_succ_self _
State after:
no goals

State before:
case h₂.zero

⊢ 0 ≤ (ENat.ofNat 0).toNat ⋯
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case h₂.succ
x : Nat
⊢ x + 1 ≤ (ENat.ofNat (x + 1)).toNat ⋯
Tactic:
apply Nat.succ_le_of_lt
State after:
case h₂.succ.h
x : Nat
⊢ x < (ENat.ofNat (x + 1)).toNat ⋯

State before:
case h₂.succ.h
x : Nat
⊢ x < (ENat.ofNat (x + 1)).toNat ⋯
Tactic:
apply Nat.not_le.1
State after:
case h₂.succ.h
x : Nat
⊢ ¬(ENat.ofNat (x + 1)).toNat ⋯ ≤ x

State before:
case h₂.succ.h
x : Nat
⊢ ¬(ENat.ofNat (x + 1)).toNat ⋯ ≤ x
Tactic:
intro (h : _ ≤ x)
State after:
case h₂.succ.h
x : Nat
h : (ENat.ofNat (x + 1)).toNat ⋯ ≤ x
⊢ False

State before:
case h₂.succ.h
x : Nat
h : (ENat.ofNat (x + 1)).toNat ⋯ ≤ x
⊢ False
Tactic:
rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le] at h
State after:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ False

State before:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ False
Tactic:
apply Nat.not_lt.2 h
State after:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ x < x + 1

State before:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ x < x + 1
Tactic:
exact Nat.lt_succ_self _
State after:
no goals