[GOAL]
⊢ 0 < 2 * π
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < π
[PROOFSTEP]
exact pi_pos
[GOAL]
x : ℝ
n : ℕ
⊢ ↑(↑n * x) = n • ↑x
[PROOFSTEP]
simpa only [nsmul_eq_mul] using coeHom.map_nsmul x n
[GOAL]
x : ℝ
n : ℤ
⊢ ↑(↑n * x) = n • ↑x
[PROOFSTEP]
simpa only [zsmul_eq_mul] using coeHom.map_zsmul x n
[GOAL]
ψ θ : ℝ
⊢ ↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * π * ↑k
[PROOFSTEP]
simp only [QuotientAddGroup.eq, AddSubgroup.zmultiples_eq_closure, AddSubgroup.mem_closure_singleton, zsmul_eq_mul',
  (sub_eq_neg_add _ _).symm, eq_comm]
  -- Porting note: added `rw`, `simp [Angle.coe, QuotientAddGroup.eq]` doesn't fire otherwise
[GOAL]
ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k
[PROOFSTEP]
rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]
[GOAL]
ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k
[PROOFSTEP]
simp only [AddSubgroup.zmultiples_eq_closure, AddSubgroup.mem_closure_singleton, zsmul_eq_mul',
  (sub_eq_neg_add _ _).symm, eq_comm]
[GOAL]
⊢ 2 * π - 0 = 2 * π * ↑1
[PROOFSTEP]
rw [sub_zero, Int.cast_one, mul_one]
[GOAL]
⊢ -↑π = ↑π
[PROOFSTEP]
rw [← coe_neg, angle_eq_iff_two_pi_dvd_sub]
[GOAL]
⊢ ∃ k, -π - π = 2 * π * ↑k
[PROOFSTEP]
use-1
[GOAL]
case h
⊢ -π - π = 2 * π * ↑(-1)
[PROOFSTEP]
simp [two_mul, sub_eq_add_neg]
[GOAL]
θ : ℝ
⊢ 2 • ↑(θ / 2) = ↑θ
[PROOFSTEP]
rw [← coe_nsmul, two_nsmul, add_halves]
[GOAL]
θ : ℝ
⊢ 2 • ↑(θ / 2) = ↑θ
[PROOFSTEP]
rw [← coe_zsmul, two_zsmul, add_halves]
[GOAL]
⊢ 2 • ↑(-π / 2) = ↑π
[PROOFSTEP]
rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]
[GOAL]
⊢ 2 • ↑(-π / 2) = ↑π
[PROOFSTEP]
rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]
[GOAL]
θ : Angle
⊢ θ - ↑π = θ + ↑π
[PROOFSTEP]
rw [sub_eq_add_neg, neg_coe_pi]
[GOAL]
⊢ 2 • ↑π = 0
[PROOFSTEP]
simp [← coe_nat_mul_eq_nsmul]
[GOAL]
⊢ 2 • ↑π = 0
[PROOFSTEP]
simp [← coe_int_mul_eq_zsmul]
[GOAL]
⊢ ↑π + ↑π = 0
[PROOFSTEP]
rw [← two_nsmul, two_nsmul_coe_pi]
[GOAL]
ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
[PROOFSTEP]
have : Int.natAbs 2 = 2 := rfl
[GOAL]
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
[PROOFSTEP]
rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero, Fin.val_one, zero_smul, coe_zero, add_zero,
  one_smul, Int.cast_two, mul_div_cancel_left (_ : ℝ) two_ne_zero]
[GOAL]
ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
[PROOFSTEP]
simp_rw [← coe_nat_zsmul, Nat.cast_ofNat, two_zsmul_eq_iff]
[GOAL]
θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
convert two_nsmul_eq_iff
[GOAL]
case h.e'_1.h.e'_3
θ : Angle
⊢ 0 = 2 • 0
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_2.h.e'_3
θ : Angle
⊢ ↑π = 0 + ↑π
[PROOFSTEP]
simp
[GOAL]
θ : Angle
⊢ 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
[PROOFSTEP]
rw [← not_or, ← two_nsmul_eq_zero_iff]
[GOAL]
θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]
[GOAL]
θ : Angle
⊢ 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
[PROOFSTEP]
rw [← not_or, ← two_zsmul_eq_zero_iff]
[GOAL]
θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
rw [← add_eq_zero_iff_eq_neg, ← two_nsmul, two_nsmul_eq_zero_iff]
[GOAL]
θ : Angle
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑π
[PROOFSTEP]
rw [← not_or, ← eq_neg_self_iff.not]
[GOAL]
θ : Angle
⊢ -θ = θ ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
rw [eq_comm, eq_neg_self_iff]
[GOAL]
θ : Angle
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑π
[PROOFSTEP]
rw [← not_or, ← neg_eq_self_iff.not]
[GOAL]
θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
have h : (π : Angle) = (2 : ℕ) • (π / 2 : ℝ) := by rw [two_nsmul, add_halves]
[GOAL]
θ : Angle
⊢ ↑π = ↑(2 • (π / 2))
[PROOFSTEP]
rw [two_nsmul, add_halves]
[GOAL]
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
nth_rw 1 [h]
[GOAL]
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
rw [coe_nsmul, two_nsmul_eq_iff]
  -- Porting note: `congr` didn't simplify the goal of iff of `Or`s
[GOAL]
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
convert Iff.rfl
[GOAL]
case h.e'_2.h.e'_2.h.e'_3
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(-π / 2) = ↑(π / 2) + ↑π
[PROOFSTEP]
rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, ← neg_sub, sub_neg_eq_add, add_assoc, add_halves, ← two_mul,
  coe_neg, coe_two_pi, neg_zero]
[GOAL]
θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]
[GOAL]
θ ψ : ℝ
⊢ cos θ = cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
[PROOFSTEP]
constructor
[GOAL]
case mp
θ ψ : ℝ
⊢ cos θ = cos ψ → ↑θ = ↑ψ ∨ ↑θ = -↑ψ
[PROOFSTEP]
intro Hcos
[GOAL]
case mp
θ ψ : ℝ
Hcos : cos θ = cos ψ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
[PROOFSTEP]
rw [← sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero, eq_false (two_ne_zero' ℝ), false_or_iff,
  sin_eq_zero_iff, sin_eq_zero_iff] at Hcos 
[GOAL]
case mp
θ ψ : ℝ
Hcos✝ : cos θ = cos ψ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ ∃ n, ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
[PROOFSTEP]
rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
[GOAL]
case mp.inl.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
[PROOFSTEP]
right
[GOAL]
case mp.inl.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = -↑ψ
[PROOFSTEP]
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn 
[GOAL]
case mp.inl.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ
[PROOFSTEP]
rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, coe_int_mul_eq_zsmul, mul_comm, coe_two_pi,
  zsmul_zero]
[GOAL]
case mp.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
[PROOFSTEP]
left
[GOAL]
case mp.inr.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ
[PROOFSTEP]
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn 
[GOAL]
case mp.inr.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑θ = ↑ψ
[PROOFSTEP]
rw [← hn, coe_add, mul_assoc, coe_int_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero, zero_add]
[GOAL]
case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ → cos θ = cos ψ
[PROOFSTEP]
rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]
[GOAL]
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - -ψ = 2 * π * ↑k) → cos θ = cos ψ
[PROOFSTEP]
rintro (⟨k, H⟩ | ⟨k, H⟩)
[GOAL]
case mpr.inl.intro
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ cos θ = cos ψ
case mpr.inr.intro θ ψ : ℝ k : ℤ H : θ - -ψ = 2 * π * ↑k ⊢ cos θ = cos ψ
[PROOFSTEP]
rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left _ (two_ne_zero' ℝ), mul_comm π _,
  sin_int_mul_pi, mul_zero]
