simp only [add_mul, mul_add]
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
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