[GOAL]
θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 :=
  by
  rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul, add_eq_zero_iff_eq_neg,
    neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]
  congr 3; ring_nf
[GOAL]
θ : ℂ
⊢ (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
[PROOFSTEP]
rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul, add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul,
  ← div_eq_iff (exp_ne_zero _), ← exp_sub]
[GOAL]
θ : ℂ
⊢ exp (θ * I - -θ * I) = -1 ↔ exp (2 * θ * I) = -1
[PROOFSTEP]
congr 3
[GOAL]
θ : ℂ
⊢ exp (θ * I - -θ * I) = -1 ↔ exp (2 * θ * I) = -1
[PROOFSTEP]
ring_nf
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
⊢ (∃ n, 2 * I * θ = ↑π * I + ↑n * (2 * ↑π * I)) ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
refine' exists_congr fun x => _
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2
[PROOFSTEP]
refine' (iff_of_eq <| congr_arg _ _).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
x : ℤ
⊢ ↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)
[PROOFSTEP]
field_simp
[GOAL]
θ : ℂ
h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1
x : ℤ
⊢ (↑π * I + ↑x * (2 * ↑π * I)) * 2 = 2 * I * ((2 * ↑x + 1) * ↑π)
[PROOFSTEP]
ring
[GOAL]
θ : ℂ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
rw [← not_exists, not_iff_not, cos_eq_zero_iff]
[GOAL]
θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
rw [← Complex.cos_sub_pi_div_two, cos_eq_zero_iff]
[GOAL]
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) ↔ ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
constructor
[GOAL]
case mp
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) → ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mp.intro
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ ∃ k, θ = ↑k * ↑π
[PROOFSTEP]
use k + 1
[GOAL]
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ θ = ↑(k + 1) * ↑π
[PROOFSTEP]
field_simp [eq_add_of_sub_eq hk]
[GOAL]
case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ (2 * ↑k + 1) * ↑π + ↑π = (↑k + 1) * ↑π * 2
[PROOFSTEP]
ring
[GOAL]
case mpr
θ : ℂ
⊢ (∃ k, θ = ↑k * ↑π) → ∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case mpr.intro
k : ℤ
⊢ ∃ k_1, ↑k * ↑π - ↑π / 2 = (2 * ↑k_1 + 1) * ↑π / 2
[PROOFSTEP]
use k - 1
[GOAL]
case h
k : ℤ
⊢ ↑k * ↑π - ↑π / 2 = (2 * ↑(k - 1) + 1) * ↑π / 2
[PROOFSTEP]
field_simp
[GOAL]
case h
k : ℤ
⊢ ↑k * ↑π * 2 - ↑π = (2 * (↑k - 1) + 1) * ↑π
[PROOFSTEP]
ring
[GOAL]
θ : ℂ
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π
[PROOFSTEP]
rw [← not_exists, not_iff_not, sin_eq_zero_iff]
[GOAL]
θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
have h := (sin_two_mul θ).symm
[GOAL]
θ : ℂ
h : 2 * sin θ * cos θ = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
rw [mul_assoc] at h 
[GOAL]
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
rw [tan, div_eq_zero_iff, ← mul_eq_zero, ← zero_mul (1 / 2 : ℂ), mul_one_div,
  CancelDenoms.cancel_factors_eq_div h two_ne_zero, mul_comm]
[GOAL]
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ sin (θ * 2) / 2 = 0 / 2 ↔ ∃ k, θ = ↑k * ↑π / 2
[PROOFSTEP]
simpa only [zero_div, zero_mul, Ne.def, not_false_iff, field_simps] using sin_eq_zero_iff
[GOAL]
θ : ℂ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π / 2
[PROOFSTEP]
rw [← not_exists, not_iff_not, tan_eq_zero_iff]
[GOAL]
n : ℤ
⊢ ∃ k, ↑n * ↑π / 2 = ↑k * ↑π / 2
[PROOFSTEP]
use n
[GOAL]
x y : ℂ
⊢ cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
[PROOFSTEP]
rw [cos_sub_cos]
[GOAL]
x y : ℂ
⊢ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0 ↔ sin ((x + y) / 2) = 0 ∨ sin ((x - y) / 2) = 0
[PROOFSTEP]
simp [(by norm_num : (2 : ℂ) ≠ 0)]
[GOAL]
x y : ℂ
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 ↔ (∃ k, y = 2 * ↑k * ↑π + x) ∨ ∃ k, y = 2 * ↑k * ↑π - x
[PROOFSTEP]
apply or_congr
[GOAL]
case h₁
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π + x
[PROOFSTEP]
field_simp [sin_eq_zero_iff, (by norm_num : -(2 : ℂ) ≠ 0), eq_sub_iff_add_eq', sub_eq_iff_eq_add, mul_comm (2 : ℂ),
  mul_right_comm _ (2 : ℂ)]
