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

State before:
x y z : ENat
⊢ x < y → y ≤ z → x < z
Tactic:
intro ⟨n, hx, hy⟩ hyz
State after:
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
⊢ x < z

State before:
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
⊢ x < z
Tactic:
cases hyz n with
| inl h => simp only [h] at hy
| inr hz => exists n
State after:
no goals

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

State before:
case inr
x y z : ENat
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hyz : y ≤ z
hz : z.leNat n = false
⊢ x < z
Tactic:
exists n
State after:
no goals