awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hn₁ : (↑(n / 2) : ℝ) * (2 * π) + π = x
⊢ n % 2 = 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 : ℝ
n : ℤ
h : Eq (α := ℝ) (-1) 1
hn : (↑(n / 2) : ℝ) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ¬Eq (α := ℝ) (-1) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
h : Eq (α := ℝ) (-1) 1
hn : (↑(n / 2) : ℝ) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ (↑(n / 2) : ℝ) * (2 * π) = x

Tactic:
exact absurd h (by norm_num)

Premises used: absurd
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -(2 * π) < x
hx₂ : x < 2 * π
h : cos x = 1
rcases :
  ∀ (n : ℤ) (hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)) (hx₂ : (↑n : ℝ) * (2 * π) < 2 * π) (h : cos ((↑n : ℝ) * (2 * π)) = 1),
    (↑n : ℝ) * (2 * π) = 0
⊢ x = 0

Tactic:
rcases (cos_eq_one_iff _).1 h with ⟨n, rfl⟩

Premises used: Iff.mp, Real.cos_eq_one_iff, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : (↑n : ℝ) * (2 * π) < 2 * π
h : cos ((↑n : ℝ) * (2 * π)) = 1
⊢ LT.lt (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂

Premises used: Real.two_pi_pos, mul_lt_iff_lt_one_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : (↑n : ℝ) * (2 * π) < 2 * π
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₃ : LT.lt (α := ℝ) (↑n : ℝ) 1
⊢ cos ((↑n : ℝ) * (2 * π)) = 1

Tactic:
rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂

Premises used: Real.two_pi_pos, mul_lt_iff_lt_one_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
⊢ LT.lt (α := ℝ) (-(↑n : ℝ)) 1

Tactic:
rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁

Premises used: Real.two_pi_pos, mul_lt_iff_lt_one_left, neg_mul_eq_neg_mul, neg_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₃ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
⊢ LT.lt (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁

Premises used: Real.two_pi_pos, mul_lt_iff_lt_one_left, neg_mul_eq_neg_mul, neg_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : -(2 * π) < (↑n : ℝ) * (2 * π)
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₃ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
hx₄ : LT.lt (α := ℝ) (↑n : ℝ) 1
⊢ cos ((↑n : ℝ) * (2 * π)) = 1

Tactic:
rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁

Premises used: Real.two_pi_pos, mul_lt_iff_lt_one_left, neg_mul_eq_neg_mul, neg_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
⊢ -n < 1

Tactic:
norm_cast at hx₁ hx₂
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
hx₁ : LT.lt (α := ℝ) (-(↑n : ℝ)) 1
hx₂ : LT.lt (α := ℝ) (↑n : ℝ) 1
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₃ : -n < 1
⊢ n < 1

Tactic:
norm_cast at hx₁ hx₂
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ n ≤ 0

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ 0 ≤ n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
h : cos ((↑n : ℝ) * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
obtain :
  ∀ (h : cos ((↑0 : ℝ) * (2 * π)) = 1) (hx₁ : LT.lt (α := ℤ) (-0) 1) (hx₂ : LT.lt (α := ℤ) 0 1), (↑0 : ℝ) * (2 * π) = 0
⊢ (↑n : ℝ) * (2 * π) = 0

Tactic:
obtain rfl : n = 0 := le_antisymm (by lia) (by lia)

Premises used: le_antisymm, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : cos ((↑0 : ℝ) * (2 * π)) = 1
hx₁ : LT.lt (α := ℤ) (-0) 1
hx₂ : LT.lt (α := ℤ) 0 1
⊢ (↑0 : ℝ) * (2 * π) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx₁ : -(2 * π) < x
hx₂ : x < 2 * π
h : x = 0
⊢ cos x = 1

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
rw : 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
⊢ sin x < sin y

Tactic:
rw [← sub_pos, sin_sub_sin]

Premises used: sub_pos, Real.sin_sub_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
h0x : 0 < (y - x) / 2
hxp : (y - x) / 2 < π
⊢ 0 < sin ((y - x) / 2)

Tactic:
apply sin_pos_of_pos_of_lt_pi

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

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

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < sin ((y - x) / 2)

Tactic:
have : 0 < sin ((y - x) / 2) := by apply sin_pos_of_pos_of_lt_pi <;> linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < cos ((y + x) / 2)

Tactic:
cos_pos_of_mem_Ioo ⟨?_, ?_⟩

Premises used: Real.cos_pos_of_mem_Ioo, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
refine_1 : -(π / 2) < (y + x) / 2
refine_2 : (y + x) / 2 < π / 2
⊢ 0 < cos ((y + x) / 2)

Tactic:
refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩

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

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

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < cos ((y + x) / 2)

Tactic:
have : 0 < cos ((y + x) / 2) := by refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this_1 : 0 < sin ((y - x) / 2)
this : 0 < cos ((y + x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ StrictMonoOn sin (Icc (-(π / 2)) (π / 2))

Tactic:
fun _ hx _ hy hxy =>
  sin_lt_sin_of_lt_of_le_pi_div_two hx.1 hy.2 hxy

Premises used: Real.sin_lt_sin_of_lt_of_le_pi_div_two, And.right, And.left, StrictMonoOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ MonotoneOn sin (Icc (-(π / 2)) (π / 2))

Tactic:
strictMonoOn_sin.monotoneOn

Premises used: StrictMonoOn.monotoneOn, Real.strictMonoOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
rw : sin (π / 2 - y) < sin (π / 2 - x)
⊢ cos y < cos x

Tactic:
rw [← sin_pi_div_two_sub, ← sin_pi_div_two_sub]

Premises used: Real.sin_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx₂ : -(π / 2) ≤ π / 2 - y
hy₃ : π / 2 - x ≤ π / 2
hxy₁ : π / 2 - y < π / 2 - x
⊢ sin (π / 2 - y) < sin (π / 2 - x)

Tactic:
apply sin_lt_sin_of_lt_of_le_pi_div_two

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

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

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

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

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ StrictAntiOn cos (Icc 0 π)

Tactic:
fun _ hx _ hy hxy =>
  cos_lt_cos_of_nonneg_of_le_pi hx.1 hy.2 hxy

Premises used: StrictAntiOn, And.right, And.left, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ AntitoneOn cos (Icc 0 π)

Tactic:
strictAntiOn_cos.antitoneOn

Premises used: StrictAntiOn.antitoneOn, Real.strictAntiOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x ≤ y
⊢ cos y ≤ cos x

Tactic:
(strictAntiOn_cos.le_iff_ge ⟨hx₁.trans hxy, hy₂⟩ ⟨hx₁, hxy.trans hy₂⟩).2 hxy

Premises used: Iff.mpr, StrictAntiOn.le_iff_ge, And.intro, Real.strictAntiOn_cos, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x ≤ y
⊢ sin x ≤ sin y

Tactic:
(strictMonoOn_sin.le_iff_le ⟨hx₁, hxy.trans hy₂⟩ ⟨hx₁.trans hxy, hy₂⟩).2 hxy

Premises used: Iff.mpr, And.intro, StrictMonoOn.le_iff_le, LE.le.trans, Real.strictMonoOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ InjOn sin (Icc (-(π / 2)) (π / 2))

Tactic:
strictMonoOn_sin.injOn

Premises used: StrictMonoOn.injOn, Real.strictMonoOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ InjOn cos (Icc 0 π)

Tactic:
strictAntiOn_cos.injOn

Premises used: StrictAntiOn.injOn, Real.strictAntiOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ SurjOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)

Tactic:
simpa only [sin_neg, sin_pi_div_two] using
    intermediate_value_Icc (neg_le_self pi_div_two_pos.le) continuous_sin.continuousOn

Premises used: Real.sin_pi_div_two, Continuous.continuousOn, Real.pi_div_two_pos, LT.lt.le, Real.sin_neg, Real.continuous_sin, neg_le_self, intermediate_value_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ SurjOn cos (Icc 0 π) (Icc (-1) 1)

Tactic:
simpa only [cos_zero, cos_pi] using intermediate_value_Icc' pi_pos.le continuous_cos.continuousOn

Premises used: Continuous.continuousOn, intermediate_value_Icc', Real.pi_pos, LT.lt.le, Real.continuous_cos, Real.cos_zero, Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) (sin x)

Tactic:
⟨neg_one_le_sin x, sin_le_one x⟩

Premises used: Real.sin_le_one, Set.Mem, setOf, Set.Icc, And.intro, Real.neg_one_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) (cos x)

Tactic:
⟨neg_one_le_cos x, cos_le_one x⟩

Premises used: Set.Mem, setOf, Real.neg_one_le_cos, Set.Icc, And.intro, Real.cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
s : Set ℝ
⊢ MapsTo sin s (Icc (-1) 1)

Tactic:
fun x _ => sin_mem_Icc x

Premises used: Set.MapsTo, Real.sin_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
s : Set ℝ
⊢ MapsTo cos s (Icc (-1) 1)

Tactic:
fun x _ => cos_mem_Icc x

Premises used: Set.MapsTo, Real.cos_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ BijOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)

Tactic:
⟨mapsTo_sin _, injOn_sin, surjOn_sin⟩

Premises used: Real.surjOn_sin, Real.injOn_sin, Real.mapsTo_sin, And.intro, Set.BijOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ BijOn cos (Icc 0 π) (Icc (-1) 1)

Tactic:
⟨mapsTo_cos _, injOn_cos, surjOn_cos⟩

Premises used: Real.mapsTo_cos, Real.surjOn_cos, And.intro, Set.BijOn, Real.injOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ range cos = Icc (-1) 1

Tactic:
Subset.antisymm (range_subset_iff.2 cos_mem_Icc) surjOn_cos.subset_range

Premises used: Set.Subset.antisymm, Iff.mpr, Real.surjOn_cos, Set.range_subset_iff, Real.cos_mem_Icc, Set.SurjOn.subset_range
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ range sin = Icc (-1) 1

Tactic:
Subset.antisymm (range_subset_iff.2 sin_mem_Icc) surjOn_sin.subset_range

Premises used: Set.Subset.antisymm, Iff.mpr, Real.surjOn_sin, Set.range_subset_iff, Real.sin_mem_Icc, Set.SurjOn.subset_range
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : Set.Infinite (α := ℝ) (Icc (-1) 1)
⊢ (range cos).Infinite

Tactic:
rw [Real.range_cos]

Premises used: Real.range_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ LT.lt (α := ℝ) (-1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Set.Infinite (α := ℝ) (Icc (-1) 1)

Tactic:
exact Icc_infinite (by simp)

Premises used: Set.Icc_infinite
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : Set.Infinite (α := ℝ) (Icc (-1) 1)
⊢ (range sin).Infinite

Tactic:
rw [Real.range_sin]

Premises used: Real.range_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ x.sqrtTwoAddSeries 0 = x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sqrtTwoAddSeries 0 1 = √2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sqrtTwoAddSeries 0 2 = √(2 + √2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sqrtTwoAddSeries 0 0 < 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < 2

Tactic:
lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le

Premises used: LT.lt.le, Eq.le, Real.sqrt_sq, zero_lt_two, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
refine : sqrtTwoAddSeries 0 (n + 1) < √(HPow.hPow (α := ℝ) (β := ℕ) 2 2)
⊢ sqrtTwoAddSeries 0 (n + 1) < 2

Tactic:
refine lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le

Premises used: LT.lt.le, Eq.le, Real.sqrt_sq, zero_lt_two, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
rw : sqrtTwoAddSeries 0 n < HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2
rw₁ : 0 ≤ 2 + sqrtTwoAddSeries 0 n
⊢ sqrtTwoAddSeries 0 (n + 1) < √(HPow.hPow (α := ℝ) (β := ℕ) 2 2)

Tactic:
rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']

Premises used: lt_sub_iff_add_lt', Real.sqrt_lt_sqrt_iff, Real.sqrtTwoAddSeries
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 n < HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2

Tactic:
(sqrtTwoAddSeries_lt_two n).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
refine : 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2
⊢ sqrtTwoAddSeries 0 n < HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2

Tactic:
refine (sqrtTwoAddSeries_lt_two n).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)

Premises used: add_nonneg, Real.sqrtTwoAddSeries_zero_nonneg, zero_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)

Premises used: add_nonneg, Real.sqrtTwoAddSeries_zero_nonneg, zero_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
rw : √(2 + x.sqrtTwoAddSeries (n + 1)) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
rw₁ : √(2 + (√(2 + x)).sqrtTwoAddSeries n) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
rw₂ rw₃ : √(2 + (√(2 + x)).sqrtTwoAddSeries n) = √(2 + (√(2 + x)).sqrtTwoAddSeries n)
⊢ x.sqrtTwoAddSeries (n + 1 + 1) = (√(2 + x)).sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]

Premises used: Real.sqrtTwoAddSeries
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
h : x ≤ y
n : ℕ
a : x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n

Tactic:
sqrtTwoAddSeries_monotone_left h _
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n

Tactic:
exact sqrtTwoAddSeries_monotone_left h _
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (π / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)) = sqrtTwoAddSeries 0 0 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 1 < HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
⊢ π / HPow.hPow (α := ℝ) 2 (n + 1) < π

Tactic:
have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
⊢ 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
⊢ 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
have C : 0 < π / 2 ^ (n + 1) := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
rw : LE.le (α := ℝ) 0 2
hx : 0 ≤ 2 + sqrtTwoAddSeries 0 n
hc : Ne (α := ℝ) 2 0
hl : -π ≤ π / HPow.hPow (α := ℝ) 2 (n + 1)
hr : π / HPow.hPow (α := ℝ) 2 (n + 1) ≤ π
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]

Premises used: pow_succ, Real.sqrt_mul_self, Real.sqrtTwoAddSeries, Real.cos_half, Real.sqrt_div, div_mul_eq_div_div, one_mul, add_div_eq_mul_add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
linarith₁ : LT.lt (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) 0 2

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Premises used: le_rfl, Real.sqrtTwoAddSeries_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
linarith :
  2 + sqrtTwoAddSeries 0 n < 0 →
    HMul.hMul (α := ℝ) 2 (-1) + (2 + sqrtTwoAddSeries 0 n - 0) + (0 - sqrtTwoAddSeries 0 n) = 0
linarith₁ : 2 + sqrtTwoAddSeries 0 n < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Premises used: le_rfl, Real.sqrtTwoAddSeries_nonneg