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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v ↔ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ = rexp x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sinh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sinh x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n k : ℕ
x✝ : k ∈ range (n + 1)
⊢ 0 ≤ x ^ k / ↑k !

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (sinh ↑x) = sinh ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (sinh ↑x).im = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v ↔ ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 1 + x + x ^ 2 / 2 = ∑ i ∈ range 3, x ^ i / ↑i !

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x + 1 < 1 + x + x ^ 2 / 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 α
u v : α → 𝕜
⊢ u =o[l] v ↔ ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x + 1 ≤ rexp x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cosh x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ rexp x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cosh ↑x) = cosh ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (cosh ↑x).im = 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : x ≤ 0
⊢ 0 < rexp x

Tactic:
by

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

Goal state before:
pp: ⊢ tanh 0 = 0

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ tanh (-x) = -tanh x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ tanh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (tanh ↑x) = tanh ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (tanh ↑x).im = 0

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ 1 < y - x + 1

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ 0 ≤ y - x

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ rexp x < rexp y

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ rexp 0 < rexp x ↔ 0 < x

Tactic:
exp_lt_exp

Goal state after:
x : ℝ
⊢ 0 < x ↔ 0 < x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh x + sinh x = cexp x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ 1 < rexp x ↔ 0 < x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sinh x + cosh x = cexp x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ rexp x < rexp 0 ↔ x < 0

Tactic:
exp_lt_exp

Goal state after:
x : ℝ
⊢ x < 0 ↔ x < 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ rexp x < 1 ↔ x < 0

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cosh x - sinh x = cexp (-x)

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sinh x - cosh x = -cexp (-x)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =O[l] g ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cosh x ^ 2 - sinh x ^ 2 = 1

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range j with n ≤ m, 1 / ↑m.factorial = ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sinh x ^ 2 = cosh x ^ 2 - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
h : u =o[l] fun _x ↦ 1
⊢ Tendsto u l (𝓝 0)

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
⊢ Tendsto u l (𝓝 0)

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
by

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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹ = (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ ↑n.succ ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
⊢ ↑n.factorial * ↑n ≠ 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
⊢ ↑n.succ - 1 = ↑n

Tactic:
by

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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
by

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

Goal state before:
pp: ⊢ sin 0 = 0

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 : ℂ
⊢ sinh (x * I) = sin x * I

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cosh (x * I) = cos x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ tanh (x * I) = tan x * I

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cos (x * I) = cosh x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ I * sin (x * I) = -sinh x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sin (x * I) = sinh x * I

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ tan (x * I) = tanh x * I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n) ≤ ↑n.succ / (↑n.factorial * ↑n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
⊢ 0 < ‖f 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: ⊢ cos 0 = 1

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.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
⊢ ∑ 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))

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.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ IsBigOWith C l f g

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.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ 0 < ‖a‖⁻¹ + 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ sin z = sin ↑z.re * cosh ↑z.im + cos ↑z.re * sinh ↑z.im * I

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ cos z = cos ↑z.re * cosh ↑z.im - sin ↑z.re * sinh ↑z.im * I

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 : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ (‖a‖⁻¹ + 1)⁻¹ < ‖a‖

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 : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ f =O[l] g

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
this : (fun x ↦ x ^ m * x ^ p) =o[𝓝 0] fun x ↦ x ^ m * 1 ^ p
⊢ (fun x ↦ x ^ (m + p)) =o[𝓝 0] fun x ↦ x ^ m

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m n : ℕ
h : m < n
⊢ (fun x ↦ x ^ n) =o[𝓝 0] fun x ↦ x ^ m

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
⊢ (fun x ↦ x ^ n) =o[𝓝 0] fun x ↦ x

Tactic:
by

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

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
⊢ (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ x

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'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖x₀ - x₀‖ ^ n = 0

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'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
by

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

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
m : ℕ
h : 1 < m
⊢ (fun x ↦ ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x ↦ x - x₀

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j with n ≤ m, x ^ m / ↑m.factorial‖ = ‖∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / ↑m.factorial)‖

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.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial) = ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, 1 / ↑m.factorial

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : x ∈ {x | (fun x ↦ ‖f₁ x‖ ≤ c * ‖f₂ x‖) x}
⊢ x ∈ {x | (fun x ↦ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖) x}

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, 1 / ↑m.factorial ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖cexp 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 y : ℂ
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((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.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
⊢ ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'

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 : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x ^ (n + i) / ↑(n + i).factorial‖ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ↑(n + i).factorial

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sin x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (sin ↑x) = sin ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (sin ↑x).im = 0

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cos x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cos ↑x) = cos ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (cos ↑x).im = 0

Tactic:
by

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

Goal state before:
pp: ⊢ tan 0 = 0

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) = -tan x

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (tan ↑x) = tan ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖

Tactic:
exact fun hx => (div_le_iff₀ (norm_pos_iff.2 h₀)).1 (this _ hx)

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (↑x).cot = (↑x).cot

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (tan ↑x).im = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
by

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

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

Tactic:
by

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

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

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
h' : f'' =O[cofinite] g''
C : ℝ
_C₀ : C > 0
hC : ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f'' x‖ ≤ C * ‖g'' x‖
x : α
hx : g'' x = 0
⊢ ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
by

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

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

Tactic:
by

Goal state after: