a b c : Int
h : a + b = a + c
h₁ : -a + (a + b) = -a + (a + c)
⊢ b = c
a b c : Int
h : a + b = a + c
⊢ b = c
have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]
a b c : Int
h : a + b = a + c
h₁ : b = c
⊢ b = c
a b c : Int
h : a + b = a + c
h₁ : -a + (a + b) = -a + (a + c)
⊢ b = c
simp [← Int.add_assoc, Int.add_left_neg, Int.zero_add] at h₁
no goals
a b c : Int
h : a + b = a + c
h₁ : b = c
⊢ b = c
exact h₁
no goals
a b c : Int
h : a + b = a + c
⊢ -a + (a + b) = -a + (a + c)
rw [h]