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

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

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

State before:
case inl
i j : Int
hne : i ≠ j
hle : i ≤ j
⊢ i < j ∨ j < i
Tactic:
left
State after:
case inl.h
i j : Int
hne : i ≠ j
hle : i ≤ j
⊢ i < j

State before:
case inl.h
i j : Int
hne : i ≠ j
hle : i ≤ j
⊢ i < j
Tactic:
apply Int.lt_of_le_of_ne hle hne
State after:
no goals

State before:
case inr
i j : Int
hne : i ≠ j
hgt : j < i
⊢ i < j ∨ j < i
Tactic:
right
State after:
case inr.h
i j : Int
hne : i ≠ j
hgt : j < i
⊢ j < i

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