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

Goal state before:
pp: x : ℝ
⊢ cosh x * 2 = rexp x + rexp (-x)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

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:
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ↑(tanh x) = ↑(sinh x / cosh x)

Tactic:
by

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

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ sinh x - cosh x = -rexp (-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.Trigonometric

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

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.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 : ℝ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ tanh x < 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ -1 < tanh x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 5 / 100

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
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P)) < ε / (2 * P) * P

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |x| ^ 4 * (5 / 96) + x ^ 2 / 2 ≤ 1 * (5 / 96) + 1 / 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ x ^ 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ 1 * (5 / 96) + 1 / 2 < 1

Tactic:
by

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

Goal state before:
pp: x r : ℝ
⊢ expNear 0 x r = r

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 0 < x - x ^ 3 / 6 - |x| ^ 5 / 100

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ≤ 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 0 < sin x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ 0 < 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ x ≤ 1 * 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
x r : ℝ
⊢ expNear (n + 1) x r = expNear n x (1 + x / (↑n + 1) * r)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 0 < 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
x r₁ r₂ : ℝ
⊢ expNear n x r₁ - expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ |x / 2| ≤ 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x

Tactic:
by

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

Goal state before:
pp: ⊢ |1| ≤ 1

Tactic:
by

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

Goal state before:
pp: ⊢ |1| ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) ≤ 5 / 9

Tactic:
by

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

Goal state before:
pp: ⊢ 2 * cos 1 ^ 2 - 1 ≤ 2 * (5 / 9) ^ 2 - 1

Tactic:
by

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

Goal state before:
pp: ⊢ 2 * (5 / 9) ^ 2 - 1 < 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ 0 < Real.cosh x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cos ↑x + sin ↑x * I‖ = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (↑x * I)‖ = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x)‖ = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (↑x * I)‖₊ = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x)‖₊ = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (↑x * I)‖ₑ = 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x)‖ₑ = 1

Tactic:
by

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

Goal state before:
pp: n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * cexp (↑x / 2 * I) * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖

Tactic:
mul_assoc _ _ (_ - _),

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * (cexp (↑x / 2 * I) * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I))) * I‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖cexp z‖ = Real.exp z.re

Tactic:
by

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

Goal state before:
pp: x y : ℂ
⊢ ‖cexp x‖ = ‖cexp y‖ ↔ x.re = y.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Even n
h : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
p : ℤ
⊢ |(-1) ^ p| = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : ofNat m ≠ 0
⊢ a ^ ofNat m = b ^ ofNat m ↔ a = b ∨ a = -b ∧ Even (ofNat m)

Tactic:
by

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

Goal state before:
pp: n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |rexp x - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
m : ℕ
hn : -[m+1] ≠ 0
⊢ a ^ -[m+1] = b ^ -[m+1] ↔ a = b ∨ a = -b ∧ Even -[m+1]

Tactic:
by

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

Goal state before:
pp: n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |1 + x / ↑m * 0 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)

Tactic:
by

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

Goal state before:
pp: n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
⊢ a ^ ofNat m = -b ^ ofNat m ↔ a = -b ∧ Odd (ofNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
⊢ a ^ -[m+1] = -b ^ -[m+1] ↔ a = -b ∧ Odd -[m+1]

Tactic:
by

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

Goal state before:
pp: n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |rexp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
by

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

Goal state before:
pp: x a b : ℝ
h : |rexp x - expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b
⊢ |rexp x - a| ≤ b

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ 0 < x ^ 3

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ x ^ 3 = 1 - (1 + x + x ^ 2) * (1 - 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''
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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
⊢ ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x ↦ ∑' (y : ι'), f (x, y).1 * g (x, y).2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun x ↦ f x.1 * g 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 : ℕ) 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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
⊢ ‖f m‖ / ‖g m‖ * ‖g m‖ ≤ C₁ * ‖g m‖

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 : ℕ) 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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
⊢ C₁ ∈ ubounds

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
this : Summable fun n ↦ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ Summable fun n ↦ ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ Summable fun n ↦ ‖∑ k ∈ range (n + 1), f k * g (n - k)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Summable f

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 : ℕ) 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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ n₁ ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: n : ℕ
h : n ≠ 0
d m : ℕ
⊢ ((fun a ↦ a + d) ∘ fun x ↦ n • id x) m ≡ d [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: ⊢ ∃ᶠ (m : ℕ) in atTop, Even m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: ⊢ ∃ᶠ (m : ℕ) in atTop, Odd m

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 : ℕ) 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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ max C₀ C₁ ≥ C₀

Tactic:
by

Goal state after: