mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖) ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℂ
⊢ sin (2 * x) * cos x + cos (2 * x) * sin x = (2 + 1) * sin x - 4 * sin x ^ 3
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).im = Real.exp x.re * Real.sin x.im
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: n : ℕ
z : ℂ
⊢ cexp (↑n * (z * I)) = cexp (↑n * (z * I))

Tactic:
]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
]

Goal state after:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.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:
]

Goal state after:
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
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: 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

Tactic:
]

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
⊢ ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 ≤
    ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2

Tactic:
]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
]

Goal state after:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖
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
⊢ (∀ᶠ (a₀ : α) in atTop, ∃ b, ∀ (a : α), a₀ ≤ a → ‖f a‖ ≤ b * ‖g a‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Tactic:
]

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:
]

Goal state after:
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
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)) <
    ε
⊢ ∑ i ∈ range K, abv (f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε

Tactic:
simpa [abv_mul abv] using this

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

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

Tactic:
]

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ Ico n j, x ^ k / ↑k.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
]

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ m / ↑m.factorial

Tactic:
]

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 * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2 +
      ‖x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2

Tactic:
]

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
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hac
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ Ico n j
⊢ ‖x‖ ^ (i - n) ≤ ‖x‖ ^ (i - n)

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
x : α
hx : f x ≠ 0
⊢ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
x : ℝ
⊢ sin x ^ 2 ≤ sin x ^ 2 + cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ cos x ^ 2 ≤ sin x ^ 2 + cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

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

Tactic:
]

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
⊢ (∃ c, IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∃ c, IsBigOWith c l g fun x ↦ h x / f x

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c, IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∃ c, IsBigOWith c l g fun x ↦ h x / f x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ √(cos x ^ 2) = √(cos x ^ 2)

Tactic:
]

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

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

Tactic:
]

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
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g fun x ↦ h x / f x

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g fun x ↦ h x / f x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cos (3 * x)) = ↑(4 * cos x ^ 3 - 3 * cos x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cos (3 * x)) = ↑(4 * cos x ^ 3 - 3 * cos x)
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:
]

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ x ≤ 1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cexp ↑x).re + (cexp (-↑x)).re = (cexp ↑x).re + (cexp (-↑x)).re

Tactic:
]

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 : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g

Tactic:
]

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
]

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x y : ℝ
⊢ ↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x y : ℝ
⊢ ↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)
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
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P

Tactic:
]

Goal state after:
α : 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
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) = (rexp x - rexp (-x)) / (rexp x + rexp (-x))

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ cosh x + sinh x = rexp x

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ rexp x = rexp x

Tactic:
]

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

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cosh x - sinh x) = ↑(rexp (-x))
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cosh x - sinh x) = ↑(rexp (-x))
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cosh x ^ 2 - sinh x ^ 2) = ↑1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cosh x ^ 2 - sinh x ^ 2) = ↑1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(sinh x ^ 2) = ↑(cosh x ^ 2 - 1)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1

Tactic:
]

Goal state after:
x : ℝ
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))

Tactic:
]

Goal state after:
x : ℝ
⊢ -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))