Sextic Cosine Power Reduction

  -- cos^6 = (cos^2)^3
  have h1 : Real.cos x ^ 6 = (Real.cos x ^ 2) ^ 3 := by ring
  rw [h1]
  -- cos^2 = (1 + cos(2x))/2
  have h2 : Real.cos x ^ 2 = (1 + Real.cos (2 * x)) / 2 := by rw [Real.cos_sq]; ring
  rw [h2]
  -- Expand ((1 + cos(2x))/2)^3
  have h3 : ((1 + Real.cos (2 * x)) / 2) ^ 3 =
      (1 + 3 * Real.cos (2 * x) + 3 * Real.cos (2 * x) ^ 2 + Real.cos (2 * x) ^ 3) / 8 := by
    field_simp
    ring
  rw [h3]
  -- Apply double-angle formulas to cos^2(2x) and cos^3(2x)
  have h4 : Real.cos (2 * x) ^ 2 = (1 + Real.cos (4 * x)) / 2 := by
    rw [Real.cos_sq]; ring_nf
  have h5 : Real.cos (2 * x) ^ 3 = (Real.cos (6 * x) + 3 * Real.cos (2 * x)) / 4 := by
    convert cos_cube_formula (2 * x) using 1
    ring_nf
  rw [h4, h5]
  field_simp
  ring