[GOAL]
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ cos θ = cos ψ
[PROOFSTEP]
rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k, mul_div_cancel_left _ (two_ne_zero' ℝ),
  mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
[GOAL]
θ ψ : ℝ
⊢ sin θ = sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
constructor
[GOAL]
case mp
θ ψ : ℝ
⊢ sin θ = sin ψ → ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
intro Hsin
[GOAL]
case mp
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin 
[GOAL]
case mp
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
cases' cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h h
[GOAL]
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
left
[GOAL]
case mp.inl.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ
[PROOFSTEP]
rw [coe_sub, coe_sub] at h 
[GOAL]
case mp.inl.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ
[PROOFSTEP]
exact sub_right_inj.1 h
[GOAL]
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
right
[GOAL]
case mp.inr.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add, add_halves, sub_sub,
  sub_eq_zero] at h 
[GOAL]
case mp.inr.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π
[PROOFSTEP]
exact h.symm
[GOAL]
case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ
[PROOFSTEP]
rw [angle_eq_iff_two_pi_dvd_sub, ← eq_sub_iff_add_eq, ← coe_sub, angle_eq_iff_two_pi_dvd_sub]
[GOAL]
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - (π - ψ) = 2 * π * ↑k) → sin θ = sin ψ
[PROOFSTEP]
rintro (⟨k, H⟩ | ⟨k, H⟩)
[GOAL]
case mpr.inl.intro
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ sin θ = sin ψ
case mpr.inr.intro θ ψ : ℝ k : ℤ H : θ - (π - ψ) = 2 * π * ↑k ⊢ sin θ = sin ψ
[PROOFSTEP]
rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left _ (two_ne_zero' ℝ), mul_comm π _,
  sin_int_mul_pi, mul_zero, zero_mul]
[GOAL]
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ sin θ = sin ψ
[PROOFSTEP]
have H' : θ + ψ = 2 * k * π + π := by
  rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ← mul_assoc] at H 
[GOAL]
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ θ + ψ = 2 * ↑k * π + π
[PROOFSTEP]
rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ← mul_assoc] at H 
[GOAL]
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ sin θ = sin ψ
[PROOFSTEP]
rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π, mul_div_cancel_left _ (two_ne_zero' ℝ),
  cos_add_pi_div_two, sin_int_mul_pi, neg_zero, mul_zero]
[GOAL]
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ
[PROOFSTEP]
cases' cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc hc
[GOAL]
case inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ
[PROOFSTEP]
exact hc
[GOAL]
case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ
[PROOFSTEP]
cases' sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs hs
[GOAL]
case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ
[PROOFSTEP]
exact hs
[GOAL]
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero, hs] at hc 
[GOAL]
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)
[GOAL]
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ ↑θ = ↑ψ
[PROOFSTEP]
rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
  eq_false (ne_of_gt pi_pos), or_false_iff, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one, ← Int.int_cast_ofNat, ←
  Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn 
