z w : ℂ
⊢ cos z - w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
z w : ℂ
⊢ cos z = w ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
rw [← sub_eq_zero]
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
z w : ℂ
⊢ cos z - w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
field_simp [cos, exp_neg, exp_ne_zero]
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
refine' Eq.congr _ rfl
no goals
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1
ring