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

State before:
x y : ENat
⊢ ¬x < y ↔ y ≤ x
Tactic:
constructor
State after:
case mp
x y : ENat
⊢ ¬x < y → y ≤ x

case mpr
x y : ENat
⊢ y ≤ x → ¬x < y

State before:
case mp
x y : ENat
⊢ ¬x < y → y ≤ x
Tactic:
intro h n
State after:
case mp
x y : ENat
h : ¬x < y
n : Nat
⊢ y.leNat n = true ∨ x.leNat n = false

State before:
case mp
x y : ENat
h : ¬x < y
n : Nat
⊢ y.leNat n = true ∨ x.leNat n = false
Tactic:
match hx : x.leNat n, hy : y.leNat n with
| false, _ => right; rfl
| _, true => left; rfl
| true, false => absurd h; exists n
State after:
no goals

State before:
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = false
hy : y.leNat n = x✝
⊢ x✝ = true ∨ false = false
Tactic:
right
State after:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = false
hy : y.leNat n = x✝
⊢ false = false

State before:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = false
hy : y.leNat n = x✝
⊢ false = false
Tactic:
rfl
State after:
no goals

State before:
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = x✝
hy : y.leNat n = true
⊢ true = true ∨ x✝ = false
Tactic:
left
State after:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = x✝
hy : y.leNat n = true
⊢ true = true

State before:
case h
x y : ENat
h : ¬x < y
n : Nat
x✝ : Bool
hx : x.leNat n = x✝
hy : y.leNat n = true
⊢ true = true
Tactic:
rfl
State after:
no goals

State before:
x y : ENat
h : ¬x < y
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ false = true ∨ true = false
Tactic:
absurd h
State after:
x y : ENat
h : ¬x < y
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ x < y

State before:
x y : ENat
h : ¬x < y
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ x < y
Tactic:
exists n
State after:
no goals

State before:
case mpr
x y : ENat
⊢ y ≤ x → ¬x < y
Tactic:
intro h ⟨n₀, hx, hy⟩
State after:
case mpr
x y : ENat
h : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
⊢ False

State before:
case mpr
x y : ENat
h : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
⊢ False
Tactic:
cases h n₀ with
| inl h => simp only [h] at hy
| inr h => simp only [h] at hx
State after:
no goals

State before:
case mpr.inl
x y : ENat
h✝ : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
h : y.leNat n₀ = true
⊢ False
Tactic:
simp only [h] at hy
State after:
no goals

State before:
case mpr.inr
x y : ENat
h✝ : y ≤ x
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
h : x.leNat n₀ = false
⊢ False
Tactic:
simp only [h] at hx
State after:
no goals