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

State before:
i j : Int
⊢ i < j ∨ j ≤ i
Tactic:
cases Int.le_or_gt j i with
| inl h => right; exact h
| inr h => left; exact h
State after:
no goals

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

State before:
case inl.h
i j : Int
h : j ≤ i
⊢ j ≤ i
Tactic:
exact h
State after:
no goals

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

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