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

State before:
x y z : ENat
⊢ x ≤ y → y ≤ z → x ≤ z
Tactic:
intro hxy hyz n
State after:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
⊢ x.leNat n = true ∨ z.leNat n = false

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

State before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = true
hz : z.leNat n = true
⊢ true = true ∨ true = false
Tactic:
trivial
State after:
no goals

State before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = true
hz : z.leNat n = false
⊢ true = true ∨ false = false
Tactic:
trivial
State after:
no goals

State before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hz : z.leNat n = true
⊢ true = true ∨ true = false
Tactic:
trivial
State after:
no goals

State before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
hz : z.leNat n = false
⊢ true = true ∨ false = false
Tactic:
trivial
State after:
no goals

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

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

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

State before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
hz : z.leNat n = false
⊢ false = true ∨ false = false
Tactic:
trivial
State after:
no goals

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

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

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

State before:
x y z : ENat
hxy : x ≤ y
hyz : y ≤ z
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
hz : z.leNat n = false
⊢ false = true ∨ false = false
Tactic:
trivial
State after:
no goals