[GOAL]
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn✝ : n • (2 * π) = -1 * π
hn : n * 2 + 1 = 0
⊢ ↑θ = ↑ψ
[PROOFSTEP]
have : (n * 2 + 1) % (2 : ℤ) = 0 % (2 : ℤ) := congr_arg (· % (2 : ℤ)) hn
[GOAL]
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn✝ : n • (2 * π) = -1 * π
hn : n * 2 + 1 = 0
this : (n * 2 + 1) % 2 = 0 % 2
⊢ ↑θ = ↑ψ
[PROOFSTEP]
rw [add_comm, Int.add_mul_emod_self] at this 
[GOAL]
case inr.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn✝ : n • (2 * π) = -1 * π
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ
[PROOFSTEP]
exact absurd this one_ne_zero
[GOAL]
θ : Angle
ψ : ℝ
⊢ cos θ = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
ψ x✝ : ℝ
⊢ cos ↑x✝ = Real.cos ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ = -↑ψ
[PROOFSTEP]
exact cos_eq_iff_coe_eq_or_eq_neg
[GOAL]
θ ψ : Angle
⊢ cos θ = cos ψ ↔ θ = ψ ∨ θ = -ψ
[PROOFSTEP]
induction ψ using Real.Angle.induction_on
[GOAL]
case h
θ : Angle
x✝ : ℝ
⊢ cos θ = cos ↑x✝ ↔ θ = ↑x✝ ∨ θ = -↑x✝
[PROOFSTEP]
exact cos_eq_real_cos_iff_eq_or_eq_neg
[GOAL]
θ : Angle
ψ : ℝ
⊢ sin θ = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑π
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
ψ x✝ : ℝ
⊢ sin ↑x✝ = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π
[PROOFSTEP]
exact sin_eq_iff_coe_eq_or_add_eq_pi
[GOAL]
θ ψ : Angle
⊢ sin θ = sin ψ ↔ θ = ψ ∨ θ + ψ = ↑π
[PROOFSTEP]
induction ψ using Real.Angle.induction_on
[GOAL]
case h
θ : Angle
x✝ : ℝ
⊢ sin θ = sin ↑x✝ ↔ θ = ↑x✝ ∨ θ + ↑x✝ = ↑π
[PROOFSTEP]
exact sin_eq_real_sin_iff_eq_or_add_eq_pi
[GOAL]
⊢ sin 0 = 0
[PROOFSTEP]
rw [← coe_zero, sin_coe, Real.sin_zero]
[GOAL]
⊢ sin ↑π = 0
[PROOFSTEP]
rw [sin_coe, Real.sin_pi]
[GOAL]
θ : Angle
⊢ sin θ = 0 ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
nth_rw 1 [← sin_zero]
[GOAL]
θ : Angle
⊢ sin θ = sin 0 ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
rw [sin_eq_iff_eq_or_add_eq_pi]
[GOAL]
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
simp
[GOAL]
θ : Angle
⊢ sin θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
[PROOFSTEP]
rw [← not_or, ← sin_eq_zero_iff]
[GOAL]
θ : Angle
⊢ sin (-θ) = -sin θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ sin (-↑x✝) = -sin ↑x✝
[PROOFSTEP]
exact Real.sin_neg _
[GOAL]
⊢ Function.Antiperiodic sin ↑π
[PROOFSTEP]
intro θ
[GOAL]
θ : Angle
⊢ sin (θ + ↑π) = -sin θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ sin (↑x✝ + ↑π) = -sin ↑x✝
[PROOFSTEP]
exact Real.sin_antiperiodic _
[GOAL]
⊢ cos 0 = 1
[PROOFSTEP]
rw [← coe_zero, cos_coe, Real.cos_zero]
[GOAL]
⊢ cos ↑π = -1
[PROOFSTEP]
rw [cos_coe, Real.cos_pi]
[GOAL]
θ : Angle
⊢ cos (-θ) = cos θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ cos (-↑x✝) = cos ↑x✝
[PROOFSTEP]
exact Real.cos_neg _
[GOAL]
⊢ Function.Antiperiodic cos ↑π
[PROOFSTEP]
intro θ
[GOAL]
θ : Angle
⊢ cos (θ + ↑π) = -cos θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ cos (↑x✝ + ↑π) = -cos ↑x✝
[PROOFSTEP]
exact Real.cos_antiperiodic _
[GOAL]
θ : Angle
⊢ cos θ = 0 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]
[GOAL]
θ₁ θ₂ : Angle
⊢ sin (θ₁ + θ₂) = sin θ₁ * cos θ₂ + cos θ₁ * sin θ₂
[PROOFSTEP]
induction θ₁ using Real.Angle.induction_on
[GOAL]
case h
θ₂ : Angle
x✝ : ℝ
⊢ sin (↑x✝ + θ₂) = sin ↑x✝ * cos θ₂ + cos ↑x✝ * sin θ₂
[PROOFSTEP]
induction θ₂ using Real.Angle.induction_on
[GOAL]
case h.h
x✝¹ x✝ : ℝ
⊢ sin (↑x✝¹ + ↑x✝) = sin ↑x✝¹ * cos ↑x✝ + cos ↑x✝¹ * sin ↑x✝
[PROOFSTEP]
exact Real.sin_add _ _
[GOAL]
θ₁ θ₂ : Angle
⊢ cos (θ₁ + θ₂) = cos θ₁ * cos θ₂ - sin θ₁ * sin θ₂
[PROOFSTEP]
induction θ₂ using Real.Angle.induction_on
[GOAL]
case h
θ₁ : Angle
x✝ : ℝ
⊢ cos (θ₁ + ↑x✝) = cos θ₁ * cos ↑x✝ - sin θ₁ * sin ↑x✝
[PROOFSTEP]
induction θ₁ using Real.Angle.induction_on
[GOAL]
case h.h
x✝¹ x✝ : ℝ
⊢ cos (↑x✝ + ↑x✝¹) = cos ↑x✝ * cos ↑x✝¹ - sin ↑x✝ * sin ↑x✝¹
[PROOFSTEP]
exact Real.cos_add _ _
[GOAL]
θ : Angle
⊢ cos θ ^ 2 + sin θ ^ 2 = 1
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ cos ↑x✝ ^ 2 + sin ↑x✝ ^ 2 = 1
[PROOFSTEP]
exact Real.cos_sq_add_sin_sq _
[GOAL]
θ : Angle
⊢ sin (θ + ↑(π / 2)) = cos θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ sin (↑x✝ + ↑(π / 2)) = cos ↑x✝
[PROOFSTEP]
exact Real.sin_add_pi_div_two _
[GOAL]
θ : Angle
⊢ sin (θ - ↑(π / 2)) = -cos θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ sin (↑x✝ - ↑(π / 2)) = -cos ↑x✝
[PROOFSTEP]
exact Real.sin_sub_pi_div_two _
[GOAL]
θ : Angle
⊢ sin (↑(π / 2) - θ) = cos θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ sin (↑(π / 2) - ↑x✝) = cos ↑x✝
[PROOFSTEP]
exact Real.sin_pi_div_two_sub _
[GOAL]
θ : Angle
⊢ cos (θ + ↑(π / 2)) = -sin θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ cos (↑x✝ + ↑(π / 2)) = -sin ↑x✝
[PROOFSTEP]
exact Real.cos_add_pi_div_two _
[GOAL]
θ : Angle
⊢ cos (θ - ↑(π / 2)) = sin θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ cos (↑x✝ - ↑(π / 2)) = sin ↑x✝
[PROOFSTEP]
exact Real.cos_sub_pi_div_two _
[GOAL]
θ : Angle
⊢ cos (↑(π / 2) - θ) = sin θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ cos (↑(π / 2) - ↑x✝) = sin ↑x✝
[PROOFSTEP]
exact Real.cos_pi_div_two_sub _
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |sin θ| = |sin ψ|
[PROOFSTEP]
rw [two_nsmul_eq_iff] at h 
[GOAL]
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |sin θ| = |sin ψ|
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inl
θ : Angle
⊢ |sin θ| = |sin θ|
[PROOFSTEP]
rfl
[GOAL]
case inr
ψ : Angle
⊢ |sin (ψ + ↑π)| = |sin ψ|
[PROOFSTEP]
rw [sin_add_pi, abs_neg]
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |sin θ| = |sin ψ|
[PROOFSTEP]
simp_rw [two_zsmul, ← two_nsmul] at h 
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |sin θ| = |sin ψ|
[PROOFSTEP]
exact abs_sin_eq_of_two_nsmul_eq h
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |cos θ| = |cos ψ|
[PROOFSTEP]
rw [two_nsmul_eq_iff] at h 
[GOAL]
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |cos θ| = |cos ψ|
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inl
θ : Angle
⊢ |cos θ| = |cos θ|
[PROOFSTEP]
rfl
[GOAL]
case inr
ψ : Angle
⊢ |cos (ψ + ↑π)| = |cos ψ|
[PROOFSTEP]
rw [cos_add_pi, abs_neg]
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |cos θ| = |cos ψ|
[PROOFSTEP]
simp_rw [two_zsmul, ← two_nsmul] at h 
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |cos θ| = |cos ψ|
[PROOFSTEP]
exact abs_cos_eq_of_two_nsmul_eq h
[GOAL]
θ ψ : ℝ
⊢ ↑(toIcoMod two_pi_pos ψ θ) = ↑θ
[PROOFSTEP]
rw [angle_eq_iff_two_pi_dvd_sub]
[GOAL]
θ ψ : ℝ
⊢ ∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k
[PROOFSTEP]
refine' ⟨-toIcoDiv two_pi_pos ψ θ, _⟩
[GOAL]
θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)
[PROOFSTEP]
rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]
[GOAL]
θ ψ : ℝ
⊢ ↑(toIocMod two_pi_pos ψ θ) = ↑θ
[PROOFSTEP]
rw [angle_eq_iff_two_pi_dvd_sub]
[GOAL]
θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k
[PROOFSTEP]
refine' ⟨-toIocDiv two_pi_pos ψ θ, _⟩
[GOAL]
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
[PROOFSTEP]
rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]
[GOAL]
θ : ℝ
⊢ toReal ↑θ = θ ↔ -π < θ ∧ θ ≤ π
[PROOFSTEP]
rw [toReal_coe, toIocMod_eq_self two_pi_pos]
[GOAL]
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
[PROOFSTEP]
ring_nf
[GOAL]
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
[PROOFSTEP]
rfl
[GOAL]
θ : ℝ
⊢ toReal ↑θ = θ ↔ θ ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [toReal_coe_eq_self_iff, ← Set.mem_Ioc]
[GOAL]
⊢ Function.Injective toReal
[PROOFSTEP]
intro θ ψ h
[GOAL]
θ ψ : Angle
h : toReal θ = toReal ψ
⊢ θ = ψ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
ψ : Angle
x✝ : ℝ
h : toReal ↑x✝ = toReal ψ
⊢ ↑x✝ = ψ
[PROOFSTEP]
induction ψ using Real.Angle.induction_on
[GOAL]
case h.h
x✝¹ x✝ : ℝ
h : toReal ↑x✝¹ = toReal ↑x✝
⊢ ↑x✝¹ = ↑x✝
[PROOFSTEP]
simpa [toReal_coe, toIocMod_eq_toIocMod, zsmul_eq_mul, mul_comm _ (2 * π), ← angle_eq_iff_two_pi_dvd_sub, eq_comm] using
  h
