α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b
α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b
rw [abs_mul_abs_self]
no goals
α : Type u_1
inst✝ : LinearOrderedCommRing α
a✝ b✝ c d a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
  neg_add_rev, neg_neg, add_assoc]