awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ arctan (f x)) s x = 1 / (1 + HPow.hPow (β := ℕ) (f x) 2) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.arctan.derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
f : ℝ → ℝ
x : ℝ
hc : DifferentiableAt ℝ f x
⊢ deriv (fun (x : ℝ) ↦ arctan (f x)) x = 1 / (1 + HPow.hPow (β := ℕ) (f x) 2) * deriv f x

Tactic:
hc.hasDerivAt.arctan.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.arctan, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ Real.arctan (f x)) ((1 / (1 + HPow.hPow (β := ℕ) (f x) 2)) • f') x

Tactic:
(hasStrictDerivAt_arctan (f x)).comp_hasStrictFDerivAt x hf

Premises used: Real.arctan, HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : E) ↦ Real.arctan (f x)) ((1 / (1 + HPow.hPow (β := ℕ) (f x) 2)) • f') x

Tactic:
(hasDerivAt_arctan (f x)).comp_hasFDerivAt x hf

Premises used: Real.arctan, Real.hasDerivAt_arctan, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ Real.arctan (f x)) ((1 / (1 + HPow.hPow (β := ℕ) (f x) 2)) • f') s x

Tactic:
(hasDerivAt_arctan (f x)).comp_hasFDerivWithinAt x hf

Premises used: Real.arctan, HasDerivAt.comp_hasFDerivWithinAt, Real.hasDerivAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
hxs : UniqueDiffWithinAt ℝ s x
⊢ fderivWithin ℝ (fun (x : E) ↦ arctan (f x)) s x =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (1 / (1 + HPow.hPow (β := ℕ) (f x) 2)) (fderivWithin ℝ f s x)

Tactic:
hf.hasFDerivWithinAt.arctan.fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.arctan, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hc : DifferentiableAt ℝ f x
⊢ fderiv ℝ (fun (x : E) ↦ arctan (f x)) x =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (1 / (1 + HPow.hPow (β := ℕ) (f x) 2)) (fderiv ℝ f x)

Tactic:
hc.hasFDerivAt.arctan.fderiv

Premises used: HasFDerivAt.arctan, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ Real.arctan (f x)) s x

Tactic:
hf.hasFDerivWithinAt.arctan.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.arctan, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hc : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ Real.arctan (f x)) x

Tactic:
hc.hasFDerivAt.arctan.differentiableAt

Premises used: HasFDerivAt.arctan, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
hc : DifferentiableOn ℝ f s
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ Real.arctan (f x)) s

Tactic:
fun x h => (hc x h).arctan

Premises used: DifferentiableWithinAt.arctan, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hc : Differentiable ℝ f
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ Real.arctan (f x)

Tactic:
fun x => (hc x).arctan

Premises used: Differentiable, DifferentiableAt.arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
n : ℕ∞
h : ContDiffAt ℝ (↑n : WithTop ℕ∞) f x
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ Real.arctan (f x)) x

Tactic:
contDiff_arctan.contDiffAt.comp x h

Premises used: Real.arctan, Real.contDiff_arctan, ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : ℕ∞
h : ContDiff ℝ (↑n : ℕ∞ω) f
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : E) ↦ Real.arctan (f x)

Tactic:
contDiff_arctan.comp h

Premises used: Real.arctan, ContDiff.comp, Real.contDiff_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
n : ℕ∞
h : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) f s x
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ Real.arctan (f x)) s x

Tactic:
contDiff_arctan.comp_contDiffWithinAt h

Premises used: ContDiff.comp_contDiffWithinAt, Real.arctan, Real.contDiff_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
n : ℕ∞
h : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
⊢ ContDiffOn ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ Real.arctan (f x)) s

Tactic:
contDiff_arctan.comp_contDiffOn h

Premises used: ContDiff.comp_contDiffOn, Real.arctan, Real.contDiff_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous (Y := ℂ) fun (z : ℂ) ↦ (cexp (-z * I) - cexp (z * I)) * I / 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
s : Set ℂ
⊢ ContinuousOn sin s

Tactic:
continuous_sin.continuousOn

Premises used: Continuous.continuousOn, Complex.continuous_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous (Y := ℂ) fun (z : ℂ) ↦ (cexp (z * I) + cexp (-z * I)) / 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
s : Set ℂ
⊢ ContinuousOn cos s

Tactic:
continuous_cos.continuousOn

Premises used: Continuous.continuousOn, Complex.continuous_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous (Y := ℂ) fun (z : ℂ) ↦ (cexp z - cexp (-z)) / 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous (Y := ℂ) fun (z : ℂ) ↦ (cexp z + cexp (-z)) / 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous sin

Tactic:
Complex.continuous_re.comp (Complex.continuous_sin.comp Complex.continuous_ofReal)

