awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ -(π / 2) ≤ x / 2
have linarith₄ : x / 2 < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ -(π / 2) ≤ x / 2
have linarith₅ : x / 2 < -(π / 2) → -π - x + (1 * x - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ x / 2 ≤ π / 2
have linarith : π / 2 < x / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
linarith : π / 2 < x / 2 → 2 / 2 = 1
⊢ x / 2 ≤ π / 2
have linarith₁ : π / 2 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ x / 2 ≤ π / 2
have linarith₄ : π / 2 < x / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ x / 2 ≤ π / 2
have linarith₅ : π / 2 < x / 2 → x - π + (1 * π - 1 * x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ cos (x / 2) = √((1 + cos x) / 2)
have this : 0 ≤ cos (x / 2)
Tactic: have : 0 ≤ cos (x / 2) := cos_nonneg_of_mem_Icc <| by constructor <;> linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
⊢ cos (x / 2) = √((1 + cos x) / 2)
have rw : √(HPow.hPow (β := ℕ) (cos (x / 2)) 2) = √((1 + cos x) / 2)
Tactic: rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
rw : √(HPow.hPow (β := ℕ) (cos (x / 2)) 2) = √((1 + cos x) / 2)
⊢ cos (x / 2) = √((1 + cos x) / 2)
have rw₁ : √(1 / 2 + cos (2 * (x / 2)) / 2) = √((1 + cos x) / 2)
Tactic: rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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)
⊢ cos (x / 2) = √((1 + cos x) / 2)
have rw₂ : √(1 / 2 + cos (2 * (x / 2)) / 2) = √(1 / 2 + cos x / 2)
Tactic: rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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)
⊢ cos (x / 2) = √((1 + cos x) / 2)
have rw₃ : √(1 / 2 + cos (x / 2 + x / 2) / 2) = √(1 / 2 + cos x / 2)
Tactic: rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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)
⊢ cos (x / 2) = √((1 + cos x) / 2)
have rw₄ : √(1 / 2 + cos x / 2) = √(1 / 2 + cos x / 2)
Tactic: rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
⊢ |sin (x / 2)| = √((1 - cos x) / 2)
have rw : √(HPow.hPow (β := ℕ) (sin (x / 2)) 2) = √((1 - cos x) / 2)
Tactic: rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : √(HPow.hPow (β := ℕ) (sin (x / 2)) 2) = √((1 - cos x) / 2)
⊢ |sin (x / 2)| = √((1 - cos x) / 2)
have rw₁ : √(1 / 2 - cos (2 * (x / 2)) / 2) = √((1 - cos x) / 2)
Tactic: rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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)
⊢ |sin (x / 2)| = √((1 - cos x) / 2)
have rw₂ : √(1 / 2 - cos (x / 2 + x / 2) / 2) = √((1 - cos x) / 2)
Tactic: rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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)
⊢ |sin (x / 2)| = √((1 - cos x) / 2)
have rw₃ : √(1 / 2 - cos x / 2) = √((1 - cos x) / 2)
Tactic: rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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)
⊢ |sin (x / 2)| = √((1 - cos x) / 2)
have rw₄ : √(1 / 2 - cos x / 2) = √(1 / 2 - cos x / 2)
Tactic: rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ sin (x / 2) = √((1 - cos x) / 2)
have rw : 0 ≤ sin (x / 2)
Tactic: rw [← abs_sin_half, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)
have h0x : 0 ≤ x / 2
Tactic: apply sin_nonneg_of_nonneg_of_le_pi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
h0x : 0 ≤ x / 2
⊢ 0 ≤ sin (x / 2)
have hxp : x / 2 ≤ π
Tactic: apply sin_nonneg_of_nonneg_of_le_pi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ x / 2
have linarith : x / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
linarith : x / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ x / 2
have linarith₁ : x / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
linarith : x / 2 < 0 → 2 / 2 = 1
linarith₁ : x / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ x / 2
have linarith₂ : x / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ 0 ≤ x / 2
have linarith₃ : x / 2 < 0 → 0 - x + (1 * x - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ x / 2 ≤ π
have linarith : π < x / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
linarith : π < x / 2 → 2 / 2 = 1
⊢ x / 2 ≤ π
have linarith₁ : π < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
linarith : π < x / 2 → 2 / 2 = 1
linarith₁ : π < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ x / 2 ≤ π
have linarith₂ : π < x / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ x / 2 ≤ π
have linarith₃ : π < x / 2 → x - 2 * π + (2 * π - 1 * x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) = -√((1 - cos x) / 2)
have rw : sin (x / 2) ≤ 0
Tactic: rw [← abs_sin_half, abs_of_nonpos, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) ≤ 0
have hx0 : x / 2 ≤ 0
Tactic: apply sin_nonpos_of_nonpos_of_neg_pi_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
hx0 : x / 2 ≤ 0
⊢ sin (x / 2) ≤ 0
have hpx : -π ≤ x / 2
Tactic: apply sin_nonpos_of_nonpos_of_neg_pi_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ x / 2 ≤ 0
have linarith : 0 < x / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
linarith : 0 < x / 2 → 2 / 2 = 1
⊢ x / 2 ≤ 0
have linarith₁ : 0 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
linarith : 0 < x / 2 → 2 / 2 = 1
linarith₁ : 0 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ x / 2 ≤ 0
have linarith₂ : 0 < x / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ x / 2 ≤ 0
have linarith₃ : 0 < x / 2 → x - 0 + (HMul.hMul (α := ℝ) 2 0 - 1 * x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ -π ≤ x / 2
have linarith : x / 2 < -π → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
linarith : x / 2 < -π → 2 / 2 = 1
⊢ -π ≤ x / 2
have linarith₁ : x / 2 < -π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
linarith : x / 2 < -π → 2 / 2 = 1
linarith₁ : x / 2 < -π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -π ≤ x / 2
have linarith₂ : x / 2 < -π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ -π ≤ x / 2
have linarith₃ : x / 2 < -π → -(2 * π) - x + (1 * x - -(2 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : sin x = 0
⊢ x = 0
have contrapose! : ∀ (h : x ≠ 0), sin x ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
⊢ sin x ≠ 0
have x₁ : 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'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
⊢ sin x ≠ 0 ↔ ∀ (n : ℤ), (↑n : ℝ) * π ≠ x
have contrapose! : sin x = 0 ↔ ∃ (n : ℤ), (↑n : ℝ) * π = x
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw : sin x = 0 ↔ cos x * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : sin x = 0 ↔ cos x * cos x = 1
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw₁ : sin x = 0 ↔ cos x * cos x = HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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₂ : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw₃ : sin x = 0 ↔ cos x * cos x = sin x * sin x + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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₄ : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw₅ : sin x = 0 ↔ cos x * cos x = sin x * sin x + cos x * cos x
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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₆ : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw₇ : sin x = 0 ↔ sin x * sin x = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw₈ : sin x = 0 ↔ sin x = 0 ∨ sin x = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
have rw₉ : sin x = 0 ↔ sin x = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw : cos x = 0 ↔ sin x * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : cos x = 0 ↔ sin x * sin x = 1
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw₁ : cos x = 0 ↔ sin x * sin x = HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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₂ : ℝ
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw₃ : cos x = 0 ↔ sin x * sin x = sin x * sin x + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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₄ : ℝ
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw₅ : cos x = 0 ↔ sin x * sin x = sin x * sin x + cos x * cos x
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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₆ : ℝ
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw₇ : cos x = 0 ↔ cos x * cos x = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw₈ : cos x = 0 ↔ cos x = 0 ∨ cos x = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1
have rw₉ : cos x = 0 ↔ cos x = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑n : ℝ) * π = x
hn0 : n % 2 = 0
⊢ (↑(n / 2) : ℝ) * (2 * π) = x
have rwa : HMul.hMul (α := ℝ) (↑(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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑n : ℝ) * π = x
hn0 : n % 2 = 0
rwa : HMul.hMul (α := ℝ) (↑(n / 2) : ℝ) 2 * π = x
⊢ (↑(n / 2) : ℝ) * (2 * π) = x
have rwa₁ : HMul.hMul (α := ℝ) (↑(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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
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
⊢ (↑(n / 2) : ℝ) * (2 * π) = x
have rwa₂ : (↑(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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑n : ℝ) * π = x
hn1 : n % 2 = 1
⊢ (↑(n / 2) : ℝ) * (2 * π) = x
have hn₁ : (↑(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
Cleared hypotheses: hn, hn1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x : ℝ
h : cos x = 1
n : ℤ
hn : (↑(n / 2) : ℝ) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ (↑(n / 2) : ℝ) * (2 * π) = x
have h₁ : Eq (α := ℝ) (-1) 1
Tactic: rw [← hn, cos_int_mul_two_pi_add_pi] at h
Cleared hypotheses: h, hn, hn1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : -(2 * π) < x
hx₂ : x < 2 * π
h : cos x = 1
⊢ x = 0
have rcases : ∀ (n : ℤ) (hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)) (hx₂ : (↑n : ℝ) * (2 * π) < 2 * π) (h : cos ((↑n : ℝ) * (2 * π)) = 1),
  (↑n : ℝ) * (2 * π) = 0
Tactic: rcases (cos_eq_one_iff _).1 h with ⟨n, rfl⟩
Cleared hypotheses: x, hx₁, hx₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : (↑n : ℝ) * (2 * π) < 2 * π
h : cos ((↑n : ℝ) * (2 * π)) = 1
⊢ (↑n : ℝ) * (2 * π) = 0
have hx₃ : LT.lt (α := ℝ) (↑n : ℝ) 1
Tactic: rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂
Cleared hypotheses: hx₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
⊢ (↑n : ℝ) * (2 * π) = 0
have hx₃ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
Tactic: rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁
Cleared hypotheses: hx₁, hx₂, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℤ
hx₁ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
⊢ (↑n : ℝ) * (2 * π) = 0
have hx₃ : -n < 1
Tactic: norm_cast at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℤ
hx₁ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₃ : -n < 1
⊢ (↑n : ℝ) * (2 * π) = 0
have hx₄ : n < 1
Tactic: norm_cast at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℤ
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ (↑n : ℝ) * (2 * π) = 0
have obtain : ∀ (h : cos ((↑0 : ℝ) * (2 * π)) = 1) (hx₁ : LT.lt (α := ℤ) (-0) 1) (hx₂ : LT.lt (α := ℤ) 0 1), (↑0 : ℝ) * (2 * π) = 0
Tactic: obtain rfl : n = 0 := le_antisymm (by lia) (by lia)
Cleared hypotheses: n, h, hx₁, hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ sin x < sin y
have rw : 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
Tactic: rw [← sub_pos, sin_sub_sin]