Theorem: zero_sub_eq_iff (FormalSnarksProject/SoundnessTactic/SoundnessProver.lean)

State before:
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ 0 - a = b ↔ a + b = 0
Tactic:
constructor
State after:
case mp
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ 0 - a = b → a + b = 0

case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ a + b = 0 → 0 - a = b

State before:
case mp
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ 0 - a = b → a + b = 0
Tactic:
aesop?
State after:
no goals

State before:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
⊢ a + b = 0 → 0 - a = b
Tactic:
intro h
State after:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ 0 - a = b

State before:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ 0 - a = b
Tactic:
rw [← add_right_inj a]
State after:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ a + (0 - a) = a + b

State before:
case mpr
R : Type u
inst✝ : AddCommGroup R
a b : R
h : a + b = 0
⊢ a + (0 - a) = a + b
Tactic:
simp [h]
State after:
no goals