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

State before:
i j : Int
⊢ i ≤ j → i < j ∨ i = j
Tactic:
intro hle
State after:
i j : Int
hle : i ≤ j
⊢ i < j ∨ i = j

State before:
i j : Int
hle : i ≤ j
⊢ i < j ∨ i = j
Tactic:
match le.dest' hle with
| ⟨0, (h : j = i + 0)⟩ =>
  right
  rw [h, Int.add_zero]
| ⟨n+1, (h : j = i + (ofNat n + 1))⟩ =>
  left
  rw [Int.lt_iff_succ_le]
  rw [h, ←Int.add_assoc, Int.add_right_comm]
  apply Int.le.intro'
State after:
no goals

State before:
i j : Int
hle : i ≤ j
h : j = i + 0
⊢ i < j ∨ i = j
Tactic:
right
State after:
case h
i j : Int
hle : i ≤ j
h : j = i + 0
⊢ i = j

State before:
case h
i j : Int
hle : i ≤ j
h : j = i + 0
⊢ i = j
Tactic:
rw [h, Int.add_zero]
State after:
no goals

State before:
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i < j ∨ i = j
Tactic:
left
State after:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i < j

State before:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i < j
Tactic:
rw [Int.lt_iff_succ_le]
State after:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ j

State before:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ j
Tactic:
rw [h, ←Int.add_assoc, Int.add_right_comm]
State after:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ i + 1 + ofNat n

State before:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ i + 1 + ofNat n
Tactic:
apply Int.le.intro'
State after:
no goals