Theorem: ENat.eq_ofNat_of_le_ofNat (GMLInit/Data/Nat/Extended/Order.lean)

State before:
case zero
x : ENat
⊢ x ≤ ENat.ofNat 0 → ∃ m, m ≤ 0 ∧ x = ENat.ofNat m
Tactic:
intro h
State after:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ ∃ m, m ≤ 0 ∧ x = ENat.ofNat m

State before:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ ∃ m, m ≤ 0 ∧ x = ENat.ofNat m
Tactic:
exists 0
State after:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0 ∧ x = ENat.ofNat 0

State before:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0 ∧ x = ENat.ofNat 0
Tactic:
constructor
State after:
case zero.left
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0

case zero.right
x : ENat
h : x ≤ ENat.ofNat 0
⊢ x = ENat.ofNat 0

State before:
case zero.left
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0
Tactic:
exact Nat.le_refl ..
State after:
no goals

State before:
case zero.right
x : ENat
h : x ≤ ENat.ofNat 0
⊢ x = ENat.ofNat 0
Tactic:
exact eq_zero_of_le_zero h
State after:
no goals

State before:
case succ
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
⊢ x ≤ ENat.ofNat (n + 1) → ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
intro h
State after:
case succ
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m

State before:
case succ.true
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x.leNat n = true
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
rw [leNat_eq_true_iff_le_coe] at hn
State after:
case succ.true
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m

State before:
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
exists m
State after:
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1 ∧ x = ENat.ofNat m

State before:
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
constructor
State after:
case left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1

case right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ x = ENat.ofNat m

State before:
case left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1
Tactic:
exact Nat.le_succ_of_le h
State after:
no goals

State before:
case right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ x = ENat.ofNat m
Tactic:
exact hm
State after:
no goals

State before:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x.leNat n = false
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
rw [leNat_eq_false_iff_coe_lt] at hn
State after:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m

State before:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
exists n+1
State after:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1 ∧ x = ENat.ofNat (n + 1)

State before:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1 ∧ x = ENat.ofNat (n + 1)
Tactic:
constructor
State after:
case succ.false.left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1

case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ x = ENat.ofNat (n + 1)

State before:
case succ.false.left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1
Tactic:
exact Nat.le_refl ..
State after:
no goals

State before:
case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ x = ENat.ofNat (n + 1)
Tactic:
apply le_antisymm h
State after:
case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ENat.ofNat (n + 1) ≤ x

State before:
case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ENat.ofNat (n + 1) ≤ x
Tactic:
exact coe_lt_iff_coe_succ_le.1 hn
State after:
no goals