awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ cos (x + (↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n * cos x

Tactic:
n.cast_negOnePow ℝ ▸ cos_antiperiodic.add_int_mul_eq n

Premises used: Function.Antiperiodic.add_int_mul_eq, Real, Int.cast_negOnePow, Eq.rec, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cos ((↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n

Tactic:
simpa using cos_add_int_mul_pi 0 n

Premises used: OfNat.ofNat, Real.cos_add_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ cos (x + (↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n * cos x

Tactic:
cos_antiperiodic.add_nat_mul_eq n

Premises used: Function.Antiperiodic.add_nat_mul_eq, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n

Tactic:
simpa using cos_add_nat_mul_pi 0 n

Premises used: Real.cos_add_nat_mul_pi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ cos (x - (↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n * cos x

Tactic:
n.cast_negOnePow ℝ ▸ cos_antiperiodic.sub_int_mul_eq n

Premises used: Real, Function.Antiperiodic.sub_int_mul_eq, Int.cast_negOnePow, Eq.rec, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ cos (x - (↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n * cos x

Tactic:
cos_antiperiodic.sub_nat_mul_eq n

Premises used: Real.cos_antiperiodic, Function.Antiperiodic.sub_nat_mul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ cos ((↑n : ℝ) * π - x) = HPow.hPow (α := ℝ) (-1) n * cos x

Tactic:
n.cast_negOnePow ℝ ▸ cos_neg x ▸ cos_antiperiodic.int_mul_sub_eq n

Premises used: Real, Int.cast_negOnePow, Eq.rec, Real.cos_neg, Real.cos_antiperiodic, Function.Antiperiodic.int_mul_sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ cos ((↑n : ℝ) * π - x) = HPow.hPow (α := ℝ) (-1) n * cos x

Tactic:
cos_neg x ▸ cos_antiperiodic.nat_mul_sub_eq n

Premises used: Eq.rec, Function.Antiperiodic.nat_mul_sub_eq, Real.cos_neg, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℝ) * (2 * π) + π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic

Premises used: Function.Periodic.nat_mul, Real.cos_antiperiodic, Real.cos_periodic, Function.Periodic.add_antiperiod_eq, Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cos ((↑n : ℝ) * (2 * π) + π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

Premises used: Function.Periodic.int_mul, Real.cos_antiperiodic, Real.cos_periodic, Function.Periodic.add_antiperiod_eq, Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℝ) * (2 * π) - π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).sub_antiperiod_eq cos_antiperiodic

Premises used: Function.Periodic.nat_mul, Function.Periodic.sub_antiperiod_eq, Real.cos_antiperiodic, Real.cos_periodic, Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cos ((↑n : ℝ) * (2 * π) - π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

Premises used: Function.Periodic.int_mul, Function.Periodic.sub_antiperiod_eq, Real.cos_antiperiodic, Real.cos_periodic, Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π
hx2 : ¬x ≤ 2
linarith : 2 < π - x → 2 - x + (2 - (π - x)) + (π - 4) = 0
⊢ π - x ≤ 2

Tactic:
linarith [pi_le_four]

Premises used: Real.pi_le_four
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Ioo 0 π
⊢ 0 < sin x

Tactic:
sin_pos_of_pos_of_lt_pi hx.1 hx.2

Premises used: Real.sin_pos_of_pos_of_lt_pi, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Icc 0 π
⊢ x ∈ closure (Ioo 0 π)

Tactic:
rw [← closure_Ioo pi_ne_zero.symm] at hx

Premises used: Ne.symm, Real.pi_ne_zero, closure_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x

Tactic:
closure_lt_subset_le continuous_const continuous_sin
      (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)

Premises used: closure_lt_subset_le, Set.Mem, continuous_const, Real.continuous_sin, closure_mono, Real.sin_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x

Tactic:
exact
    closure_lt_subset_le continuous_const continuous_sin
      (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)

Premises used: closure_lt_subset_le, continuous_const, Real.continuous_sin, closure_mono, Real.sin_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 ≤ x
hxp : x ≤ π
⊢ 0 ≤ sin x

Tactic:
sin_nonneg_of_mem_Icc ⟨h0x, hxp⟩

Premises used: Real.sin_nonneg_of_mem_Icc, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx0 : x < 0
hpx : -π < x
⊢ sin x < 0

Tactic:
neg_pos.1 <| sin_neg x ▸ sin_pos_of_pos_of_lt_pi (neg_pos.2 hx0) (neg_lt.1 hpx)

Premises used: Iff.mpr, neg_pos, Eq.rec, Real.sin_neg, Real.sin_pos_of_pos_of_lt_pi, Iff.mp, neg_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -π ≤ x
⊢ sin x ≤ 0

Tactic:
neg_nonneg.1 <| sin_neg x ▸ sin_nonneg_of_nonneg_of_le_pi (neg_nonneg.2 hx0) (neg_le.1 hpx)

Premises used: Iff.mpr, neg_le, Real.sin_nonneg_of_nonneg_of_le_pi, Eq.rec, Real.sin_neg, neg_nonneg, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : |x| ≤ π
inl : ∀ (h : x < 0), |sin x| = sin |x|
inr : ∀ (h : 0 ≤ x), |sin x| = sin |x|
⊢ |sin x| = sin |x|

Tactic:
rcases lt_or_ge x 0 with h | h

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : |x| ≤ π
h : x < 0
inl : |sin x| = sin (-x)
inl₁ : |sin x| = -sin x
inl₂ inl₃ : -sin x = -sin x
⊢ |sin x| = sin |x|

Tactic:
rw [abs_of_neg h, sin_neg,
      abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)]

Premises used: abs_of_neg, abs_le, LT.lt.le, Real.sin_neg, Real.sin_nonpos_of_nonpos_of_neg_pi_le, abs_of_nonpos, And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : |x| ≤ π
h : 0 ≤ x
inr : |sin x| = sin x
inr₁ inr₂ : sin x = sin x
⊢ |sin x| = sin |x|

Tactic:
rw [abs_of_nonneg h, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi h (abs_le.1 hx).2)]

Premises used: abs_le, Real.sin_nonneg_of_nonneg_of_le_pi, And.right, Iff.mp, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1

Tactic:
simpa [sq, mul_self_eq_one_iff] using sin_sq_add_cos_sq (π / 2)

Premises used: Real.pi, HDiv.hDiv, sq, mul_self_eq_one_iff, Real.sin_sq_add_cos_sq, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
this : sin (π / 2) = 1 ∨ sin (π / 2) = -1
h : sin (π / 2) = -1
⊢ ¬LT.lt (α := ℝ) 0 (-1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin (x + π / 2) = cos x

Tactic:
simp [sin_add]

Premises used: Real.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin (x - π / 2) = -cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Premises used: sub_eq_add_neg, Real.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin (π / 2 - x) = cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Premises used: sub_eq_add_neg, Real.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ cos (x + π / 2) = -sin x

Tactic:
simp [cos_add]

Premises used: Real.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ cos (x - π / 2) = sin x

Tactic:
simp [sub_eq_add_neg, cos_add]

Premises used: sub_eq_add_neg, Real.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
rw : cos (-(π / 2 - x)) = sin x
rw₁ : cos (x - π / 2) = sin x
rw₂ rw₃ : sin x = sin x
⊢ cos (π / 2 - x) = sin x

Tactic:
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]

Premises used: neg_sub, Real.cos_neg, Real.cos_sub_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : x + π / 2 < 0 → 2 / 2 = 1
linarith₁ : x + π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x + π / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : x + π / 2 < 0 → 2 / 2 = 1
linarith₄ : x + π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x + π / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₆ : x + π / 2 < 0 → 2 * x + 1 * π - HMul.hMul (α := ℝ) 2 0 + (-(1 * π) - 2 * x) = 0
⊢ 0 ≤ x + π / 2

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : π < x + π / 2 → 2 / 2 = 1
linarith₁ : π < x + π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < x + π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < x + π / 2 → 2 / 2 = 1
linarith₄ : π < x + π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π < x + π / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : π < x + π / 2 → 2 * π - (2 * x + 1 * π) + (2 * x - 1 * π) = 0
⊢ x + π / 2 ≤ π

Tactic:
linarith [hx.2]

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
⊢ 0 ≤ cos x

Tactic:
cos_nonneg_of_mem_Icc ⟨hl, hu⟩

Premises used: Real.cos_nonneg_of_mem_Icc, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₇ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₉ : π - x ≤ -(π / 2) → 2 * x - (2 * π + 1 * π) + (2 * π - 2 * x - -(1 * π)) = 0
⊢ -(π / 2) < π - x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π / 2 ≤ π - x → 2 / 2 = 1
linarith₁ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ π - x → 2 / 2 = 1
linarith₄ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 ≤ π - x → 2 / 2 = 1
linarith₇ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
linarith₉ : π / 2 ≤ π - x → 1 * π - 2 * x + (1 * π - (2 * π - 2 * x)) = 0
⊢ π - x < π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π - x < -(π / 2) → 2 / 2 = 1
linarith₁ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : π - x < -(π / 2) → 2 / 2 = 1
linarith₄ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : π - x < -(π / 2) → 2 / 2 = 1
linarith₇ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₉ : π - x < -(π / 2) → 2 * x - (2 * π + 1 * π) + (2 * π - 2 * x - -(1 * π)) = 0
⊢ -(π / 2) ≤ π - x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π / 2 < π - x → 2 / 2 = 1
linarith₁ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 < π - x → 2 / 2 = 1
linarith₄ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 < π - x → 2 / 2 = 1
linarith₇ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
linarith₉ : π / 2 < π - x → 1 * π - 2 * x + (1 * π - (2 * π - 2 * x)) = 0
⊢ π - x ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : 0 ≤ x
hu : x ≤ π
rw : sin x = |sin x|
rw₁ rw₂ : sin x = sin x
⊢ sin x = √(1 - HPow.hPow (β := ℕ) (cos x) 2)

Tactic:
rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]

Premises used: Real.sin_nonneg_of_nonneg_of_le_pi, Real.abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
rw : cos x = |cos x|
rw₁ rw₂ : cos x = cos x
⊢ cos x = √(1 - HPow.hPow (β := ℕ) (sin x) 2)

Tactic:
rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]

Premises used: Real.cos_nonneg_of_mem_Icc, Real.abs_cos_eq_sqrt_one_sub_sin_sq, And.intro, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
left : -(π / 2) ≤ x / 2
right : x / 2 ≤ π / 2
⊢ x / 2 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
linarith : x / 2 < -(π / 2) → 2 / 2 = 1
linarith₁ : x / 2 < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x / 2 < -(π / 2) → 2 / 2 = 1
linarith₃ : x / 2 < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : x / 2 < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₅ : x / 2 < -(π / 2) → -π - x + (1 * x - -(1 * π)) = 0
⊢ -(π / 2) ≤ x / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
linarith : π / 2 < x / 2 → 2 / 2 = 1
linarith₁ : π / 2 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < x / 2 → 2 / 2 = 1
linarith₃ : π / 2 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 < x / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π / 2 < x / 2 → x - π + (1 * π - 1 * x) = 0
⊢ x / 2 ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ 0 ≤ cos (x / 2)

Tactic:
have : 0 ≤ cos (x / 2) := cos_nonneg_of_mem_Icc <| by constructor <;> linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
rw : √(HPow.hPow (β := ℕ) (cos (x / 2)) 2) = √((1 + cos x) / 2)
rw₁ : √(1 / 2 + cos (2 * (x / 2)) / 2) = √((1 + cos x) / 2)
rw₂ : √(1 / 2 + cos (2 * (x / 2)) / 2) = √(1 / 2 + cos x / 2)
rw₃ : √(1 / 2 + cos (x / 2 + x / 2) / 2) = √(1 / 2 + cos x / 2)
rw₄ rw₅ : √(1 / 2 + cos x / 2) = √(1 / 2 + cos x / 2)
⊢ cos (x / 2) = √((1 + cos x) / 2)

Tactic:
rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]

Premises used: add_halves, two_mul, Real.sqrt_sq, Real.cos_sq, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
rw : √(HPow.hPow (β := ℕ) (sin (x / 2)) 2) = √((1 - cos x) / 2)
rw₁ : √(1 / 2 - cos (2 * (x / 2)) / 2) = √((1 - cos x) / 2)
rw₂ : √(1 / 2 - cos (x / 2 + x / 2) / 2) = √((1 - cos x) / 2)
rw₃ : √(1 / 2 - cos x / 2) = √((1 - cos x) / 2)
rw₄ rw₅ : √(1 / 2 - cos x / 2) = √(1 / 2 - cos x / 2)
⊢ |sin (x / 2)| = √((1 - cos x) / 2)

Tactic:
rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]

Premises used: add_halves, Real.sqrt_sq_eq_abs, two_mul, Real.sin_sq_eq_half_sub, sub_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
rw : 0 ≤ sin (x / 2)
⊢ sin (x / 2) = √((1 - cos x) / 2)

Tactic:
rw [← abs_sin_half, abs_of_nonneg]

Premises used: Real.abs_sin_half, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
h0x : 0 ≤ x / 2
hxp : x / 2 ≤ π
⊢ 0 ≤ sin (x / 2)

Tactic:
apply sin_nonneg_of_nonneg_of_le_pi

Premises used: Real.sin_nonneg_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
linarith : x / 2 < 0 → 2 / 2 = 1
linarith₁ : x / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : x / 2 < 0 → 0 - x + (1 * x - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ x / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
linarith : π < x / 2 → 2 / 2 = 1
linarith₁ : π < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < x / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < x / 2 → x - 2 * π + (2 * π - 1 * x) = 0
⊢ x / 2 ≤ π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
rw : sin (x / 2) ≤ 0
⊢ sin (x / 2) = -√((1 - cos x) / 2)

Tactic:
rw [← abs_sin_half, abs_of_nonpos, neg_neg]

Premises used: neg_neg, Real.abs_sin_half, abs_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
hx0 : x / 2 ≤ 0
hpx : -π ≤ x / 2
⊢ sin (x / 2) ≤ 0

Tactic:
apply sin_nonpos_of_nonpos_of_neg_pi_le

Premises used: Real.sin_nonpos_of_nonpos_of_neg_pi_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
linarith : 0 < x / 2 → 2 / 2 = 1
linarith₁ : 0 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 < x / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : 0 < x / 2 → x - 0 + (HMul.hMul (α := ℝ) 2 0 - 1 * x) = 0
⊢ x / 2 ≤ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
linarith : x / 2 < -π → 2 / 2 = 1
linarith₁ : x / 2 < -π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x / 2 < -π → GT.gt (α := ℝ) 2 0
linarith₃ : x / 2 < -π → -(2 * π) - x + (1 * x - -(2 * π)) = 0
⊢ -π ≤ x / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : sin x = 0
contrapose! : ∀ (h : x ≠ 0), sin x ≠ 0
⊢ x = 0

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : x < 0
⊢ sin x ≠ 0

Tactic:
(sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne

Premises used: Real.sin_neg_of_neg_of_neg_pi_lt, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : x < 0
⊢ sin x ≠ 0

Tactic:
exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne

Premises used: Real.sin_neg_of_neg_of_neg_pi_lt, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : 0 < x
⊢ sin x ≠ 0

Tactic:
(sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

Premises used: Real.sin_pos_of_pos_of_lt_pi, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : 0 < x
⊢ sin x ≠ 0

Tactic:
exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

Premises used: Real.sin_pos_of_pos_of_lt_pi, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
⊢ x < 0 ∨ 0 < x

Tactic:
cases h.lt_or_gt with
    | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
    | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x = 0
⊢ sin x = 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h : sin x = 0
h₃ : 0 < x - (↑⌊x / π⌋ : ℝ) * π
⊢ 0 = sin (x - (↑⌊x / π⌋ : ℝ) * π)

Tactic:
simp [sub_eq_add_neg, sin_add, h, sin_int_mul_pi]

Premises used: sub_eq_add_neg, Real.sin_add, Real.sin_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
contrapose! : sin x = 0 ↔ ∃ (n : ℤ), (↑n : ℝ) * π = x
⊢ sin x ≠ 0 ↔ ∀ (n : ℤ), (↑n : ℝ) * π ≠ x

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin x = 0 ↔ ∃ (n : ℤ), (↑n : ℝ) * π = x

Tactic:
sin_eq_zero_iff

Premises used: Real.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin x = 0 ↔ ∃ (n : ℤ), (↑n : ℝ) * π = x

Tactic:
exact sin_eq_zero_iff

Premises used: Real.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
rw : sin x = 0 ↔ cos x * cos x = 1
rw₁ : sin x = 0 ↔ cos x * cos x = HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
rw₂ : ℝ
rw₃ : sin x = 0 ↔ cos x * cos x = sin x * sin x + HPow.hPow (β := ℕ) (cos x) 2
rw₄ : ℝ
rw₅ : sin x = 0 ↔ cos x * cos x = sin x * sin x + cos x * cos x
rw₆ : ℝ
rw₇ : sin x = 0 ↔ sin x * sin x = 0
rw₈ : sin x = 0 ↔ sin x = 0 ∨ sin x = 0
rw₉ rw₁₀ : sin x = 0 ↔ sin x = 0
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]

Premises used: sq, mul_eq_zero, mul_self_eq_one_iff, Real.sin_sq_add_cos_sq, or_self, right_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
rw : cos x = 0 ↔ sin x * sin x = 1
rw₁ : cos x = 0 ↔ sin x * sin x = HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
rw₂ : ℝ
rw₃ : cos x = 0 ↔ sin x * sin x = sin x * sin x + HPow.hPow (β := ℕ) (cos x) 2
rw₄ : ℝ
rw₅ : cos x = 0 ↔ sin x * sin x = sin x * sin x + cos x * cos x
rw₆ : ℝ
rw₇ : cos x = 0 ↔ cos x * cos x = 0
rw₈ : cos x = 0 ↔ cos x = 0 ∨ cos x = 0
rw₉ rw₁₀ : cos x = 0 ↔ cos x = 0
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]

Premises used: left_eq_add, sq, mul_eq_zero, mul_self_eq_one_iff, Real.sin_sq_add_cos_sq, or_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑n : ℝ) * π = x
hn0 : n % 2 = 0
rwa : HMul.hMul (α := ℝ) (↑(n / 2) : ℝ) 2 * π = x
rwa₁ : HMul.hMul (α := ℝ) (↑(n / 2) : ℝ) (↑2 : ℝ) * π = x
rwa₂ : (↑(n / 2 * 2) : ℝ) * π = x
rwa₃ rwa₄ rwa₅ rwa₆ : (↑n : ℝ) * π = x
⊢ (↑(n / 2) : ℝ) * (2 * π) = x

Tactic:
rwa [← mul_assoc, ← @Int.cast_two ℝ, ← Int.cast_mul,
            Int.ediv_mul_cancel (Int.dvd_iff_emod_eq_zero.2 hn0)]

Premises used: Iff.mpr, Int.ediv_mul_cancel, mul_assoc, Int.cast_two, Int.cast_mul, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑n : ℝ) * π = x
hn1 : n % 2 = 1
⊢ (↑(n / 2) : ℝ) * (2 * π) + π = x

Tactic:
rw [← Int.emod_add_mul_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul,
          add_comm, mul_comm (2 : ℤ), Int.cast_mul, mul_assoc, Int.cast_two] at hn

Premises used: add_mul, mul_assoc, Int.cast_two, Int.cast_add, add_comm, Int.emod_add_mul_ediv, Int.cast_mul, mul_comm, OfNat.ofNat, one_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑n : ℝ) * π = x
hn1 : n % 2 = 1
hn₁ : (↑(n / 2) : ℝ) * (2 * π) + π = x
⊢ n % 2 = 1

Tactic:
rw [← Int.emod_add_mul_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul,
          add_comm, mul_comm (2 : ℤ), Int.cast_mul, mul_assoc, Int.cast_two] at hn

Premises used: add_mul, mul_assoc, Int.cast_two, Int.cast_add, add_comm, Int.emod_add_mul_ediv, Int.cast_mul, mul_comm, OfNat.ofNat, one_mul, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑(n / 2) : ℝ) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ Eq (α := ℝ) (-1) 1

Tactic:
rw [← hn, cos_int_mul_two_pi_add_pi] at h

Premises used: Real.cos_int_mul_two_pi_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑(n / 2) : ℝ) * (2 * π) + π = x
hn1 : n % 2 = 1
h₁ : Eq (α := ℝ) (-1) 1
⊢ (↑(n / 2) : ℝ) * (2 * π) + π = x

Tactic:
rw [← hn, cos_int_mul_two_pi_add_pi] at h

Premises used: Real.cos_int_mul_two_pi_add_pi