x : ℂ
⊢ ∃ a, cos a = x
⊢ Function.Surjective cos
intro x
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ ∃ a, cos a = x
x : ℂ
⊢ ∃ a, cos a = x
obtain ⟨w, w₀, hw⟩ : ∃ (w : _) (_ : w ≠ 0), 1 * w * w + -2 * x * w + 1 = 0 := by
  rcases exists_quadratic_eq_zero one_ne_zero
      ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
    ⟨w, hw⟩
  refine' ⟨w, _, hw⟩
  rintro rfl
  simp only [zero_add, one_ne_zero, MulZeroClass.mul_zero] at hw
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ exp (log w / I * I) ^ 2 - 2 * x * exp (log w / I * I) + 1 = 0
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ ∃ a, cos a = x
refine' ⟨log w / I, cos_eq_iff_quadratic.2 _⟩
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ exp (log w / I * I) ^ 2 - 2 * x * exp (log w / I * I) + 1 = 0
rw [div_mul_cancel _ I_ne_zero, exp_log w₀]
case h.e'_2
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 1 * w * w + -2 * x * w + 1
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0
convert hw using 1
no goals
case h.e'_2
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 1 * w * w + -2 * x * w + 1
ring
case intro
x w : ℂ
hw : 1 * w * w + ?m.62077 * w + ?m.62078 = 0
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
x : ℂ
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
rcases exists_quadratic_eq_zero one_ne_zero
    ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
  ⟨w, hw⟩
case intro
x w : ℂ
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ≠ 0
case intro
x w : ℂ
hw : 1 * w * w + ?m.62077 * w + ?m.62078 = 0
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
refine' ⟨w, _, hw⟩
case intro
x : ℂ
hw : 1 * 0 * 0 + -2 * x * 0 + 1 = 0
⊢ False
case intro
x w : ℂ
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ≠ 0
rintro rfl
no goals
case intro
x : ℂ
hw : 1 * 0 * 0 + -2 * x * 0 + 1 = 0
⊢ False
simp only [zero_add, one_ne_zero, MulZeroClass.mul_zero] at hw