rw [add_assoc] at hw1
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + z + w = b
⊢ a = b
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
⊢ a = b