[GOAL]
x y : ℂ
⊢ -2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case h₂
x y : ℂ
⊢ sin ((x + y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π - x
[PROOFSTEP]
field_simp [sin_eq_zero_iff, (by norm_num : -(2 : ℂ) ≠ 0), eq_sub_iff_add_eq', sub_eq_iff_eq_add, mul_comm (2 : ℂ),
  mul_right_comm _ (2 : ℂ)]
[GOAL]
x y : ℂ
⊢ -2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case h₁
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) ↔ ∃ k, y = ↑k * ↑π * 2 + x
[PROOFSTEP]
constructor
[GOAL]
case h₁.mp
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) → ∃ k, y = ↑k * ↑π * 2 + x
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case h₁.mp.intro
y : ℂ
k : ℤ
⊢ ∃ k_1, y = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + y)
[PROOFSTEP]
use-k
[GOAL]
case h
y : ℂ
k : ℤ
⊢ y = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + y)
[PROOFSTEP]
simp
[GOAL]
case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case h₁.mpr.intro
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)
[PROOFSTEP]
use-k
[GOAL]
case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)
[PROOFSTEP]
simp
[GOAL]
x y : ℂ
⊢ sin x = sin y ↔ ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]
[GOAL]
x y : ℂ
⊢ (∃ k, y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ∨ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2) ↔
    ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
refine' exists_congr fun k => or_congr _ _
[GOAL]
case refine'_1
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ↔ y = 2 * ↑k * ↑π + x
[PROOFSTEP]
refine' Eq.congr rfl _
[GOAL]
case refine'_2
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 ↔ y = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
refine' Eq.congr rfl _
[GOAL]
case refine'_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 = 2 * ↑k * ↑π + x
[PROOFSTEP]
field_simp
[GOAL]
case refine'_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 = (2 * ↑k + 1) * ↑π - x
[PROOFSTEP]
field_simp
[GOAL]
case refine'_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π * 2 + (x * 2 - ↑π) + ↑π = (2 * ↑k * ↑π + x) * 2
[PROOFSTEP]
ring
[GOAL]
case refine'_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π * 2 - (x * 2 - ↑π) + ↑π = ((2 * ↑k + 1) * ↑π - x) * 2
[PROOFSTEP]
ring
[GOAL]
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
rcases h with (⟨h1, h2⟩ | ⟨⟨k, rfl⟩, ⟨l, rfl⟩⟩)
[GOAL]
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
rw [tan, sin_add, cos_add, ←
  div_div_div_cancel_right (sin x * cos y + cos x * sin y)
    (mul_ne_zero (cos_ne_zero_iff.mpr h1) (cos_ne_zero_iff.mpr h2)),
  add_div, sub_div]
[GOAL]
case inl.intro
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
simp only [← div_mul_div_comm, tan, mul_one, one_mul, div_self (cos_ne_zero_iff.mpr h1),
  div_self (cos_ne_zero_iff.mpr h2)]
[GOAL]
case inr.intro.intro.intro
k l : ℤ
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
haveI t := tan_int_mul_pi_div_two
[GOAL]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
[GOAL]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan (↑(2 * k + 1) * ↑π / 2) = 0
hy : tan (↑(2 * l + 1) * ↑π / 2) = 0
hxy : tan (↑(2 * k + 1 + (2 * l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one, hx, hy] at hx hy hxy 
[GOAL]
case inr.intro.intro.intro
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))
[PROOFSTEP]
rw [hx, hy, add_zero, zero_div, mul_div_assoc, mul_div_assoc, ← add_mul (2 * (k : ℂ) + 1) (2 * l + 1) (π / 2), ←
  mul_div_assoc, hxy]
