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

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

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

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

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