calc 
(x + y)^2 = (x + y)*(x + y) := by rw [square_eq_two_times]
_ = x*x + y*x + (x*y + y*y) := by rw [Distrib.left_distrib,
Distrib.right_distrib, Distrib.right_distrib]
_ = x*x + x*y + x*y + y*y := by simp only [add_left_comm,
add_assoc, mul_comm]
_ = x*x + (x*y + x*y) + y*y := by simp only [add_assoc]
_ = x*x + 2*(x*y) + y*y := by rw [← double_eq_two_additions]
_ = x^2 + 2*(x*y) + y^2 := by rw [square_eq_two_times,
square_eq_two_times]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + 2 * (x * y) + y ^ 2
no goals