a b : Int
h : a - b = 0
this : 0 + b = b
⊢ a = b
a b : Int
h : a - b = 0
⊢ a = b
have : 0 + b = b := by rw [Int.zero_add]
a b : Int
h : a - b = 0
this✝ : 0 + b = b
this : a - b + b = b
⊢ a = b
a b : Int
h : a - b = 0
this : 0 + b = b
⊢ a = b
have : a - b + b = b := by rwa [h]
no goals
a b : Int
h : a - b = 0
this✝ : 0 + b = b
this : a - b + b = b
⊢ a = b
rwa [Int.sub_eq_add_neg, Int.neg_add_cancel_right] at this
no goals
a b : Int
h : a - b = 0
⊢ 0 + b = b
rw [Int.zero_add]
no goals
a b : Int
h : a - b = 0
this : 0 + b = b
⊢ a - b + b = b
rwa [h]