[GOAL]
θ : Angle
⊢ ↑(toReal θ) = θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ ↑(toReal ↑x✝) = ↑x✝
[PROOFSTEP]
exact coe_toIocMod _ _
[GOAL]
θ : Angle
⊢ -π < toReal θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ -π < toReal ↑x✝
[PROOFSTEP]
exact left_lt_toIocMod _ _ _
[GOAL]
θ : Angle
⊢ toReal θ ≤ π
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ toReal ↑x✝ ≤ π
[PROOFSTEP]
convert toIocMod_le_right two_pi_pos _ _
[GOAL]
case h.e'_4
x✝ : ℝ
⊢ π = -π + 2 * π
[PROOFSTEP]
ring
[GOAL]
θ : Angle
⊢ toIocMod two_pi_pos (-π) (toReal θ) = toReal θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toReal ↑x✝) = toReal ↑x✝
[PROOFSTEP]
rw [toReal_coe]
[GOAL]
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
[PROOFSTEP]
exact toIocMod_toIocMod _ _ _ _
[GOAL]
⊢ toReal 0 = 0
[PROOFSTEP]
rw [← coe_zero, toReal_coe_eq_self_iff]
[GOAL]
⊢ -π < 0 ∧ 0 ≤ π
[PROOFSTEP]
exact ⟨Left.neg_neg_iff.2 Real.pi_pos, Real.pi_pos.le⟩
[GOAL]
θ : Angle
⊢ toReal θ = 0 ↔ θ = 0
[PROOFSTEP]
nth_rw 1 [← toReal_zero]
[GOAL]
θ : Angle
⊢ toReal θ = toReal 0 ↔ θ = 0
[PROOFSTEP]
exact toReal_inj
[GOAL]
⊢ toReal ↑π = π
[PROOFSTEP]
rw [toReal_coe_eq_self_iff]
[GOAL]
⊢ -π < π ∧ π ≤ π
[PROOFSTEP]
exact ⟨Left.neg_lt_self Real.pi_pos, le_refl _⟩
[GOAL]
θ : Angle
⊢ toReal θ = π ↔ θ = ↑π
[PROOFSTEP]
rw [← toReal_inj, toReal_pi]
[GOAL]
⊢ ↑π ≠ 0
[PROOFSTEP]
rw [← toReal_injective.ne_iff, toReal_pi, toReal_zero]
[GOAL]
⊢ π ≠ 0
[PROOFSTEP]
exact Real.pi_ne_zero
[GOAL]
⊢ -π < π / 2 ∧ π / 2 ≤ π
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ -π < π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case right
⊢ π / 2 ≤ π
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
θ : Angle
⊢ toReal θ = π / 2 ↔ θ = ↑(π / 2)
[PROOFSTEP]
rw [← toReal_inj, toReal_pi_div_two]
[GOAL]
⊢ -π < -π / 2 ∧ -π / 2 ≤ π
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ -π < -π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case right
⊢ -π / 2 ≤ π
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
θ : Angle
⊢ toReal θ = -π / 2 ↔ θ = ↑(-π / 2)
[PROOFSTEP]
rw [← toReal_inj, toReal_neg_pi_div_two]
[GOAL]
⊢ ↑(π / 2) ≠ 0
[PROOFSTEP]
rw [← toReal_injective.ne_iff, toReal_pi_div_two, toReal_zero]
[GOAL]
⊢ π / 2 ≠ 0
[PROOFSTEP]
exact div_ne_zero Real.pi_ne_zero two_ne_zero
[GOAL]
⊢ ↑(-π / 2) ≠ 0
[PROOFSTEP]
rw [← toReal_injective.ne_iff, toReal_neg_pi_div_two, toReal_zero]
[GOAL]
⊢ -π / 2 ≠ 0
[PROOFSTEP]
exact div_ne_zero (neg_ne_zero.2 Real.pi_ne_zero) two_ne_zero
[GOAL]
θ : ℝ
⊢ |toReal (-↑θ)| = θ ↔ 0 ≤ θ ∧ θ ≤ π
[PROOFSTEP]
refine' ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => _⟩
[GOAL]
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ |toReal (-↑θ)| = θ
[PROOFSTEP]
by_cases hnegpi : θ = π
[GOAL]
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |toReal (-↑θ)| = θ
[PROOFSTEP]
simp [hnegpi, Real.pi_pos.le]
[GOAL]
case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |toReal (-↑θ)| = θ
[PROOFSTEP]
rw [← coe_neg,
  toReal_coe_eq_self_iff.2 ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩, abs_neg,
  abs_eq_self.2 h.1]
[GOAL]
θ : Angle
⊢ |toReal θ| = π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
[PROOFSTEP]
rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff, toReal_eq_neg_pi_div_two_iff]
[GOAL]
n : ℕ
h : n ≠ 0
θ : Angle
⊢ toReal (n • θ) = ↑n * toReal θ ↔ toReal θ ∈ Set.Ioc (-π / ↑n) (π / ↑n)
[PROOFSTEP]
nth_rw 1 [← coe_toReal θ]
[GOAL]
n : ℕ
h : n ≠ 0
θ : Angle
⊢ toReal (n • ↑(toReal θ)) = ↑n * toReal θ ↔ toReal θ ∈ Set.Ioc (-π / ↑n) (π / ↑n)
[PROOFSTEP]
have h' : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero h
[GOAL]
n : ℕ
h : n ≠ 0
θ : Angle
⊢ 0 < ↑n
[PROOFSTEP]
exact_mod_cast Nat.pos_of_ne_zero h
[GOAL]
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ toReal (n • ↑(toReal θ)) = ↑n * toReal θ ↔ toReal θ ∈ Set.Ioc (-π / ↑n) (π / ↑n)
[PROOFSTEP]
rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff' h', le_div_iff' h']
[GOAL]
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ ↔ toReal θ ∈ Set.Ioc (-π / 2) (π / 2)
[PROOFSTEP]
exact_mod_cast nsmul_toReal_eq_mul two_ne_zero
[GOAL]
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ ↔ toReal θ ∈ Set.Ioc (-π / 2) (π / 2)
[PROOFSTEP]
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]
[GOAL]
θ : ℝ
k : ℤ
⊢ toReal ↑θ = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)
[PROOFSTEP]
rw [← sub_zero (θ : Angle), ← zsmul_zero k, ← coe_two_pi, ← coe_zsmul, ← coe_sub, zsmul_eq_mul, ← mul_assoc,
  mul_comm (k : ℝ), toReal_coe_eq_self_iff, Set.mem_Ioc]
