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 : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (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 : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b

State before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (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 : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * 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 : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * 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

State before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b
Tactic:
rw [h1]
State after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * (a + b) + b * (a + b) = a * a + 2 * a * b + b * b

State before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * (a + b) + b * (a + b) = a * a + 2 * a * b + b * b
Tactic:
rw [h2]
State after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + b * a + b * b = a * a + 2 * a * b + b * b

State before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + b * a + b * b = a * a + 2 * a * b + b * b
Tactic:
rw [h3]
State after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b

State before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
Tactic:
rw [h4]
State after:
no goals