Premises used: Complex.continuous_sin, Complex.continuous_re, Continuous.comp, Complex.continuous_ofReal, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
s : Set ℝ
⊢ ContinuousOn sin s

Tactic:
continuous_sin.continuousOn

Premises used: Continuous.continuousOn, Real.continuous_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous cos

Tactic:
Complex.continuous_re.comp (Complex.continuous_cos.comp Complex.continuous_ofReal)

Premises used: Real.cos, Complex.continuous_re, Continuous.comp, Complex.continuous_cos, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
s : Set ℝ
⊢ ContinuousOn cos s

Tactic:
continuous_cos.continuousOn

Premises used: Continuous.continuousOn, Real.continuous_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous sinh

Tactic:
Complex.continuous_re.comp (Complex.continuous_sinh.comp Complex.continuous_ofReal)

Premises used: Complex.continuous_re, Continuous.comp, Real.sinh, Complex.continuous_sinh, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Continuous cosh

Tactic:
Complex.continuous_re.comp (Complex.continuous_cosh.comp Complex.continuous_ofReal)

Premises used: Complex.continuous_re, Continuous.comp, Complex.continuous_cosh, Complex.continuous_ofReal, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ LE.le (α := ℝ) 1 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw :
  cos (Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero) = 0
⊢ cos (π / 2) = 0

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]

Premises used: Real.pi, mul_div_cancel_left₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero) = 0

Tactic:
(Classical.choose_spec exists_cos_eq_zero).2

Premises used: Set.Mem, Classical.choose_spec, And.right, Real.exists_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero) = 0

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).2

Premises used: Classical.choose_spec, And.right, Real.exists_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : 1 ≤ Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero
⊢ 1 ≤ π / 2

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]

Premises used: Real.pi, mul_div_cancel_left₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 1 ≤ Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero

Tactic:
(Classical.choose_spec exists_cos_eq_zero).1.1

Premises used: Set.Mem, Classical.choose_spec, And.left, Real.exists_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 1 ≤ Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).1.1

Premises used: Classical.choose_spec, And.left, Real.exists_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero ≤ 2
⊢ π / 2 ≤ 2

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]

Premises used: Real.pi, mul_div_cancel_left₀, two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero ≤ 2

Tactic:
(Classical.choose_spec exists_cos_eq_zero).1.2

Premises used: Set.Mem, Classical.choose_spec, And.right, And.left, Real.exists_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero ≤ 2

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).1.2

Premises used: Classical.choose_spec, And.right, And.left, Real.exists_cos_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : 1 ≤ π / 2
⊢ 2 / 2 ≤ π / 2

Tactic:
rw [div_self two_ne_zero]

Premises used: two_ne_zero, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 1 ≤ π / 2

Tactic:
one_le_pi_div_two

Premises used: Real.one_le_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 1 ≤ π / 2

Tactic:
exact one_le_pi_div_two

Premises used: Real.one_le_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 2 = 4 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 0 ≤ π

Tactic:
pi_pos.le

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ π ≠ 0

Tactic:
pi_pos.ne'

Premises used: Real.pi_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 0 < π / 2

Tactic:
half_pos pi_pos

Premises used: half_pos, Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
linarith : 2 * π ≤ 0 → 2 * π - 0 + 2 * (0 - π) = 0
linarith₁ : 2 * π ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 2 * π

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ (↑pi : ℝ) = π

Tactic:
rfl

Premises used: Real.pi, NNReal.toReal, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 0 < pi

Tactic:
mod_cast Real.pi_pos

Premises used: Real.pi, congrArg, cast, Real.pi_pos, LT.lt, congrFun', NNReal.pi, Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ pi ≠ 0

Tactic:
pi_pos.ne'

Premises used: NNReal.pi_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : sin (π / 2) * 0 + 0 * sin (π / 2) = 0
⊢ sin π = 0

Tactic:
rw [← mul_div_cancel_left₀ π two_ne_zero, two_mul, add_div, sin_add, cos_pi_div_two]

Premises used: Real.pi, two_mul, Real.cos_pi_div_two, mul_div_cancel_left₀, Real.sin_add, two_ne_zero, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : 2 * HPow.hPow (α := ℝ) (β := ℕ) 0 2 - 1 = -1
⊢ cos π = -1

Tactic:
rw [← mul_div_cancel_left₀ π two_ne_zero, mul_div_assoc, cos_two_mul, cos_pi_div_two]

Premises used: Real.pi, mul_div_assoc, Real.cos_pi_div_two, mul_div_cancel_left₀, two_ne_zero, Real.cos_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 2 * HPow.hPow (α := ℝ) (β := ℕ) 0 2 - 1 = -1

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

Tactic:
simp [two_mul, sin_add]

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

