Theorem: binomial_formula (PowerCalc/Examples/Polynomials.lean)

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + 2 * (x * y) + y ^ 2
Tactic:
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]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) ^ 2 = (x + y) * (x + y)
Tactic:
rw [square_eq_two_times]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) * (x + y) = x * x + y * x + (x * y + y * y)
Tactic:
rw [Distrib.left_distrib,
Distrib.right_distrib, Distrib.right_distrib]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + y * x + (x * y + y * y) = x * x + x * y + x * y + y * y
Tactic:
simp only [add_left_comm,
add_assoc, mul_comm]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + x * y + x * y + y * y = x * x + (x * y + x * y) + y * y
Tactic:
simp only [add_assoc]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + (x * y + x * y) + y * y = x * x + 2 * (x * y) + y * y
Tactic:
rw [← double_eq_two_additions]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + 2 * (x * y) + y * y = x ^ 2 + 2 * (x * y) + y ^ 2
Tactic:
rw [square_eq_two_times,
square_eq_two_times]
State after:
no goals