[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


[GOAL]
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
have : HasStrictDerivAt log (exp <| log x)⁻¹ x :=
  (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne') (ne_of_gt <| exp_pos _) <|
    Eventually.mono (lt_mem_nhds hx) @exp_log
[GOAL]
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (exp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
rwa [exp_log hx] at this
[GOAL]
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
cases' hx.lt_or_lt with hx hx
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
convert (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1
[GOAL]
case h.e'_6
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg
[PROOFSTEP]
ext y
[GOAL]
case h.e'_6.h
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y
[PROOFSTEP]
exact (log_neg_eq_log y).symm
[GOAL]
case h.e'_7
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1
[PROOFSTEP]
field_simp [hx.ne]
[GOAL]
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
[PROOFSTEP]
exact hasStrictDerivAt_log_of_pos hx
[GOAL]
x✝ x : ℝ
hx : x = 0
⊢ deriv log x = x⁻¹
[PROOFSTEP]
rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
[GOAL]
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ n log {0}ᶜ
[PROOFSTEP]
suffices : ContDiffOn ℝ ⊤ log {0}ᶜ
[GOAL]
x : ℝ
n : ℕ∞
this : ContDiffOn ℝ ⊤ log {0}ᶜ
⊢ ContDiffOn ℝ n log {0}ᶜ
case this x : ℝ n : ℕ∞ ⊢ ContDiffOn ℝ ⊤ log {0}ᶜ
[PROOFSTEP]
exact this.of_le le_top
[GOAL]
case this
x : ℝ
n : ℕ∞
⊢ ContDiffOn ℝ ⊤ log {0}ᶜ
[PROOFSTEP]
refine' (contDiffOn_top_iff_deriv_of_open isOpen_compl_singleton).2 _
[GOAL]
case this
x : ℝ
n : ℕ∞
⊢ DifferentiableOn ℝ log {0}ᶜ ∧ ContDiffOn ℝ ⊤ (deriv log) {0}ᶜ
[PROOFSTEP]
simp [differentiableOn_log, contDiffOn_inv]
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) s x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') s x
[PROOFSTEP]
exact (hasDerivAt_log hx).comp_hasDerivWithinAt x hf
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y => Real.log (f y)) (f' / f x) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x
[PROOFSTEP]
exact hf.log hx
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x
[PROOFSTEP]
exact (hasStrictDerivAt_log hx).comp x hf
[GOAL]
t : ℝ
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
[PROOFSTEP]
have h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t) := by
  simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
    (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)
[GOAL]
t : ℝ
⊢ Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
[PROOFSTEP]
simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
  (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)
[GOAL]
t : ℝ
⊢ 1 + t * id 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
[PROOFSTEP]
have h₂ : Tendsto (fun x : ℝ => x⁻¹) atTop (𝓝[≠] 0) :=
  tendsto_inv_atTop_zero'.mono_right (nhdsWithin_mono _ fun x hx => (Set.mem_Ioi.mp hx).ne')
[GOAL]
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
h₂ : Tendsto (fun x => x⁻¹) atTop (𝓝[{0}ᶜ] 0)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
[PROOFSTEP]
simpa only [(· ∘ ·), inv_inv] using h₁.comp h₂
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
let F : ℝ → ℝ := fun x => (∑ i in range n, x ^ (i + 1) / (i + 1)) + log (1 - x)
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
let F' : ℝ → ℝ := fun x ↦
  -x ^ n /
    (1 - x)
      -- Porting note: In `mathlib3`, the proof used `deriv`/`DifferentiableAt`. `simp` failed to
        -- compute `deriv`, so I changed the proof to use `HasDerivAt` instead
        -- First step: compute the derivative of `F`
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
have A : ∀ y ∈ Ioo (-1 : ℝ) 1, HasDerivAt F (F' y) y := fun y hy ↦
  by
  have : HasDerivAt F ((∑ i in range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
    .add (.sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
      (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
  convert this using 1
  calc
    -y ^ n / (1 - y) = ∑ i in Finset.range n, y ^ i + -1 / (1 - y) :=
      by
      field_simp [geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
      ring
    _ = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) :=
      by
      congr with i
      rw [Nat.cast_succ, mul_div_cancel_left _ (Nat.cast_add_one_pos i).ne']
        -- second step: show that the derivative of `F` is small
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
⊢ HasDerivAt F (F' y) y
[PROOFSTEP]
have : HasDerivAt F ((∑ i in range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
  .add (.sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
    (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ HasDerivAt F (F' y) y
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_7
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ F' y = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)
[PROOFSTEP]
calc
  -y ^ n / (1 - y) = ∑ i in Finset.range n, y ^ i + -1 / (1 - y) :=
    by
    field_simp [geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
    ring
  _ = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) :=
    by
    congr with i
    rw [Nat.cast_succ, mul_div_cancel_left _ (Nat.cast_add_one_pos i).ne']
      -- second step: show that the derivative of `F` is small
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ -y ^ n / (1 - y) = ∑ i in Finset.range n, y ^ i + -1 / (1 - y)
[PROOFSTEP]
field_simp [geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ -(y ^ n * ((y - 1) * (1 - y))) = ((y ^ n - 1) * (1 - y) + (1 - y)) * (1 - y)
[PROOFSTEP]
ring
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ ∑ i in Finset.range n, y ^ i + -1 / (1 - y) = ∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)
[PROOFSTEP]
congr with i
[GOAL]
case e_a.e_f.h
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i in Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
i : ℕ
⊢ y ^ i = ↑(i + 1) * y ^ i / (↑i + 1)
[PROOFSTEP]
rw [Nat.cast_succ, mul_div_cancel_left _ (Nat.cast_add_one_pos i).ne']
  -- second step: show that the derivative of `F` is small
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
have B : ∀ y ∈ Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|) := fun y hy ↦
  calc
    |F' y| = |y| ^ n / |1 - y| := by simp [abs_div]
    _ ≤ |x| ^ n / (1 - |x|) := by
      have : |y| ≤ |x| := abs_le.2 hy
      have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
      gcongr
      exact sub_pos.2 h
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ |F' y| = |y| ^ n / |1 - y|
[PROOFSTEP]
simp [abs_div]
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
[PROOFSTEP]
have : |y| ≤ |x| := abs_le.2 hy
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : |y| ≤ |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
[PROOFSTEP]
have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : |y| ≤ |x|
⊢ 1 - |x| ≤ 1 - y
[PROOFSTEP]
linarith [hy.2]
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this✝ : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
[PROOFSTEP]
gcongr
[GOAL]
case hd
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this✝ : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
⊢ 0 < 1 - |x|
[PROOFSTEP]
exact sub_pos.2 h
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ :=
  by
  refine
    Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
  · exact Icc_subset_Ioo (neg_lt_neg h) h hy
  · simp
  ·
    simp [le_abs_self x, neg_le.mp (neg_le_abs_self x)]
      -- fourth step: conclude by massaging the inequality of the third step
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
[PROOFSTEP]
refine
  Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
[GOAL]
case refine_1
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ y ∈ Set.Ioo (-1) 1
[PROOFSTEP]
exact Icc_subset_Ioo (neg_lt_neg h) h hy
[GOAL]
case refine_2
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ 0 ∈ Set.Icc (-|x|) |x|
[PROOFSTEP]
simp
[GOAL]
case refine_3
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ x ∈ Set.Icc (-|x|) |x|
[PROOFSTEP]
simp [le_abs_self x, neg_le.mp (neg_le_abs_self x)]
  -- fourth step: conclude by massaging the inequality of the third step
[GOAL]
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)
A : ∀ (y : ℝ), y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y
B : ∀ (y : ℝ), y ∈ Set.Icc (-|x|) |x| → |F' y| ≤ |x| ^ n / (1 - |x|)
C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
⊢ |∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
[PROOFSTEP]
simpa [div_mul_eq_mul_div, pow_succ'] using C
[GOAL]
x : ℝ
h : |x| < 1
⊢ HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-log (1 - x))
[PROOFSTEP]
rw [Summable.hasSum_iff_tendsto_nat]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))
x : ℝ h : |x| < 1 ⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
show Tendsto (fun n : ℕ => ∑ i : ℕ in range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x)))
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))
[PROOFSTEP]
rw [tendsto_iff_norm_tendsto_zero]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => ‖∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)
[PROOFSTEP]
simp only [norm_eq_abs, sub_neg_eq_add]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => |∑ i in Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x)|) atTop (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) _
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
[PROOFSTEP]
suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by simpa
[GOAL]
x : ℝ
h : |x| < 1
this : Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
[PROOFSTEP]
simpa
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
[PROOFSTEP]
simp only [pow_succ]
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
[PROOFSTEP]
refine' (tendsto_const_nhds.mul _).div_const _
[GOAL]
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ t) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_pow_atTop_nhds_0_of_lt_1 (abs_nonneg _) h
[GOAL]
x : ℝ
h : |x| < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
show Summable fun n : ℕ => x ^ (n + 1) / (n + 1)
[GOAL]
x : ℝ
h : |x| < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
refine' summable_of_norm_bounded _ (summable_geometric_of_lt_1 (abs_nonneg _) h) fun i => _
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ |x| ^ i
[PROOFSTEP]
calc
  ‖x ^ (i + 1) / (i + 1)‖ = |x| ^ (i + 1) / (i + 1) :=
    by
    have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
    rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
  _ ≤ |x| ^ (i + 1) / (0 + 1) := by
    gcongr
    exact i.cast_nonneg
  _ ≤ |x| ^ i := by simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)
[PROOFSTEP]
have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)
[PROOFSTEP]
rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (↑i + 1) ≤ |x| ^ (i + 1) / (0 + 1)
[PROOFSTEP]
gcongr
[GOAL]
case h.bc
x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ ↑i
[PROOFSTEP]
exact i.cast_nonneg
[GOAL]
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (0 + 1) ≤ |x| ^ i
[PROOFSTEP]
simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)
[GOAL]
x : ℝ
h : |x| < 1
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
[PROOFSTEP]
set term := fun n : ℕ => -1 * ((-x) ^ (n + 1) / ((n : ℝ) + 1)) + x ^ (n + 1) / (n + 1)
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
[PROOFSTEP]
have h_term_eq_goal : term ∘ (· * ·) 2 = fun k : ℕ => 2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1) :=
  by
  ext n
  dsimp only [(· ∘ ·)]
  rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
  push_cast
  ring_nf
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
⊢ term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
[PROOFSTEP]
ext n
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ (term ∘ (fun x x_1 => x * x_1) 2) n = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
dsimp only [(· ∘ ·)]
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * ((-x) ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) =
    2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
