mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 + sin x ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = cos x ^ 2 - sin x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = 2 * cos x ^ 2 - 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = 1 - 2 * sin x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E : Type u_3
E'' : Type u_9
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup E''
f : ℕ → E
g'' : ℕ → E''
h : f =O[atTop] g''
⊢ f =O[cofinite] g''

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin (2 * x) = 2 * sin x * cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 = 1 / 2 + cos (2 * x) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 = 1 - cos x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ (x : ℕ), g x = 0 → f x = 0
⊢ f =O[atTop] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ (1 + tan x ^ 2) * cos x ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
inst✝ : NormedAddCommGroup E''
f : ℕ → E''
⊢ (∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖1‖) ↔ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1‖ = ‖cexp x - ∑ m ∈ range 1, x ^ m / ↑m.factorial‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 1 * (↑(Nat.succ 1) * (↑(Nat.factorial 1) * ↑1)⁻¹) = 2 * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1 - x‖ = ‖cexp x - ∑ m ∈ range 2, x ^ m / ↑m.factorial‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 * (↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹) ≤ ‖x‖ ^ 2 * 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cexp (x + y * I) = cexp x * (cos y + sin y * I)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 * 1 = ‖x‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cexp x = cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖Real.exp x - 1 - x‖ = ‖↑(Real.exp x) - 1 - ↑x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑(Real.exp x) - 1 - ↑x‖ = ‖cexp ↑x - 1 - ↑x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (cexp x).re = Real.exp x.re * Real.cos x.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑x‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑x‖ ^ 2 = ‖x‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (cexp x).im = Real.exp x.re * Real.sin x.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cexp (↑x * I)).re = Real.cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cexp (↑x * I)).im = Real.sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cexp (↑x * I) = ↑(Real.cos x) + ↑(Real.sin x) * I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: n : ℕ
z : ℂ
⊢ (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cos x - (1 - x ^ 2 / 2)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial) / 2‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤
    ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ range j with n ≤ k, x ^ k / ↑k.factorial‖ ≤ ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / ↑k.factorial
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤
    ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖-x * I‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
⊢ f =O[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 4

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
x : α
⊢ 0 ≤ C * ‖g' x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x * I‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x ↦ f x i) g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =O[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =O[l] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 ≤
    ‖x‖ ^ 4 * (5 / 96)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =o[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =o[l] g'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖sin x - (x - x ^ 3 / 6)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → E
g : α → F
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 5

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ Ico n j, x ^ m / ↑m.factorial‖ = ‖∑ m ∈ Ico n j, x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
this :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) +
      (∑ i ∈ range K, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) -
        ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) <
    ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)
⊢ ∑ i ∈ range K, abv (f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖-x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2 +
      ‖x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖-x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2 +
      ‖x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2 =
    ‖x‖ ^ 5 / 100

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin (-x) = -sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(sin (x + y)) = ↑(sin x * cos y + cos x * sin y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos (-x) = cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos |x| = cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos (x + y)) = ↑(cos x * cos y - sin x * sin y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ sin (x - y) = sin x * cos y - cos x * sin y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ cos (x - y) = cos x * cos y + sin x * sin y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(sin x + sin y) = ↑(2 * sin ((x + y) / 2) * cos ((x - y) / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(sin x - sin y) = ↑(2 * sin ((x - y) / 2) * cos ((x + y) / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos x + cos y) = ↑(2 * cos ((x + y) / 2) * cos ((x - y) / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos x - cos y) = ↑(-2 * sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial) = ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / ↑m.factorial

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * sin y = cos (x - y) - cos (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * cos x * cos y = cos (x - y) + cos (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / ↑m.factorial ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
gcongr
      refine Real.sum_le_exp_of_nonneg ?_ _
      exact norm_nonneg _

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / ↑m.factorial ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * cos y = sin (x - y) + sin (x + y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(tan x) = ↑(sin x / cos x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑x.cot = ↑(cos x / sin x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
⊢ tan x * cos x = sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(tan x)⁻¹ = ↑x.cot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑x.cot⁻¹ = ↑(tan x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ tan (-x) = -tan x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(sin x ^ 2 + cos x ^ 2) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 + sin x ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin x * sin x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x * cos x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cos (2 * x)) = ↑(2 * cos x ^ 2 - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cos (2 * x)) = ↑(cos x ^ 2 - sin x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cos (2 * x)) = ↑(1 - 2 * sin x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsBigOWith c l (fun x ↦ f x * g x) h ↔ IsBigOWith c l g fun x ↦ h x / f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(sin (2 * x)) = ↑(2 * sin x * cos x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cos x ^ 2) = ↑(1 / 2 + cos (2 * x) / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 = 1 / 2 - cos (2 * x) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ |sin x| = √(1 - cos x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ |cos x| = √(1 - sin x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
this : Complex.cos ↑x ≠ 0
⊢ ↑(1 + tan x ^ 2)⁻¹ = ↑(cos x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x ↦ f x * g x) =O[l] h ↔ g =O[l] fun x ↦ h x / f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
⊢ tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ (√(1 + tan x ^ 2))⁻¹ = cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ |x| = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ |x| ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(sinh x) = ↑((rexp x - rexp (-x)) / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x ↦ f x * g x) =o[l] h ↔ g =o[l] fun x ↦ h x / f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh (-x) = -sinh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Tactic:
by

Goal state after: