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

State before:
i j : Int
⊢ i ≤ j ↔ i < j + 1
Tactic:
rw [Int.lt_iff_succ_le]
State after:
i j : Int
⊢ i ≤ j ↔ i + 1 ≤ j + 1

State before:
i j : Int
⊢ i ≤ j ↔ i + 1 ≤ j + 1
Tactic:
constructor
State after:
case mp
i j : Int
⊢ i ≤ j → i + 1 ≤ j + 1

case mpr
i j : Int
⊢ i + 1 ≤ j + 1 → i ≤ j

State before:
case mp
i j : Int
⊢ i ≤ j → i + 1 ≤ j + 1
Tactic:
apply Int.add_le_add_right (c:=1)
State after:
no goals

State before:
case mpr
i j : Int
⊢ i + 1 ≤ j + 1 → i ≤ j
Tactic:
apply Int.le_of_add_le_add_right
State after:
no goals