[GOAL]
z : ℂ
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
by_cases h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
[GOAL]
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
[GOAL]
case neg
z : ℂ
h : ¬∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
rw [not_forall_not] at h 
[GOAL]
case neg
z : ℂ
h : ∃ x, z = (2 * ↑x + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
[PROOFSTEP]
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]
[GOAL]
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)
[PROOFSTEP]
rw [tan_add h, tan_mul_I, mul_assoc]
[GOAL]
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan z = (tan ↑z.re + tanh ↑z.im * I) / (1 - tan ↑z.re * tanh ↑z.im * I)
[PROOFSTEP]
convert tan_add_mul_I h
[GOAL]
case h.e'_2.h.e'_1
z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ z = ↑z.re + ↑z.im * I
[PROOFSTEP]
exact (re_add_im z).symm
[GOAL]
z w : ℂ
⊢ cos z = w ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
z w : ℂ
⊢ cos z - w = 0 ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0
[PROOFSTEP]
field_simp [cos, exp_neg, exp_ne_zero]
[GOAL]
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
[PROOFSTEP]
refine' Eq.congr _ rfl
[GOAL]
z w : ℂ
⊢ exp (z * I) * exp (z * I) + 1 - exp (z * I) * 2 * w = exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1
[PROOFSTEP]
ring
[GOAL]
⊢ Function.Surjective cos
[PROOFSTEP]
intro x
[GOAL]
x : ℂ
⊢ ∃ a, cos a = x
[PROOFSTEP]
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, mul_zero] at hw 
[GOAL]
x : ℂ
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
[PROOFSTEP]
rcases exists_quadratic_eq_zero one_ne_zero ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with ⟨w, hw⟩
[GOAL]
case intro
x w : ℂ
hw : 1 * w * w + ?m.63171 * w + ?m.63172 = 0
⊢ ∃ w x_1, 1 * w * w + -2 * x * w + 1 = 0
[PROOFSTEP]
refine' ⟨w, _, hw⟩
[GOAL]
case intro
x w : ℂ
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro
x : ℂ
hw : 1 * 0 * 0 + -2 * x * 0 + 1 = 0
⊢ False
[PROOFSTEP]
simp only [zero_add, one_ne_zero, mul_zero] at hw 
[GOAL]
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ ∃ a, cos a = x
[PROOFSTEP]
refine' ⟨log w / I, cos_eq_iff_quadratic.2 _⟩
[GOAL]
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
[PROOFSTEP]
rw [div_mul_cancel _ I_ne_zero, exp_log w₀]
[GOAL]
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * w * w + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0
[PROOFSTEP]
convert hw using 1
[GOAL]
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
[PROOFSTEP]
ring
[GOAL]
⊢ Function.Surjective sin
[PROOFSTEP]
intro x
[GOAL]
x : ℂ
⊢ ∃ a, sin a = x
[PROOFSTEP]
rcases cos_surjective x with ⟨z, rfl⟩
[GOAL]
case intro
z : ℂ
⊢ ∃ a, sin a = cos z
[PROOFSTEP]
exact ⟨z + π / 2, sin_add_pi_div_two z⟩
[GOAL]
θ : ℝ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * π / 2
[PROOFSTEP]
exact_mod_cast @Complex.cos_eq_zero_iff θ
[GOAL]
θ : ℝ
⊢ cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * π / 2
[PROOFSTEP]
rw [← not_exists, not_iff_not, cos_eq_zero_iff]
[GOAL]
x y : ℝ
⊢ cos x = cos y ↔ ∃ k, y = 2 * ↑k * π + x ∨ y = 2 * ↑k * π - x
[PROOFSTEP]
exact_mod_cast @Complex.cos_eq_cos_iff x y
[GOAL]
x y : ℝ
⊢ sin x = sin y ↔ ∃ k, y = 2 * ↑k * π + x ∨ y = (2 * ↑k + 1) * π - x
[PROOFSTEP]
exact_mod_cast @Complex.sin_eq_sin_iff x y
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)
[PROOFSTEP]
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩ pi_div_two_pos.ne
    (sub_pos.2 hx') hx
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ 1
⊢ x ≤ sin (π / 2 * x)
[PROOFSTEP]
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.concaveOn.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩ (sub_nonneg.2 hx')
    hx
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ 2 / π * x < sin x
[PROOFSTEP]
rw [← inv_div]
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x
[PROOFSTEP]
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using
  @lt_sin_mul ((π / 2)⁻¹ * x) (mul_pos (inv_pos.2 pi_div_two_pos) hx)
    (by rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos])
[GOAL]
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < 1
[PROOFSTEP]
rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos]
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ 2 / π * x ≤ sin x
[PROOFSTEP]
rw [← inv_div]
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x
[PROOFSTEP]
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using
  @le_sin_mul ((π / 2)⁻¹ * x) (mul_nonneg (inv_nonneg.2 pi_div_two_pos.le) hx)
    (by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos])
[GOAL]
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1
[PROOFSTEP]
rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos]