[GOAL]
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
[PROOFSTEP]
exact ⟨fun h => ⟨by linarith, by linarith⟩, fun h => ⟨by linarith, by linarith⟩⟩
[GOAL]
θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ (2 * ↑k - 1) * π < θ
[PROOFSTEP]
linarith
[GOAL]
θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ θ ≤ (2 * ↑k + 1) * π
[PROOFSTEP]
linarith
[GOAL]
θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ -π < θ - 2 * ↑k * π
[PROOFSTEP]
linarith
[GOAL]
θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ θ - 2 * ↑k * π ≤ π
[PROOFSTEP]
linarith
[GOAL]
θ : ℝ
⊢ toReal ↑θ = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)
[PROOFSTEP]
convert @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1
[GOAL]
case h.e'_1.h.e'_3.h.e'_6.h.e'_5
θ : ℝ
⊢ 2 = 2 * ↑1
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_2.h.e'_5.h.e'_3
θ : ℝ
⊢ π = (2 * ↑1 - 1) * π
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_2.h.e'_5.h.e'_4.h.e'_5
θ : ℝ
⊢ 3 = 2 * ↑1 + 1
[PROOFSTEP]
norm_num
[GOAL]
θ : ℝ
⊢ toReal ↑θ = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)
[PROOFSTEP]
convert @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2
[GOAL]
case h.e'_1.h.e'_3
θ : ℝ
⊢ θ + 2 * π = θ - 2 * ↑(-1) * π
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_2.h.e'_5
θ : ℝ
⊢ Set.Ioc (-3 * π) (-π) = Set.Ioc ((2 * ↑(-1) - 1) * π) ((2 * ↑(-1) + 1) * π)
[PROOFSTEP]
norm_num
[GOAL]
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ - 2 * π ↔ π / 2 < toReal θ
[PROOFSTEP]
nth_rw 1 [← coe_toReal θ]
[GOAL]
θ : Angle
⊢ toReal (2 • ↑(toReal θ)) = 2 * toReal θ - 2 * π ↔ π / 2 < toReal θ
[PROOFSTEP]
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc]
[GOAL]
θ : Angle
⊢ π < 2 * toReal θ ∧ 2 * toReal θ ≤ 3 * π ↔ π / 2 < toReal θ
[PROOFSTEP]
exact ⟨fun h => by linarith, fun h => ⟨(div_lt_iff' (zero_lt_two' ℝ)).1 h, by linarith [pi_pos, toReal_le_pi θ]⟩⟩
[GOAL]
θ : Angle
h : π < 2 * toReal θ ∧ 2 * toReal θ ≤ 3 * π
⊢ π / 2 < toReal θ
[PROOFSTEP]
linarith
[GOAL]
θ : Angle
h : π / 2 < toReal θ
⊢ 2 * toReal θ ≤ 3 * π
[PROOFSTEP]
linarith [pi_pos, toReal_le_pi θ]
[GOAL]
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ - 2 * π ↔ π / 2 < toReal θ
[PROOFSTEP]
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]
[GOAL]
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ + 2 * π ↔ toReal θ ≤ -π / 2
[PROOFSTEP]
nth_rw 1 [← coe_toReal θ]
[GOAL]
θ : Angle
⊢ toReal (2 • ↑(toReal θ)) = 2 * toReal θ + 2 * π ↔ toReal θ ≤ -π / 2
[PROOFSTEP]
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]
[GOAL]
θ : Angle
⊢ -3 * π < 2 * toReal θ ∧ 2 * toReal θ ≤ -π ↔ toReal θ ≤ -π / 2
[PROOFSTEP]
refine' ⟨fun h => by linarith, fun h => ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff' (zero_lt_two' ℝ)).1 h⟩⟩
[GOAL]
θ : Angle
h : -3 * π < 2 * toReal θ ∧ 2 * toReal θ ≤ -π
⊢ toReal θ ≤ -π / 2
[PROOFSTEP]
linarith
[GOAL]
θ : Angle
h : toReal θ ≤ -π / 2
⊢ -3 * π < 2 * toReal θ
[PROOFSTEP]
linarith [pi_pos, neg_pi_lt_toReal θ]
[GOAL]
θ : Angle
⊢ toReal (2 • θ) = 2 * toReal θ + 2 * π ↔ toReal θ ≤ -π / 2
[PROOFSTEP]
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_add_two_pi]
[GOAL]
θ : Angle
⊢ Real.sin (toReal θ) = sin θ
[PROOFSTEP]
conv_rhs => rw [← coe_toReal θ, sin_coe]
[GOAL]
θ : Angle
| sin θ
[PROOFSTEP]
rw [← coe_toReal θ, sin_coe]
[GOAL]
θ : Angle
| sin θ
[PROOFSTEP]
rw [← coe_toReal θ, sin_coe]
[GOAL]
θ : Angle
| sin θ
[PROOFSTEP]
rw [← coe_toReal θ, sin_coe]
[GOAL]
θ : Angle
⊢ Real.cos (toReal θ) = cos θ
[PROOFSTEP]
conv_rhs => rw [← coe_toReal θ, cos_coe]
[GOAL]
θ : Angle
| cos θ
[PROOFSTEP]
rw [← coe_toReal θ, cos_coe]
[GOAL]
θ : Angle
| cos θ
[PROOFSTEP]
rw [← coe_toReal θ, cos_coe]
[GOAL]
θ : Angle
| cos θ
[PROOFSTEP]
rw [← coe_toReal θ, cos_coe]
[GOAL]
θ : Angle
⊢ 0 ≤ cos θ ↔ |toReal θ| ≤ π / 2
[PROOFSTEP]
nth_rw 1 [← coe_toReal θ]
[GOAL]
θ : Angle
⊢ 0 ≤ cos ↑(toReal θ) ↔ |toReal θ| ≤ π / 2
[PROOFSTEP]
rw [abs_le, cos_coe]
[GOAL]
θ : Angle
⊢ 0 ≤ Real.cos (toReal θ) ↔ -(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2
[PROOFSTEP]
refine' ⟨fun h => _, cos_nonneg_of_mem_Icc⟩
[GOAL]
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
⊢ -(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2
[PROOFSTEP]
by_contra hn
[GOAL]
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : ¬(-(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2)
⊢ False
[PROOFSTEP]
rw [not_and_or, not_le, not_le] at hn 
[GOAL]
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2) ∨ π / 2 < toReal θ
⊢ False
[PROOFSTEP]
refine' (not_lt.2 h) _
[GOAL]
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2) ∨ π / 2 < toReal θ
⊢ Real.cos (toReal θ) < 0
[PROOFSTEP]
rcases hn with (hn | hn)
[GOAL]
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ Real.cos (toReal θ) < 0
[PROOFSTEP]
rw [← Real.cos_neg]
[GOAL]
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ Real.cos (-toReal θ) < 0
[PROOFSTEP]
refine' cos_neg_of_pi_div_two_lt_of_lt (by linarith) _
[GOAL]
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ π / 2 < -toReal θ
[PROOFSTEP]
linarith
[GOAL]
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ -toReal θ < π + π / 2
[PROOFSTEP]
linarith [neg_pi_lt_toReal θ]
[GOAL]
case inr
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : π / 2 < toReal θ
⊢ Real.cos (toReal θ) < 0
[PROOFSTEP]
refine' cos_neg_of_pi_div_two_lt_of_lt hn _
[GOAL]
case inr
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : π / 2 < toReal θ
⊢ toReal θ < π + π / 2
[PROOFSTEP]
linarith [toReal_le_pi θ]
[GOAL]
θ : Angle
⊢ 0 < cos θ ↔ |toReal θ| < π / 2
[PROOFSTEP]
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, cos_nonneg_iff_abs_toReal_le_pi_div_two, ← and_congr_right]
[GOAL]
θ : Angle
⊢ |toReal θ| ≤ π / 2 → (|toReal θ| ≠ π / 2 ↔ 0 ≠ cos θ)
[PROOFSTEP]
rintro -
[GOAL]
θ : Angle
⊢ |toReal θ| ≠ π / 2 ↔ 0 ≠ cos θ
[PROOFSTEP]
rw [Ne.def, Ne.def, not_iff_not, @eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]
[GOAL]
θ : Angle
⊢ cos θ < 0 ↔ π / 2 < |toReal θ|
[PROOFSTEP]
rw [← not_le, ← not_le, not_iff_not, cos_nonneg_iff_abs_toReal_le_pi_div_two]
[GOAL]
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |cos θ| = |sin ψ|
[PROOFSTEP]
rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h 
[GOAL]
θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |cos θ| = |sin ψ|
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inl
ψ : Angle
⊢ |cos (↑(π / 2) - ψ)| = |sin ψ|
[PROOFSTEP]
simp [cos_pi_div_two_sub]
[GOAL]
case inr
ψ : Angle
⊢ |cos (↑(π / 2) - ψ + ↑π)| = |sin ψ|
[PROOFSTEP]
simp [cos_pi_div_two_sub]
[GOAL]
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |cos θ| = |sin ψ|
[PROOFSTEP]
simp_rw [two_zsmul, ← two_nsmul] at h 
[GOAL]
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |cos θ| = |sin ψ|
[PROOFSTEP]
exact abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h
[GOAL]
x : ℝ
⊢ tan ↑x = Real.tan x
[PROOFSTEP]
rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]
[GOAL]
⊢ tan 0 = 0
[PROOFSTEP]
rw [← coe_zero, tan_coe, Real.tan_zero]
[GOAL]
⊢ tan ↑π = 0
[PROOFSTEP]
rw [tan_coe, Real.tan_pi]
[GOAL]
⊢ Function.Periodic tan ↑π
[PROOFSTEP]
intro θ
[GOAL]
θ : Angle
⊢ tan (θ + ↑π) = tan θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ tan (↑x✝ + ↑π) = tan ↑x✝
[PROOFSTEP]
rw [← coe_add, tan_coe, tan_coe]
[GOAL]
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝
[PROOFSTEP]
exact Real.tan_periodic _
[GOAL]
θ : Angle
⊢ Real.tan (toReal θ) = tan θ
[PROOFSTEP]
conv_rhs => rw [← coe_toReal θ, tan_coe]
[GOAL]
θ : Angle
| tan θ
[PROOFSTEP]
rw [← coe_toReal θ, tan_coe]
[GOAL]
θ : Angle
| tan θ
[PROOFSTEP]
rw [← coe_toReal θ, tan_coe]
[GOAL]
θ : Angle
| tan θ
[PROOFSTEP]
rw [← coe_toReal θ, tan_coe]
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ tan θ = tan ψ
[PROOFSTEP]
rw [two_nsmul_eq_iff] at h 
[GOAL]
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ tan θ = tan ψ
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inl
θ : Angle
⊢ tan θ = tan θ
[PROOFSTEP]
rfl
[GOAL]
case inr
ψ : Angle
⊢ tan (ψ + ↑π) = tan ψ
[PROOFSTEP]
exact tan_add_pi _
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ tan θ = tan ψ
[PROOFSTEP]
simp_rw [two_zsmul, ← two_nsmul] at h 
[GOAL]
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ tan θ = tan ψ
[PROOFSTEP]
exact tan_eq_of_two_nsmul_eq h
[GOAL]
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ tan ψ = (tan θ)⁻¹
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
ψ : Angle
x✝ : ℝ
h : 2 • ↑x✝ + 2 • ψ = ↑π
⊢ tan ψ = (tan ↑x✝)⁻¹
[PROOFSTEP]
induction ψ using Real.Angle.induction_on
[GOAL]
case h.h
x✝¹ x✝ : ℝ
h : 2 • ↑x✝¹ + 2 • ↑x✝ = ↑π
⊢ tan ↑x✝ = (tan ↑x✝¹)⁻¹
[PROOFSTEP]
rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h 
[GOAL]
case h.h
x✝¹ x✝ : ℝ
h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ tan ↑x✝ = (tan ↑x✝¹)⁻¹
[PROOFSTEP]
rcases h with ⟨k, h⟩
[GOAL]
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ tan ↑x✝ = (tan ↑x✝¹)⁻¹
[PROOFSTEP]
rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add, mul_right_inj' (two_ne_zero' ℝ), ←
  eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π, inv_mul_eq_div, mul_comm] at h 
