Theorem: Int.add_left_cancel' (GMLInit/Data/Int.lean)

State before:
i j k : Int
h : i + j = i + k
⊢ j = 0 + j
Tactic:
rw [Int.zero_add]
State after:
no goals

State before:
i j k : Int
h : i + j = i + k
⊢ 0 + j = -i + i + j
Tactic:
rw [Int.add_neg_self_left]
State after:
no goals

State before:
i j k : Int
h : i + j = i + k
⊢ -i + i + j = -i + (i + j)
Tactic:
rw [Int.add_assoc]
State after:
no goals

State before:
i j k : Int
h : i + j = i + k
⊢ -i + (i + j) = -i + (i + k)
Tactic:
rw [h]
State after:
no goals

State before:
i j k : Int
h : i + j = i + k
⊢ -i + (i + k) = -i + i + k
Tactic:
rw [Int.add_assoc]
State after:
no goals

State before:
i j k : Int
h : i + j = i + k
⊢ -i + i + k = 0 + k
Tactic:
rw [Int.add_neg_self_left]
State after:
no goals

State before:
i j k : Int
h : i + j = i + k
⊢ 0 + k = k
Tactic:
rw [Int.zero_add]
State after:
no goals