[GOAL]
α : Type u_1
a b a' b' : α
inst✝ : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
⊢ a' = b'
[PROOFSTEP]
rw [← sub_eq_zero] at p ⊢
[GOAL]
α : Type u_1
a b a' b' : α
inst✝ : AddGroup α
p✝ : a = b
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0
[PROOFSTEP]
rwa [sub_eq_zero, p] at H


[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : Nat.AtLeastTwo n
⊢ OfNat.ofNat n * r = n • r
[PROOFSTEP]
simp only [nsmul_eq_mul, Nat.cast_eq_ofNat]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : Nat.AtLeastTwo n
⊢ r * OfNat.ofNat n = n • r
[PROOFSTEP]
simp only [nsmul_eq_mul', Nat.cast_eq_ofNat]


[GOAL]
α : Sort ?u.352
p q : Prop
s : α → Prop
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
[PROOFSTEP]
rw [not_not, or_comm]


[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)
[PROOFSTEP]
rw [mul_assoc, ← zpow_add]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * b * b ^ m = a * b ^ (m + 1)
[PROOFSTEP]
rw [mul_assoc, mul_self_zpow]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * b ^ n * b = a * b ^ (n + 1)
[PROOFSTEP]
rw [mul_assoc, mul_zpow_self]