awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : √3 / 2 / (1 / 2) = √3
⊢ tan (π / 3) = √3

Tactic:
rw [tan_eq_sin_div_cos, sin_pi_div_three, cos_pi_div_three]

Premises used: Real.sin_pi_div_three, Real.cos_pi_div_three, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ √3 / 2 / (1 / 2) = √3

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
rw : 0 < sin x / cos x
⊢ 0 < tan x

Tactic:
rw [tan_eq_sin_div_cos]

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

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 < x
hxp : 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) → 4 * (0 - x) + (2 * x - 1 * π) + (2 * x - -(1 * π)) = 0
linarith₇ : x ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) < x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x

Tactic:
exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)

Premises used: Real.sin_pos_of_pos_of_lt_pi, Real.cos_pos_of_mem_Ioo, And.intro, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 ≤ x
hxp_1 : x ≤ π / 2
h : 0 < x
hxp : x = π / 2
⊢ 0 ≤ tan x

Tactic:
simp [hxp, tan_eq_sin_div_cos]

Premises used: Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
h0x : 0 ≤ x
hxp : x ≤ π / 2
hx0 : 0 = x
h : x < π / 2 ∨ x = π / 2
⊢ 0 ≤ tan x

Tactic:
simp [hx0.symm]

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

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
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 * x)) = 0
⊢ -x < π / 2

Tactic:
linarith [pi_pos]

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

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
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 * x)) = 0
⊢ -x ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
rw : 0 < sin (y - x)
⊢ tan x < tan y

Tactic:
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos,
    div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy), mul_comm, ← sub_pos, ← sin_sub]

Premises used: sub_pos, Real.sin_sub, Real.cos_pos_of_mem_Ioo, mul_comm, div_lt_div_iff₀, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
linarith : π ≤ y - x → 2 / 2 = 1
linarith₁ : π ≤ y - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π ≤ y - x → GT.gt (α := ℝ) 2 0
linarith₃ : π ≤ y - x → 2 / 2 = 1
linarith₄ : π ≤ y - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π ≤ y - x → GT.gt (α := ℝ) 2 0
linarith₆ : π ≤ y - x → 2 * (π - (y - x)) + (-(1 * π) - 2 * x) + (2 * y - 1 * π) = 0
linarith₇ : π ≤ y - x → GT.gt (α := ℝ) 2 0
⊢ y - x < π

Tactic:
linarith [hx.1, hy.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ 0 < sin (y - x)

Tactic:
exact sin_pos_of_pos_of_lt_pi (sub_pos.2 hlt) <| by linarith [hx.1, hy.2]

Premises used: Iff.mpr, sub_pos, 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
⊢ tan x < tan y

Tactic:
strictMonoOn_tan ⟨hx₁, hxy.trans hy₂⟩ ⟨hx₁.trans hxy, hy₂⟩ hxy

Premises used: And.intro, LT.lt.trans, Real.strictMonoOn_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
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) → 4 * (0 - x) + (2 * y - 1 * π) + 2 * (x - y) + (2 * x - -(1 * π)) = 0
linarith₇ : x ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
linarith₈ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ InjOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
strictMonoOn_tan.injOn

Premises used: StrictMonoOn.injOn, Real.strictMonoOn_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x y : ℝ
hx₁ : -(π / 2) < x
hx₂ : x < π / 2
hy₁ : -(π / 2) < y
hy₂ : y < π / 2
hxy : tan x = tan y
⊢ x = y

Tactic:
injOn_tan ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩ hxy

Premises used: Real.injOn_tan, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic tan π

Tactic:
simpa only [Function.Periodic, tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic

Premises used: Function.Antiperiodic.div, Real.sin_antiperiodic, Function.Periodic, Real.cos_antiperiodic, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : tan 0 = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ tan π = 0

Tactic:
rw [tan_periodic.eq, tan_zero]

Premises used: Real.tan_periodic, Function.Periodic.eq, Real.tan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ tan (x + π) = tan x

Tactic:
tan_periodic x

Premises used: Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ tan (x - π) = tan x

Tactic:
tan_periodic.sub_eq x

Premises used: Real.tan_periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ tan (π - x) = -tan x

Tactic:
tan_neg x ▸ tan_periodic.sub_eq'

Premises used: Real.tan_neg, Eq.rec, Real.tan_periodic, Function.Periodic.sub_eq'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
rw : sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
rw₁ : sin (π / 2 - x) / cos (π / 2 - x) = (sin x / cos x)⁻¹
rw₂ : sin (π / 2 - x) / cos (π / 2 - x) = cos x / sin x
rw₃ : cos x / cos (π / 2 - x) = cos x / sin x
rw₄ rw₅ : cos x / sin x = cos x / sin x
⊢ tan (π / 2 - x) = (tan x)⁻¹

Tactic:
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]