[GOAL]
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ tan ↑x✝ = (tan ↑x✝¹)⁻¹
[PROOFSTEP]
rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]
[GOAL]
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan (π / 2 - x✝¹ + ↑k * π) = Real.tan (π / 2 - x✝¹)
[PROOFSTEP]
exact Real.tan_periodic.int_mul _ _
[GOAL]
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ tan ψ = (tan θ)⁻¹
[PROOFSTEP]
simp_rw [two_zsmul, ← two_nsmul] at h 
[GOAL]
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ tan ψ = (tan θ)⁻¹
[PROOFSTEP]
exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h
[GOAL]
⊢ sign 0 = 0
[PROOFSTEP]
rw [sign, sin_zero, _root_.sign_zero]
[GOAL]
⊢ sign ↑π = 0
[PROOFSTEP]
rw [sign, sin_coe_pi, _root_.sign_zero]
[GOAL]
θ : Angle
⊢ sign (-θ) = -sign θ
[PROOFSTEP]
simp_rw [sign, sin_neg, Left.sign_neg]
[GOAL]
θ : Angle
⊢ sign (θ + ↑π) = -sign θ
[PROOFSTEP]
rw [sign, sign, sin_add_pi, Left.sign_neg]
[GOAL]
θ : Angle
⊢ sign (↑π + θ) = -sign θ
[PROOFSTEP]
rw [add_comm, sign_add_pi]
[GOAL]
θ : Angle
⊢ sign (↑π - θ) = sign θ
[PROOFSTEP]
simp [sign_antiperiodic.sub_eq']
[GOAL]
θ : Angle
⊢ sign θ = 0 ↔ θ = 0 ∨ θ = ↑π
[PROOFSTEP]
rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]
[GOAL]
θ : Angle
⊢ sign θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
[PROOFSTEP]
rw [← not_or, ← sign_eq_zero_iff]
[GOAL]
θ : Angle
⊢ toReal θ < 0 ↔ sign θ = -1
[PROOFSTEP]
rw [sign, ← sin_toReal, sign_eq_neg_one_iff]
[GOAL]
θ : Angle
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
[PROOFSTEP]
rcases lt_trichotomy θ.toReal 0 with (h | h | h)
[GOAL]
case inl
θ : Angle
h : toReal θ < 0
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
[PROOFSTEP]
exact ⟨fun _ => Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_toReal θ), fun _ => h⟩
[GOAL]
case inr.inl
θ : Angle
h : toReal θ = 0
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr.inr
θ : Angle
h : 0 < toReal θ
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
[PROOFSTEP]
exact
  ⟨fun hn => False.elim (h.asymm hn), fun hn =>
    False.elim (hn.not_le (sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)))⟩
