Theorem: MyRing.eq_neg_of_add_eq_zeroαα (MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean)

State before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ a = -b
Tactic:
symm
State after:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -b = a

State before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -b = a
Tactic:
apply neg_eq_of_add_eq_zero
State after:
case h
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ b + a = 0

State before:
case h
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ b + a = 0
Tactic:
rw [add_comm, h]
State after:
no goals