Theorem: LoVe.binomial_square (LoVe/Labs/Lab3Solution.lean)

State before:
a b : ℕ
⊢ (a + b) * (a + b) = a * (a + b) + b * (a + b)
Tactic:
simp only [add_mul, mul_add]
State after:
a b : ℕ
⊢ a * a + b * a + (a * b + b * b) = a * a + a * b + (b * a + b * b)

State before:
a b : ℕ
⊢ a * a + b * a + (a * b + b * b) = a * a + a * b + (b * a + b * b)
Tactic:
ac_rfl
State after:
no goals

State before:
a b : ℕ
⊢ a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
Tactic:
simp only [add_mul, mul_add]
State after:
a b : ℕ
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b

State before:
a b : ℕ
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b
Tactic:
ac_rfl
State after:
no goals

State before:
a b : ℕ
⊢ a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
Tactic:
simp only [mul_comm]
State after:
no goals

State before:
a b : ℕ
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
Tactic:
simp only [Nat.two_mul, add_mul, add_assoc]
State after:
no goals