x y : ℂ
h2 : 2 ≠ 0
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
x y : ℂ
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
have h2 : (2 : ℂ) ≠ 0 := by norm_num
case calc_1
x y : ℂ
h2 : 2 ≠ 0
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

case calc_2
x y : ℂ
h2 : 2 ≠ 0
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

case calc_3
x y : ℂ
h2 : 2 ≠ 0
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)
x y : ℂ
h2 : 2 ≠ 0
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
calc
  cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
  _ =
      cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
        (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
    ?_
  _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
no goals
case calc_3
x y : ℂ
h2 : 2 ≠ 0
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)
ring
no goals
x y : ℂ
⊢ 2 ≠ 0
norm_num
no goals
case calc_1
x y : ℂ
h2 : 2 ≠ 0
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
congr <;> field_simp [h2]
no goals
case calc_2
x y : ℂ
h2 : 2 ≠ 0
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
rw [cos_add, cos_sub]