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

State before:
n : Nat
x : ENat
⊢ ENat.ofNat n < x ↔ ENat.ofNat (n + 1) ≤ x
Tactic:
constructor
State after:
case mp
n : Nat
x : ENat
⊢ ENat.ofNat n < x → ENat.ofNat (n + 1) ≤ x

case mpr
n : Nat
x : ENat
⊢ ENat.ofNat (n + 1) ≤ x → ENat.ofNat n < x

State before:
case mp
n : Nat
x : ENat
⊢ ENat.ofNat n < x → ENat.ofNat (n + 1) ≤ x
Tactic:
intro ⟨m, h, hm⟩ k
State after:
case mp
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
k : Nat
⊢ (ENat.ofNat (n + 1)).leNat k = true ∨ x.leNat k = false

State before:
case mp
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
k : Nat
⊢ (ENat.ofNat (n + 1)).leNat k = true ∨ x.leNat k = false
Tactic:
rw [leNat_coe_eq_true_iff_le] at h ⊢
State after:
case mp
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
⊢ n + 1 ≤ k ∨ x.leNat k = false

State before:
case mp
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
⊢ n + 1 ≤ k ∨ x.leNat k = false
Tactic:
cases Nat.lt_or_ge n k with
| inl hlt => left; exact hlt
| inr hge => right; apply mono' hge; apply mono' h; exact hm
State after:
no goals

State before:
case mp.inl
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hlt : n < k
⊢ n + 1 ≤ k ∨ x.leNat k = false
Tactic:
left
State after:
case mp.inl.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hlt : n < k
⊢ n + 1 ≤ k

State before:
case mp.inl.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hlt : n < k
⊢ n + 1 ≤ k
Tactic:
exact hlt
State after:
no goals

State before:
case mp.inr
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ n + 1 ≤ k ∨ x.leNat k = false
Tactic:
right
State after:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat k = false

State before:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat k = false
Tactic:
apply mono' hge
State after:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat n = false

State before:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat n = false
Tactic:
apply mono' h
State after:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat m = false

State before:
case mp.inr.h
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
hge : n ≥ k
⊢ x.leNat m = false
Tactic:
exact hm
State after:
no goals

State before:
case mpr
n : Nat
x : ENat
⊢ ENat.ofNat (n + 1) ≤ x → ENat.ofNat n < x
Tactic:
intro h
State after:
case mpr
n : Nat
x : ENat
h : ENat.ofNat (n + 1) ≤ x
⊢ ENat.ofNat n < x

State before:
case mpr
n : Nat
x : ENat
h : ENat.ofNat (n + 1) ≤ x
⊢ ENat.ofNat n < x
Tactic:
cases h n with
| inl h => rw [leNat_coe_eq_true_iff_le] at h; absurd h; exact Nat.lt_irrefl n
| inr h => exists n; rw [leNat_coe_eq_true_iff_le]; exact ⟨Nat.le_refl n, h⟩
State after:
no goals

State before:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : (ENat.ofNat (n + 1)).leNat n = true
⊢ ENat.ofNat n < x
Tactic:
rw [leNat_coe_eq_true_iff_le] at h
State after:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ENat.ofNat n < x

State before:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ENat.ofNat n < x
Tactic:
absurd h
State after:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ¬n + 1 ≤ n

State before:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ¬n + 1 ≤ n
Tactic:
exact Nat.lt_irrefl n
State after:
no goals

State before:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ ENat.ofNat n < x
Tactic:
exists n
State after:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false

State before:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
Tactic:
rw [leNat_coe_eq_true_iff_le]
State after:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ n ≤ n ∧ x.leNat n = false

State before:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ n ≤ n ∧ x.leNat n = false
Tactic:
exact ⟨Nat.le_refl n, h⟩
State after:
no goals