## formal statement:

theorem mathd_algebra_338 (a b c : ℝ) (h₀ : 3 * a + b + c = -3) (h₁ : a + 3 * b + c = 9)
    (h₂ : a + b + 3 * c = 19) : a * b * c = -56

## informal statement:

If $3a + b + c = -3, a+3b+c = 9, a+b+3c = 19$, then find $abc$. Show that it is -56.

## informal proof:

Summing all three equations yields that $5a + 5b + 5c = -3 + 9 + 19 = 25$. Thus, $a + b + c = 5$. Subtracting this from each of the given equations, we obtain that $2a = -8, 2b = 4, 2c = 14$. Thus, $a = -4, b = 2, c =7$, and their product is $abc = -4 \times 2 \times 7 = -56$.

## formal proof:


theorem mathd_algebra_338 (a b c : ℝ) (h₀ : 3 * a + b + c = -3) (h₁ : a + 3 * b + c = 9)
    (h₂ : a + b + 3 * c = 19) : a * b * c = -56 :=
  by
  have ha : a = -4; linarith
  have hb : b = 2; linarith
  have hc : c = 7; linarith
  rw [ha, hb, hc]
  norm_num
