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

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

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

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

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

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

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

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