Tactic:
simp [two_mul, cos_add]

Premises used: two_mul, Real.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic sin π

Tactic:
simp [sin_add]

Premises used: Real.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, Real.sin_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin (x + π) = -sin x

Tactic:
sin_antiperiodic x

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

Tactic:
sin_periodic x

Premises used: Real.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, Real.sin_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin (x - 2 * π) = sin x

Tactic:
sin_periodic.sub_eq x

Premises used: Real.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: Real.sin_antiperiodic, Eq.rec, Function.Antiperiodic.sub_eq', neg_neg, Real.sin_neg, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ sin (2 * π - x) = -sin x

Tactic:
sin_neg x ▸ sin_periodic.sub_eq'

Premises used: Real.sin_periodic, Eq.rec, Real.sin_neg, Function.Periodic.sub_eq'
-- 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: Real.sin_antiperiodic, Real.sin_zero, Function.Antiperiodic.nat_mul_eq_of_eq_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: Real.sin_antiperiodic, Real.sin_zero, Function.Antiperiodic.int_mul_eq_of_eq_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: Real.sin_periodic, Function.Periodic.nat_mul
-- 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, Real.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: Real.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: Real.sin_periodic, Function.Periodic.sub_int_mul_eq
-- 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: Real.sin_periodic, Eq.rec, Real.sin_neg, Function.Periodic.nat_mul_sub_eq
-- 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: Real.sin_periodic, Eq.rec, Real.sin_neg, Function.Periodic.int_mul_sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℤ
⊢ sin (x + (↑n : ℝ) * π) = HPow.hPow (α := ℝ) (-1) n * sin x

Tactic:
n.cast_negOnePow ℝ ▸ sin_antiperiodic.add_int_mul_eq n

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

Tactic:
sin_antiperiodic.add_nat_mul_eq n

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

Tactic:
n.cast_negOnePow ℝ ▸ sin_antiperiodic.sub_int_mul_eq n

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

Tactic:
sin_antiperiodic.sub_nat_mul_eq n

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

Tactic:
simpa only [sin_neg, mul_neg, Int.cast_negOnePow] using sin_antiperiodic.int_mul_sub_eq n

Premises used: Real.sin_antiperiodic, Int.cast_negOnePow, Real.sin_neg, Function.Antiperiodic.int_mul_sub_eq, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ sin ((↑n : ℝ) * π - x) = -(HPow.hPow (α := ℝ) (-1) n * sin x)

Tactic:
simpa only [sin_neg, mul_neg] using sin_antiperiodic.nat_mul_sub_eq n

Premises used: Real.sin_antiperiodic, Function.Antiperiodic.nat_mul_sub_eq, Real.sin_neg, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic cos π

Tactic:
simp [cos_add]

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

Tactic:
cos_antiperiodic.periodic_two_mul

Premises used: Function.Antiperiodic.periodic_two_mul, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
k : ℤ
⊢ |cos ((↑k : ℝ) * π)| = 1

Tactic:
simp [abs_cos_eq_sqrt_one_sub_sin_sq]

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

Tactic:
cos_antiperiodic x

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

Tactic:
cos_periodic x

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

Tactic:
cos_antiperiodic.sub_eq x

Premises used: Function.Antiperiodic.sub_eq, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ cos (x - 2 * π) = cos x

Tactic:
cos_periodic.sub_eq x

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

Tactic:
cos_neg x ▸ cos_antiperiodic.sub_eq'

Premises used: Eq.rec, Function.Antiperiodic.sub_eq', Real.cos_neg, Real.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
⊢ cos (2 * π - x) = cos x

Tactic:
cos_neg x ▸ cos_periodic.sub_eq'

Premises used: Eq.rec, Function.Periodic.sub_eq', Real.cos_neg, Real.cos_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℝ) * (2 * π)) = 1

Tactic:
(cos_periodic.nat_mul_eq n).trans cos_zero

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

Tactic:
(cos_periodic.int_mul_eq n).trans cos_zero

Premises used: Function.Periodic.int_mul_eq, Real.cos_periodic, Real.cos_zero, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℝ
n : ℕ
⊢ cos (x + (↑n : ℝ) * (2 * π)) = cos x

Tactic:
cos_periodic.nat_mul n x

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

Tactic:
cos_periodic.int_mul n x

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

Tactic:
cos_periodic.sub_nat_mul_eq n

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

Tactic:
cos_periodic.sub_int_mul_eq n

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

Tactic:
cos_neg x ▸ cos_periodic.nat_mul_sub_eq n

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

Tactic:
cos_neg x ▸ cos_periodic.int_mul_sub_eq n

Premises used: Eq.rec, Real.cos_neg, Real.cos_periodic, Function.Periodic.int_mul_sub_eq