Premises used: Real.sin_pi_div_two_sub, inv_div, Real.cos_pi_div_two_sub, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ tan ((↑n : ℝ) * π) = 0

Tactic:
tan_zero ▸ tan_periodic.nat_mul_eq n

Premises used: Eq.rec, Function.Periodic.nat_mul_eq, Real.tan_periodic, Real.tan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ tan ((↑n : ℝ) * π) = 0

Tactic:
tan_zero ▸ tan_periodic.int_mul_eq n

Premises used: Eq.rec, Real.tan_periodic, Function.Periodic.int_mul_eq, Real.tan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ tan (x + (↑n : ℝ) * π) = tan x

Tactic:
tan_periodic.nat_mul n x

Premises used: Function.Periodic.nat_mul, Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ tan (x + (↑n : ℝ) * π) = tan x

Tactic:
tan_periodic.int_mul n x

Premises used: Function.Periodic.int_mul, Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ tan (x - (↑n : ℝ) * π) = tan x

Tactic:
tan_periodic.sub_nat_mul_eq n

Premises used: Real.tan_periodic, Function.Periodic.sub_nat_mul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ tan (x - (↑n : ℝ) * π) = tan x

Tactic:
tan_periodic.sub_int_mul_eq n

Premises used: Function.Periodic.sub_int_mul_eq, Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ tan ((↑n : ℝ) * π - x) = -tan x

Tactic:
tan_neg x ▸ tan_periodic.nat_mul_sub_eq n

Premises used: Real.tan_neg, Eq.rec, Function.Periodic.nat_mul_sub_eq, Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ tan ((↑n : ℝ) * π - x) = -tan x

Tactic:
tan_neg x ▸ tan_periodic.int_mul_sub_eq n

Premises used: Real.tan_neg, Eq.rec, Real.tan_periodic, Function.Periodic.int_mul_sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Tendsto sin (𝓝[<] (π / 2)) (𝓝 (sin (π / 2)))

Tactic:
continuous_sin.continuousWithinAt.tendsto

Premises used: Real.continuous_sin, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : 1 = sin (π / 2)
⊢ Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)

Tactic:
convert! continuous_sin.continuousWithinAt.tendsto

Premises used: Real.continuous_sin, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 1 = sin (π / 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h1 : Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)
h2 : ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 (cos (π / 2)))

Tactic:
continuous_cos.continuousWithinAt.tendsto

Premises used: Real.continuous_cos, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : 0 = cos (π / 2)
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)

Tactic:
convert! continuous_cos.continuousWithinAt.tendsto

Premises used: Real.continuous_cos, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 0 = cos (π / 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : ∀ (x : ℝ) (hx : x ∈ Ioo (-(π / 2)) (π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)

Tactic:
filter_upwards [Ioo_mem_nhdsLT (neg_lt_self pi_div_two_pos)] with x hx

Premises used: Real.pi_div_two_pos, Ioo_mem_nhdsLT, neg_lt_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)

Tactic:
cos_pos_of_mem_Ioo hx

Premises used: Set.Ioi, Set.Mem, setOf, Real.cos_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)

Tactic:
exact cos_pos_of_mem_Ioo hx

Premises used: Real.cos_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ cos⁻¹ x * sin x) (𝓝[<] (π / 2)) atTop

Tactic:
tendsto_cos_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul_pos zero_lt_one
      tendsto_sin_pi_div_two

Premises used: Real.tendsto_cos_pi_div_two, zero_lt_one, Filter.Tendsto.atTop_mul_pos, Filter.Tendsto.inv_tendsto_nhdsGT_zero, Real.tendsto_sin_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : tan = fun (x : ℝ) ↦ cos⁻¹ x * sin x
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Tactic:
convert!
    tendsto_cos_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul_pos zero_lt_one
      tendsto_sin_pi_div_two using 1

