mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ f' =o[l] g ↔ f' =o[l] g

Tactic:
]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖c • f' x‖) ↔ f =O[l] f'

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖c • f' x‖) ↔ f =O[l] f'
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
⊢ ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ x ∈ range K, (f x * (∑ k ∈ range (K - x), g k - ∑ k ∈ range K, g k) + f x * ∑ k ∈ range K, g k)

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
⊢ ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ x ∈ range K, (f x * (∑ k ∈ range (K - x), g k - ∑ k ∈ range K, g k) + f x * ∑ k ∈ range K, g k)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ f =O[l] f' ↔ f =O[l] f'

Tactic:
]

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

Goal state before:
pp: case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ ∃ b ∈ s, C j ≤ C b

Tactic:
]

Goal state after:
case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ ∃ b ∈ s, C j ≤ C b
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c • f' x‖) ↔ f =o[l] f'

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c • f' x‖) ↔ f =o[l] f'
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ f =o[l] f' ↔ f =o[l] f'

Tactic:
]

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

Goal state before:
pp: case e_a
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∑ i ∈ s, ‖B i x‖ = ∑ i ∈ s, ‖B i x‖

Tactic:
]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖) = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)

Tactic:
]

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ < ↑n

Tactic:
]

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ < ↑n
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ↑m.succ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
]

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ↑m.succ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
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
⊢ ε = ε

Tactic:
]

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

Goal state before:
pp: ⊢ (exp' 0).lim = 1

Tactic:
]

Goal state after:
⊢ (exp' 0).lim = 1
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖

Tactic:
]

Goal state after:
case succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case e_a
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ∑ j ∈ i H, ‖B j H‖ = ∑ i ∈ i H, ‖B i H‖

Tactic:
]

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) = ε
⊢ max N M + 1 < max N M + 1 + (max N M + 1)

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) = ε
⊢ max N M + 1 < max N M + 1 + (max N M + 1)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ ∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * ↑(m.choose i) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
]

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ ∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * ↑(m.choose i) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
]

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * ((↑(m.choose I))⁻¹ * (↑I.factorial)⁻¹ * (↑(m - I).factorial)⁻¹) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
]

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * ((↑(m.choose I))⁻¹ * (↑I.factorial)⁻¹ * (↑(m - I).factorial)⁻¹) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
]

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: a b c d : ℂ
⊢ (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)

Tactic:
by ring

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

Goal state before:
pp: x y : ℂ
⊢ (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + (cexp x + cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))

Tactic:
]

Goal state after:
x y : ℂ
⊢ (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + (cexp x + cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x a p : ℂ
n : ℕ
⊢ cexp (a * ↑n * x / p) = cexp (n • (a * x / p))

Tactic:
]

Goal state after:
x a p : ℂ
n : ℕ
⊢ cexp (a * ↑n * x / p) = cexp (n • (a * x / p))
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
]

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

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

Tactic:
simp [add_comm, cosh, exp_neg]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℂ
h : cexp x = 0
⊢ x + -x = 0 * cexp (-x)

Tactic:
]

Goal state after:
x : ℂ
h : cexp x = 0
⊢ x + -x = 0 * cexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: a b c d : ℂ
⊢ (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)

Tactic:
by ring

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

Goal state before:
pp: x : ℂ
⊢ cexp (x + -x) = cexp x * (cexp x)⁻¹

Tactic:
]

Goal state after:
x : ℂ
⊢ cexp (x + -x) = cexp x * (cexp x)⁻¹
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
⊢ (exp' ((starRingEnd ℂ) x)).lim = (cauSeqConj (exp' x)).lim

Tactic:
]

Goal state after:
x : ℂ
⊢ (exp' ((starRingEnd ℂ) x)).lim = (cauSeqConj (exp' x)).lim
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = ∑ x_1 ∈ range x✝, (starRingEnd ℂ) (x ^ x_1 / ↑x_1.factorial)

Tactic:
]

Goal state after:
x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = ∑ x_1 ∈ range x✝, (starRingEnd ℂ) (x ^ x_1 / ↑x_1.factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑↑n.factorial = (starRingEnd ℂ) x ^ n / ↑↑n.factorial

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ cexp ↑x = cexp ↑x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atBot
⊢ Tendsto (fun x ↦ -(g x / -f x)) l atBot

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atBot
⊢ Tendsto (fun x ↦ -(g x / -f x)) l atBot
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
]

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

Goal state before:
pp: x : ℝ
h : (cexp ↑x).re = 0
⊢ cexp ↑x = 0

Tactic:
← ofReal_inj

Goal state after:
x : ℝ
h : ↑(cexp ↑x).re = ↑0
⊢ cexp ↑x = 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h : ↑(cexp ↑x).re = ↑0
⊢ cexp ↑x = 0

Tactic:
]

Goal state after:
x : ℝ
h : ↑(cexp ↑x).re = ↑0
⊢ cexp ↑x = 0
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))

Tactic:
]

Goal state after:
x y : ℂ
⊢ (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (exp' ↑x).lim.re = (exp' ↑x).lim.re

Tactic:
]

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

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x - cexp (-x)) / 2

Tactic:
]

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

Goal state before:
pp: case hbc
α : 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
m : ℕ
hmJ : m ∈ range (max N M + 1)
⊢ m + N ≤ max N M + 1 + (max N M + 1)

Tactic:
]

Goal state after:
case hbc
α : 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
m : ℕ
hmJ : m ∈ range (max N M + 1)
⊢ m + N ≤ max N M + 1 + (max N M + 1)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh ↑x = sinh ↑x

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
]

Goal state after:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x + cexp (-x)) / 2

Tactic:
]

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
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 ↦ x1 ≤ x2) (‖f x‖ / ‖g x‖) c

Tactic:
]

Goal state after:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
c : ℝ
h₀ : c ≥ 0
hc : IsBigOWith c l f g
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (fun x1 x2 ↦ x1 ≤ x2) (‖f x‖ / ‖g x‖) c
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

Goal state before:
pp: x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹

Tactic:
]

Goal state after:
x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
]

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x

Tactic:
]

Goal state after:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ tanh ↑x = tanh ↑x

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℂ
⊢ cexp x = cexp x

Tactic:
]

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

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

Tactic:
]

Goal state after: