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

State before:
i j : Int
⊢ i ≤ j → i ≠ j → i < j
Tactic:
intro hle hne
State after:
i j : Int
hle : i ≤ j
hne : i ≠ j
⊢ i < j

State before:
i j : Int
hle : i ≤ j
hne : i ≠ j
⊢ i < j
Tactic:
cases lt_or_eq_of_le hle with
| inl hlt => exact hlt
| inr heq => absurd heq; exact hne
State after:
no goals

State before:
case inl
i j : Int
hle : i ≤ j
hne : i ≠ j
hlt : i < j
⊢ i < j
Tactic:
exact hlt
State after:
no goals

State before:
case inr
i j : Int
hle : i ≤ j
hne : i ≠ j
heq : i = j
⊢ i < j
Tactic:
absurd heq
State after:
case inr
i j : Int
hle : i ≤ j
hne : i ≠ j
heq : i = j
⊢ ¬i = j

State before:
case inr
i j : Int
hle : i ≤ j
hne : i ≠ j
heq : i = j
⊢ ¬i = j
Tactic:
exact hne
State after:
no goals