rw [h1]
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
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