no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
⊢ a * e + c = b * e + d ↔ a * e + c = d + b * e
simp [add_comm]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ d + b * e - b * e = d
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ a * e + c - b * e = d
rw [h]
no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ d + b * e - b * e = d
simp
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = a * e + c - b * e + b * e
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = d + b * e
rw [← h]
no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = a * e + c - b * e + b * e
simp
no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
⊢ a * e + c - b * e = d ↔ (a - b) * e + c = d
simp [sub_mul, sub_add_eq_add_sub]