Theorem: Int.lt_compare (GMLInit/Data/Int.lean)

State before:
i j : Int
⊢ i < j → ∀ (k : Int), i < k ∨ k < j
Tactic:
intro hij k
State after:
i j : Int
hij : i < j
k : Int
⊢ i < k ∨ k < j

State before:
i j : Int
hij : i < j
k : Int
⊢ i < k ∨ k < j
Tactic:
cases Int.le_or_gt k i with
| inl hle => right; exact Int.lt_of_le_of_lt hle hij
| inr hgt => left; exact hgt
State after:
no goals

State before:
case inl
i j : Int
hij : i < j
k : Int
hle : k ≤ i
⊢ i < k ∨ k < j
Tactic:
right
State after:
case inl.h
i j : Int
hij : i < j
k : Int
hle : k ≤ i
⊢ k < j

State before:
case inl.h
i j : Int
hij : i < j
k : Int
hle : k ≤ i
⊢ k < j
Tactic:
exact Int.lt_of_le_of_lt hle hij
State after:
no goals

State before:
case inr
i j : Int
hij : i < j
k : Int
hgt : i < k
⊢ i < k ∨ k < j
Tactic:
left
State after:
case inr.h
i j : Int
hij : i < j
k : Int
hgt : i < k
⊢ i < k

State before:
case inr.h
i j : Int
hij : i < j
k : Int
hgt : i < k
⊢ i < k
Tactic:
exact hgt
State after:
no goals