Premises used: Real.tendsto_cos_pi_div_two, zero_lt_one, Filter.Tendsto.atTop_mul_pos, Filter.Tendsto.inv_tendsto_nhdsGT_zero, Real.tendsto_sin_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ tan = fun (x : ℝ) ↦ cos⁻¹ x * sin x

Tactic:
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]

Premises used: div_eq_inv_mul, Pi.inv_apply, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (sin (-(π / 2))))

Tactic:
continuous_sin.continuousWithinAt.tendsto

Premises used: Real.continuous_sin, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : -1 = sin (-(π / 2))
⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))

Tactic:
convert! continuous_sin.continuousWithinAt.tendsto using 2

Premises used: Real.continuous_sin, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ -1 = sin (-(π / 2))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h1 : Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)
h2 : ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 (cos (-(π / 2))))

Tactic:
continuous_cos.continuousWithinAt.tendsto

Premises used: Real.continuous_cos, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : 0 = cos (-(π / 2))
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)

Tactic:
convert! continuous_cos.continuousWithinAt.tendsto

Premises used: Real.continuous_cos, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 0 = cos (-(π / 2))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : ∀ (x : ℝ) (hx : x ∈ Ioo (-(π / 2)) (π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)

Tactic:
filter_upwards [Ioo_mem_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx

Premises used: Real.pi_div_two_pos, neg_lt_self, Ioo_mem_nhdsGT
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ LT.lt (α := ℝ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : tan = fun (x : ℝ) ↦ cos⁻¹ x * sin x
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Tactic:
convert!
    tendsto_cos_neg_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul_neg (by simp)
      tendsto_sin_neg_pi_div_two using 1

Premises used: Real.tendsto_cos_neg_pi_div_two, Real.tendsto_sin_neg_pi_div_two, Filter.Tendsto.atTop_mul_neg, Filter.Tendsto.inv_tendsto_nhdsGT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : sin z = 0 ↔ cos z * cos z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : sin z = 0 ↔ cos z * cos z = sin z * sin z + cos z * cos z
rw₆ : ℂ
rw₇ : sin z = 0 ↔ sin z * sin z = 0
rw₈ : sin z = 0 ↔ sin z = 0 ∨ sin z = 0
rw₉ rw₁₀ : sin z = 0 ↔ sin z = 0
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -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, Complex.sin_sq_add_cos_sq, mul_self_eq_one_iff, or_self, right_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : cos z = 0 ↔ sin z * sin z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : cos z = 0 ↔ sin z * sin z = sin z * sin z + cos z * cos z
rw₆ : ℂ
rw₇ : cos z = 0 ↔ cos z * cos z = 0
rw₈ : cos z = 0 ↔ cos z = 0 ∨ cos z = 0
rw₉ rw₁₀ : cos z = 0 ↔ cos z = 0
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -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, Complex.sin_sq_add_cos_sq, mul_self_eq_one_iff, or_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : cos ((↑π : ℂ) / 2) = cos (↑(π / 2) : ℂ)
⊢ cos ((↑π : ℂ) / 2) = (↑(Real.cos (π / 2)) : ℂ)

Tactic:
rw [ofReal_cos]

Premises used: Complex.ofReal_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos ((↑π : ℂ) / 2) = cos (↑(π / 2) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ (↑(Real.cos (π / 2)) : ℂ) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : sin ((↑π : ℂ) / 2) = sin (↑(π / 2) : ℂ)
⊢ sin ((↑π : ℂ) / 2) = (↑(Real.sin (π / 2)) : ℂ)

Tactic:
rw [ofReal_sin]

Premises used: Complex.ofReal_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin ((↑π : ℂ) / 2) = sin (↑(π / 2) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ (↑(Real.sin (π / 2)) : ℂ) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : (↑0 : ℂ) = 0
⊢ sin (↑π : ℂ) = 0

Tactic:
rw [← ofReal_sin, Real.sin_pi]

Premises used: Real.sin_pi, Complex.ofReal_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ (↑0 : ℂ) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : (↑(-1) : ℂ) = -1
⊢ cos (↑π : ℂ) = -1

Tactic:
rw [← ofReal_cos, Real.cos_pi]

Premises used: Complex.ofReal_cos, Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ (↑(-1) : ℂ) = -1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (2 * (↑π : ℂ)) = 0

Tactic:
simp [two_mul, sin_add]

Premises used: two_mul, Complex.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (2 * (↑π : ℂ)) = 1

Tactic:
simp [two_mul, cos_add]

Premises used: two_mul, Complex.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic sin (↑π : ℂ)

Tactic:
simp [sin_add]

Premises used: Complex.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic sin (2 * (↑π : ℂ))

Tactic:
sin_antiperiodic.periodic_two_mul

Premises used: Function.Antiperiodic.periodic_two_mul, Complex.sin_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (x + (↑π : ℂ)) = -sin x

Tactic:
sin_antiperiodic x

Premises used: Complex.sin_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (x + 2 * (↑π : ℂ)) = sin x

Tactic:
sin_periodic x

Premises used: Complex.sin_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (x - (↑π : ℂ)) = -sin x

Tactic:
sin_antiperiodic.sub_eq x

Premises used: Function.Antiperiodic.sub_eq, Complex.sin_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (x - 2 * (↑π : ℂ)) = sin x

Tactic:
sin_periodic.sub_eq x

Premises used: Complex.sin_periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin ((↑π : ℂ) - x) = sin x

Tactic:
neg_neg (sin x) ▸ sin_neg x ▸ sin_antiperiodic.sub_eq'

Premises used: Complex.sin, Eq.rec, Function.Antiperiodic.sub_eq', neg_neg, Complex.sin_antiperiodic, Complex.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (2 * (↑π : ℂ) - x) = -sin x

Tactic:
sin_neg x ▸ sin_periodic.sub_eq'

Premises used: Eq.rec, Complex.sin_periodic, Function.Periodic.sub_eq', Complex.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ sin ((↑n : ℂ) * (↑π : ℂ)) = 0

Tactic:
sin_antiperiodic.nat_mul_eq_of_eq_zero sin_zero n

Premises used: Complex.sin_antiperiodic, Function.Antiperiodic.nat_mul_eq_of_eq_zero, Complex.sin_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ sin ((↑n : ℂ) * (↑π : ℂ)) = 0

Tactic:
sin_antiperiodic.int_mul_eq_of_eq_zero sin_zero n

Premises used: Complex.sin_antiperiodic, Function.Antiperiodic.int_mul_eq_of_eq_zero, Complex.sin_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ sin (x + (↑n : ℂ) * (2 * (↑π : ℂ))) = sin x

Tactic:
sin_periodic.nat_mul n x

Premises used: Function.Periodic.nat_mul, Complex.sin_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ sin (x + (↑n : ℂ) * (2 * (↑π : ℂ))) = sin x

Tactic:
sin_periodic.int_mul n x

Premises used: Function.Periodic.int_mul, Complex.sin_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ sin (x - (↑n : ℂ) * (2 * (↑π : ℂ))) = sin x

Tactic:
sin_periodic.sub_nat_mul_eq n

Premises used: Complex.sin_periodic, Function.Periodic.sub_nat_mul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ sin (x - (↑n : ℂ) * (2 * (↑π : ℂ))) = sin x

Tactic:
sin_periodic.sub_int_mul_eq n

Premises used: Function.Periodic.sub_int_mul_eq, Complex.sin_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ sin ((↑n : ℂ) * (2 * (↑π : ℂ)) - x) = -sin x

Tactic:
sin_neg x ▸ sin_periodic.nat_mul_sub_eq n

Premises used: Eq.rec, Function.Periodic.nat_mul_sub_eq, Complex.sin_periodic, Complex.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ sin ((↑n : ℂ) * (2 * (↑π : ℂ)) - x) = -sin x

Tactic:
sin_neg x ▸ sin_periodic.int_mul_sub_eq n

Premises used: Eq.rec, Complex.sin_periodic, Complex.sin_neg, Function.Periodic.int_mul_sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic cos (↑π : ℂ)

Tactic:
simp [cos_add]

Premises used: Complex.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic cos (2 * (↑π : ℂ))

Tactic:
cos_antiperiodic.periodic_two_mul

Premises used: Complex.cos_antiperiodic, Function.Antiperiodic.periodic_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (x + (↑π : ℂ)) = -cos x

Tactic:
cos_antiperiodic x

Premises used: Complex.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (x + 2 * (↑π : ℂ)) = cos x

Tactic:
cos_periodic x

Premises used: Complex.cos_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (x - (↑π : ℂ)) = -cos x

Tactic:
cos_antiperiodic.sub_eq x

Premises used: Complex.cos_antiperiodic, Function.Antiperiodic.sub_eq