[GOAL]
θ : Angle
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
[PROOFSTEP]
rcases lt_trichotomy θ.toReal 0 with (h | h | h)
[GOAL]
case inl
θ : Angle
h : toReal θ < 0
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
[PROOFSTEP]
refine' ⟨fun hn => False.elim (h.not_le hn), fun hn => _⟩
[GOAL]
case inl
θ : Angle
h : toReal θ < 0
hn : 0 ≤ sign θ
⊢ 0 ≤ toReal θ
[PROOFSTEP]
rw [toReal_neg_iff_sign_neg.1 h] at hn 
[GOAL]
case inl
θ : Angle
h : toReal θ < 0
hn : 0 ≤ -1
⊢ 0 ≤ toReal θ
[PROOFSTEP]
exact False.elim (hn.not_lt (by decide))
[GOAL]
θ : Angle
h : toReal θ < 0
hn : 0 ≤ -1
⊢ -1 < 0
[PROOFSTEP]
decide
[GOAL]
case inr.inl
θ : Angle
h : toReal θ = 0
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
[PROOFSTEP]
simp [h, sign, ← sin_toReal]
[GOAL]
case inr.inr
θ : Angle
h : 0 < toReal θ
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
[PROOFSTEP]
refine' ⟨fun _ => _, fun _ => h.le⟩
[GOAL]
case inr.inr
θ : Angle
h : 0 < toReal θ
x✝ : 0 ≤ toReal θ
⊢ 0 ≤ sign θ
[PROOFSTEP]
rw [sign, ← sin_toReal, sign_nonneg_iff]
[GOAL]
case inr.inr
θ : Angle
h : 0 < toReal θ
x✝ : 0 ≤ toReal θ
⊢ 0 ≤ Real.sin (toReal θ)
[PROOFSTEP]
exact sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)
[GOAL]
θ : Angle
h : θ ≠ ↑π
⊢ ↑SignType.sign (toReal θ) = sign θ
[PROOFSTEP]
rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
[GOAL]
case inl
θ : Angle
h : θ ≠ ↑π
ht : toReal θ < 0
⊢ ↑SignType.sign (toReal θ) = sign θ
[PROOFSTEP]
simp [ht, toReal_neg_iff_sign_neg.1 ht]
[GOAL]
case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : toReal θ = 0
⊢ ↑SignType.sign (toReal θ) = sign θ
[PROOFSTEP]
simp [sign, ht, ← sin_toReal]
[GOAL]
case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < toReal θ
⊢ ↑SignType.sign (toReal θ) = sign θ
[PROOFSTEP]
rw [sign, ← sin_toReal, sign_pos ht,
  sign_pos (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]
[GOAL]
θ : Angle
h : 0 ≤ sign θ
⊢ ↑|toReal θ| = θ
[PROOFSTEP]
rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]
[GOAL]
θ : Angle
h : sign θ ≤ 0
⊢ -↑|toReal θ| = θ
[PROOFSTEP]
rw [SignType.nonpos_iff] at h 
[GOAL]
θ : Angle
h : sign θ = -1 ∨ sign θ = 0
⊢ -↑|toReal θ| = θ
[PROOFSTEP]
rcases h with (h | h)
[GOAL]
case inl
θ : Angle
h : sign θ = -1
⊢ -↑|toReal θ| = θ
[PROOFSTEP]
rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
[GOAL]
case inr
θ : Angle
h : sign θ = 0
⊢ -↑|toReal θ| = θ
[PROOFSTEP]
rw [sign_eq_zero_iff] at h 
[GOAL]
case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑|toReal θ| = θ
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case inr.inl
⊢ -↑|toReal 0| = 0
[PROOFSTEP]
simp [abs_of_pos Real.pi_pos]
[GOAL]
case inr.inr
⊢ -↑|toReal ↑π| = ↑π
[PROOFSTEP]
simp [abs_of_pos Real.pi_pos]
[GOAL]
θ ψ : Angle
⊢ θ = ψ ↔ sign θ = sign ψ ∧ |toReal θ| = |toReal ψ|
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case refine'_1
θ ψ : Angle
⊢ θ = ψ → sign θ = sign ψ ∧ |toReal θ| = |toReal ψ|
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
θ : Angle
⊢ sign θ = sign θ ∧ |toReal θ| = |toReal θ|
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
case refine'_2
θ ψ : Angle
h : sign θ = sign ψ ∧ |toReal θ| = |toReal ψ|
⊢ θ = ψ
[PROOFSTEP]
rcases h with ⟨hs, hr⟩
[GOAL]
case refine'_2.intro
θ ψ : Angle
hs : sign θ = sign ψ
hr : |toReal θ| = |toReal ψ|
⊢ θ = ψ
[PROOFSTEP]
rw [abs_eq_abs] at hr 
[GOAL]
case refine'_2.intro
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = toReal ψ ∨ toReal θ = -toReal ψ
⊢ θ = ψ
[PROOFSTEP]
rcases hr with (hr | hr)
[GOAL]
case refine'_2.intro.inl
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = toReal ψ
⊢ θ = ψ
[PROOFSTEP]
exact toReal_injective hr
[GOAL]
case refine'_2.intro.inr
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = -toReal ψ
⊢ θ = ψ
[PROOFSTEP]
by_cases h : θ = π
[GOAL]
case pos
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = -toReal ψ
h : θ = ↑π
⊢ θ = ψ
[PROOFSTEP]
rw [h, toReal_pi, ← neg_eq_iff_eq_neg] at hr 
[GOAL]
case pos
θ ψ : Angle
hs : sign θ = sign ψ
hr : -π = toReal ψ
h : θ = ↑π
⊢ θ = ψ
[PROOFSTEP]
exact False.elim ((neg_pi_lt_toReal ψ).ne hr)
[GOAL]
case neg
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = -toReal ψ
h : ¬θ = ↑π
⊢ θ = ψ
[PROOFSTEP]
by_cases h' : ψ = π
[GOAL]
case pos
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = -toReal ψ
h : ¬θ = ↑π
h' : ψ = ↑π
⊢ θ = ψ
[PROOFSTEP]
rw [h', toReal_pi] at hr 
[GOAL]
case pos
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = -π
h : ¬θ = ↑π
h' : ψ = ↑π
⊢ θ = ψ
[PROOFSTEP]
exact False.elim ((neg_pi_lt_toReal θ).ne hr.symm)
[GOAL]
case neg
θ ψ : Angle
hs : sign θ = sign ψ
hr : toReal θ = -toReal ψ
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ
[PROOFSTEP]
rw [← sign_toReal h, ← sign_toReal h', hr, Left.sign_neg, SignType.neg_eq_self_iff, _root_.sign_eq_zero_iff,
  toReal_eq_zero_iff] at hs 
[GOAL]
case neg
θ ψ : Angle
hs : ψ = 0
hr : toReal θ = -toReal ψ
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ
[PROOFSTEP]
rw [hs, toReal_zero, neg_zero, toReal_eq_zero_iff] at hr 
[GOAL]
case neg
θ ψ : Angle
hs : ψ = 0
hr : θ = 0
h : ¬θ = ↑π
h' : ¬ψ = ↑π
⊢ θ = ψ
[PROOFSTEP]
rw [hr, hs]
[GOAL]
θ ψ : Angle
h : sign θ = sign ψ
⊢ θ = ψ ↔ |toReal θ| = |toReal ψ|
[PROOFSTEP]
simpa [h] using @eq_iff_sign_eq_and_abs_toReal_eq θ ψ
[GOAL]
⊢ sign ↑(π / 2) = 1
[PROOFSTEP]
rw [sign, sin_coe, sin_pi_div_two, sign_one]
[GOAL]
⊢ sign ↑(-π / 2) = -1
[PROOFSTEP]
rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
[GOAL]
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sign ↑θ
[PROOFSTEP]
rw [sign, sign_nonneg_iff]
[GOAL]
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sin ↑θ
[PROOFSTEP]
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi
[GOAL]
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ sign (-↑θ) ≤ 0
[PROOFSTEP]
rw [sign, sign_nonpos_iff, sin_neg, Left.neg_nonpos_iff]
[GOAL]
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ sin ↑θ
[PROOFSTEP]
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi
[GOAL]
θ : Angle
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ |toReal θ| < π / 2
[PROOFSTEP]
by_cases hpi : θ = π
[GOAL]
case pos
θ : Angle
hpi : θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ |toReal θ| < π / 2
[PROOFSTEP]
simp [hpi]
[GOAL]
case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ |toReal θ| < π / 2
[PROOFSTEP]
rw [or_iff_right hpi]
[GOAL]
case neg
θ : Angle
hpi : ¬θ = ↑π
⊢ sign (2 • θ) = sign θ ↔ |toReal θ| < π / 2
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
⊢ |toReal θ| < π / 2
[PROOFSTEP]
by_contra hle
[GOAL]
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : ¬|toReal θ| < π / 2
⊢ False
[PROOFSTEP]
rw [not_lt, le_abs, le_neg] at hle 
[GOAL]
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
⊢ False
[PROOFSTEP]
have hpi' : θ.toReal ≠ π := by simpa using hpi
[GOAL]
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
⊢ toReal θ ≠ π
[PROOFSTEP]
simpa using hpi
[GOAL]
case neg.refine'_1
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hle : π / 2 ≤ toReal θ ∨ toReal θ ≤ -(π / 2)
hpi' : toReal θ ≠ π
⊢ False
[PROOFSTEP]
rcases hle with (hle | hle)
[GOAL]
case neg.refine'_1.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
⊢ False
[PROOFSTEP]
rcases hle.eq_or_lt with (heq | hlt)
[GOAL]
case neg.refine'_1.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
⊢ False
[PROOFSTEP]
rcases hle.eq_or_lt with (heq | hlt)
[GOAL]
case neg.refine'_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
heq : π / 2 = toReal θ
⊢ False
[PROOFSTEP]
rw [← coe_toReal θ, ← heq] at h 
[GOAL]
case neg.refine'_1.inl.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • ↑(π / 2)) = sign ↑(π / 2)
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
heq : π / 2 = toReal θ
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ False
[PROOFSTEP]
rw [← sign_toReal hpi, sign_pos (pi_div_two_pos.trans hlt), ← sign_toReal, two_nsmul_toReal_eq_two_mul_sub_two_pi.2 hlt,
  _root_.sign_neg] at h 
[GOAL]
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : -1 = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (2 * toReal θ - 2 * π) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ 2 * toReal θ - 2 * π < 0
[PROOFSTEP]
rw [← mul_sub]
[GOAL]
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (2 * toReal θ - 2 * π) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ 2 * (toReal θ - π) < 0
[PROOFSTEP]
exact mul_neg_of_pos_of_neg two_pos (sub_neg.2 ((toReal_le_pi _).lt_of_ne hpi'))
[GOAL]
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
⊢ 2 • θ ≠ ↑π
[PROOFSTEP]
intro he
[GOAL]
case neg.refine'_1.inl.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = 1
hpi' : toReal θ ≠ π
hle : π / 2 ≤ toReal θ
hlt : π / 2 < toReal θ
he : 2 • θ = ↑π
⊢ False
[PROOFSTEP]
simp [he] at h 
[GOAL]
case neg.refine'_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
heq : toReal θ = -(π / 2)
⊢ False
[PROOFSTEP]
rw [← coe_toReal θ, heq] at h 
[GOAL]
case neg.refine'_1.inr.inl
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • ↑(-(π / 2))) = sign ↑(-(π / 2))
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
heq : toReal θ = -(π / 2)
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = sign θ
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False
[PROOFSTEP]
rw [← sign_toReal hpi, _root_.sign_neg (hlt.trans (Left.neg_neg_iff.2 pi_div_two_pos)), ← sign_toReal] at h 
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ 2 • θ ≠ ↑π
[PROOFSTEP]
swap
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ 2 • θ ≠ ↑π
[PROOFSTEP]
intro he
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : sign (2 • θ) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
he : 2 • θ = ↑π
⊢ False
[PROOFSTEP]
simp [he] at h 
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -(π / 2)
⊢ False
[PROOFSTEP]
rw [← neg_div] at hlt 
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (toReal (2 • θ)) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -π / 2
⊢ False
[PROOFSTEP]
rw [two_nsmul_toReal_eq_two_mul_add_two_pi.2 hlt.le, sign_pos] at h 
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : 1 = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -π / 2
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case neg.refine'_1.inr.inr
θ : Angle
hpi : ¬θ = ↑π
h : ↑SignType.sign (2 * toReal θ + 2 * π) = -1
hpi' : toReal θ ≠ π
hle : toReal θ ≤ -(π / 2)
hlt : toReal θ < -π / 2
⊢ 0 < 2 * toReal θ + 2 * π
[PROOFSTEP]
linarith [neg_pi_lt_toReal θ]
[GOAL]
case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : |toReal θ| < π / 2
⊢ sign (2 • θ) = sign θ
[PROOFSTEP]
have hpi' : (2 : ℕ) • θ ≠ π := by
  rw [Ne.def, two_nsmul_eq_pi_iff, not_or]
  constructor
  · rintro rfl
    simp [pi_pos, div_pos, abs_of_pos] at h 
  · rintro rfl
    rw [toReal_neg_pi_div_two] at h 
    simp [pi_pos, div_pos, neg_div, abs_of_pos] at h 
[GOAL]
θ : Angle
hpi : ¬θ = ↑π
h : |toReal θ| < π / 2
⊢ 2 • θ ≠ ↑π
[PROOFSTEP]
rw [Ne.def, two_nsmul_eq_pi_iff, not_or]
[GOAL]
θ : Angle
hpi : ¬θ = ↑π
h : |toReal θ| < π / 2
⊢ ¬θ = ↑(π / 2) ∧ ¬θ = ↑(-π / 2)
[PROOFSTEP]
constructor
[GOAL]
case left
θ : Angle
hpi : ¬θ = ↑π
h : |toReal θ| < π / 2
⊢ ¬θ = ↑(π / 2)
[PROOFSTEP]
rintro rfl
[GOAL]
case left
hpi : ¬↑(π / 2) = ↑π
h : |toReal ↑(π / 2)| < π / 2
⊢ False
[PROOFSTEP]
simp [pi_pos, div_pos, abs_of_pos] at h 
[GOAL]
case right
θ : Angle
hpi : ¬θ = ↑π
h : |toReal θ| < π / 2
⊢ ¬θ = ↑(-π / 2)
[PROOFSTEP]
rintro rfl
[GOAL]
case right
hpi : ¬↑(-π / 2) = ↑π
h : |toReal ↑(-π / 2)| < π / 2
⊢ False
[PROOFSTEP]
rw [toReal_neg_pi_div_two] at h 
[GOAL]
case right
hpi : ¬↑(-π / 2) = ↑π
h : |-π / 2| < π / 2
⊢ False
[PROOFSTEP]
simp [pi_pos, div_pos, neg_div, abs_of_pos] at h 
[GOAL]
case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : |toReal θ| < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ sign (2 • θ) = sign θ
[PROOFSTEP]
rw [abs_lt, ← neg_div] at h 
[GOAL]
case neg.refine'_2
θ : Angle
hpi : ¬θ = ↑π
h : -π / 2 < toReal θ ∧ toReal θ < π / 2
hpi' : 2 • θ ≠ ↑π
⊢ sign (2 • θ) = sign θ
[PROOFSTEP]
rw [← sign_toReal hpi, ← sign_toReal hpi', two_nsmul_toReal_eq_two_mul.2 ⟨h.1, h.2.le⟩, sign_mul,
  sign_pos (zero_lt_two' ℝ), one_mul]
[GOAL]
θ : Angle
⊢ sign (2 • θ) = sign θ ↔ θ = ↑π ∨ |toReal θ| < π / 2
[PROOFSTEP]
rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑π
⊢ ContinuousOn (sign ∘ f) s
[PROOFSTEP]
refine' (ContinuousAt.continuousOn fun θ hθ => _).comp hf (Set.mapsTo_image f s)
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑π
θ : Angle
hθ : θ ∈ f '' s
⊢ ContinuousAt sign θ
[PROOFSTEP]
obtain ⟨z, hz, rfl⟩ := hθ
[GOAL]
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑π
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)
[PROOFSTEP]
exact continuousAt_sign (hs _ hz).1 (hs _ hz).2
