factoring

Stream: new members

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

-- theorem factor (x y z : ℤ) : (x + y + z) ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + 2 * x * y + 2 * x * z
--   + 2 * y * z := by
--   sorry

example (a b c : ℤ  ) :  0 ≤  16 * a ^ 2 * c ^ 2 - 48 * a * c ^ 3 + 36 * c ^ 4 + 8 * a * c ^ 2 - 12 * c ^ 3  + c ^ 2:= by
  -- goal becomes  0 ≤ (6 * c ^ 2 - 4 * a * c - c) ^ 2
  have h1 : 16 * a ^ 2 * c ^ 2 - 48 * a * c ^ 3 + 36 * c ^ 4 + 8 * a * c ^ 2 - 12 * c ^ 3  + c ^ 2 = (6 * c ^ 2 - 4 * a * c - c) ^ 2 := by
    have c1 : 16 * a ^ 2 * c ^ 2 - 48 * a * c ^ 3 + 36 * c ^ 4 + 8 * a * c ^ 2 - 12 * c ^ 3  + c ^ 2
    = (4 * a * c) ^ 2 + (6 * c ^ 2) + c ^ 2 + 2 * (6 * c ^ 2) *(- 4 * a * c) + 2 * (6 * c ^ 2) * (- c)
      + 2 * (- 4 * a * c) * (- c) := by
      sorry
    sorry
  rw[h1]
  exact sq_nonneg (6 * c ^ 2 - 4 * a * c - c)

Does anyone know how to complete this code?

[chenjulang]

try simp? or apply?