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

State before:
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
⊢ x ≤ y
Tactic:
intro n
State after:
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
⊢ x.leNat n = true ∨ y.leNat n = false

State before:
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
⊢ x.leNat n = true ∨ y.leNat n = false
Tactic:
cases Nat.le_total n n₀ with
| inl h => right; exact mono' h hy
| inr h => left; exact mono h hx
State after:
no goals

State before:
case inl
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n ≤ n₀
⊢ x.leNat n = true ∨ y.leNat n = false
Tactic:
right
State after:
case inl.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n ≤ n₀
⊢ y.leNat n = false

State before:
case inl.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n ≤ n₀
⊢ y.leNat n = false
Tactic:
exact mono' h hy
State after:
no goals

State before:
case inr
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true ∨ y.leNat n = false
Tactic:
left
State after:
case inr.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true

State before:
case inr.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true
Tactic:
exact mono h hx
State after:
no goals