push_cast
[GOAL]
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (2 * ↑n + 1)) + x ^ (2 * n + 1) / (2 * ↑n + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
[PROOFSTEP]
ring_nf
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
[PROOFSTEP]
rw [← h_term_eq_goal, (mul_right_injective₀ (two_ne_zero' ℕ)).hasSum_iff]
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))
[PROOFSTEP]
have h₁ := (hasSum_pow_div_log_of_abs_lt_1 (Eq.trans_lt (abs_neg x) h)).mul_left (-1)
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ HasSum term (log (1 + x) - log (1 - x))
[PROOFSTEP]
convert h₁.add (hasSum_pow_div_log_of_abs_lt_1 h) using 1
[GOAL]
case h.e'_6
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)
[PROOFSTEP]
ring_nf
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ (x : ℕ), ¬x ∈ Set.range ((fun x x_1 => x * x_1) 2) → term x = 0
[PROOFSTEP]
intro m hm
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : ¬m ∈ Set.range ((fun x x_1 => x * x_1) 2)
⊢ term m = 0
[PROOFSTEP]
rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ term m = 0
[PROOFSTEP]
dsimp
[GOAL]
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : term ∘ (fun x x_1 => x * x_1) 2 = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ -1 * ((-x) ^ (m + 1) / (↑m + 1)) + x ^ (m + 1) / (↑m + 1) = 0
[PROOFSTEP]
rw [Even.neg_pow hm, neg_one_mul, neg_add_self]
[GOAL]
a : ℝ
h : 0 < a
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
[PROOFSTEP]
have h₁ : |1 / (2 * a + 1)| < 1 := by
  rw [abs_of_pos, div_lt_one]
  · linarith
  · linarith
  · exact div_pos one_pos (by linarith)
[GOAL]
a : ℝ
h : 0 < a
⊢ |1 / (2 * a + 1)| < 1
[PROOFSTEP]
rw [abs_of_pos, div_lt_one]
[GOAL]
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)
[PROOFSTEP]
exact div_pos one_pos (by linarith)
[GOAL]
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
[PROOFSTEP]
convert hasSum_log_sub_log_of_abs_lt_1 h₁ using 1
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
[PROOFSTEP]
have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith
[GOAL]
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ 2 * a + 1 ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
[PROOFSTEP]
have h₃ := h.ne'
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
[PROOFSTEP]
rw [← log_div]
[GOAL]
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
[PROOFSTEP]
congr
[GOAL]
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * (2 * a) = (2 * a + 1 + 1) * a
[PROOFSTEP]
linarith
[GOAL]
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ ¬2 * a + 1 + 1 = 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_6.hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0
[PROOFSTEP]
field_simp