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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖

Tactic:
;

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖k' x‖
hg : ∀ᶠ (x : α) in l, ‖g' x‖ ≤ c * ‖k' x‖
⊢ ∀ᶠ (x : α) in l, ‖(f' x, g' x)‖ ≤ c * ‖k' x‖
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
x✝ : E × E₂
⊢ ‖(LinearEquiv.prodComm R E E₂) x✝‖ = ‖x✝‖

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
x✝ : E × E₂
⊢ ‖(LinearEquiv.prodComm R E E₂) x✝‖ = ‖x✝‖
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case hbc
α : Type u_1
R : Type u_13
inst✝³ : SeminormedRing R
S : Type u_17
inst✝² : NormedRing S
inst✝¹ : NormMulClass S
c c' : ℝ
l : Filter α
inst✝ : NormOneClass S
n : ℕ
f : α → S
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ ‖g x ^ n‖ ≤ ‖g x‖ ^ n

Tactic:
;

Goal state after:
case hbc
α : Type u_1
R : Type u_13
inst✝³ : SeminormedRing R
S : Type u_17
inst✝² : NormedRing S
inst✝¹ : NormMulClass S
c c' : ℝ
l : Filter α
inst✝ : NormOneClass S
n : ℕ
f : α → S
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ ‖g x ^ n‖ ≤ ‖g x‖ ^ n
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
hn : 0 < n.succ
⊢ (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
hn : 0 < n.succ
⊢ (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
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'
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
⊢ C j * ‖B j x‖ ≤ sSup (C '' ↑s) * ‖B j x‖

Tactic:
;

Goal state after:
α : 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
⊢ C j * ‖B j x‖ ≤ sSup (C '' ↑s) * ‖B j x‖
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.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:
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‖‖
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.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‖ = ‖∑ j ∈ i H, ‖B j H‖‖

Tactic:
;

Goal state after:
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‖ = ‖∑ j ∈ i H, ‖B j H‖‖
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.Trigonometric

Goal state before:
pp: ⊢ sinh 0 = 0

Tactic:
by simp [sinh]

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

Goal state before:
pp: case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ Tendsto (fun x ↦ ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop

Tactic:
;

Goal state after:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ Tendsto (fun x ↦ ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop
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.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: case ofNat
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.ofNat a✝) * z) = cexp z ^ Int.ofNat a✝

pp: case negSucc
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.negSucc a✝) * z) = cexp z ^ Int.negSucc a✝

Tactic:
· simp [exp_nat_mul]

Goal state after:
case negSucc
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.negSucc a✝) * z) = cexp z ^ Int.negSucc a✝
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.Asymptotics.Lemmas

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
exact ⟨φ, ⟨c, hφ⟩, huvφ⟩

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

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

Tactic:
;

Goal state after:
x : ℂ
⊢ cosh (x * I * I) = cosh x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
;

Goal state after:
x : ℂ
⊢ cosh (x * I ^ 2) = cosh x
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
;

Goal state after:
case hab
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n) ≤ ↑n.succ
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
;

Goal state after:
case hab
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
;

Goal state after:
z : ℂ
⊢ z = ↑z.re + ↑z.im * I
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
exact (re_add_im z).symm

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
⊢ 1 < 1 + ‖a‖

Tactic:
;

Goal state after:
α : 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
⊢ 1 < 1 + ‖a‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:

Tactic:
cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_

Goal state after:
case calc_1
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

case calc_2
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
by
  rw [← lim_const (abv := norm) (∑ m ∈ range n, _),
    exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_norm]
  refine lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
  simp_rw [← sub_eq_add_neg]
  change ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤
    ‖x‖ ^ n / n.factorial * 2
  let k := j - n
  have hj : j = n + k := (add_tsub_cancel_of_le hj).symm
  rw [hj, sum_range_add_sub_sum_range]
  calc
    ‖∑ i ∈ range k, x ^ (n + i) / ((n + i).factorial : ℂ)‖ ≤
        ∑ i ∈ range k, ‖x ^ (n + i) / ((n + i).factorial : ℂ)‖ :=
      IsAbsoluteValue.abv_sum _ _ _
    _ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / (n + i).factorial := by
      simp [norm_natCast, Complex.norm_pow]
    _ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ((n.factorial : ℝ) * (n.succ : ℝ) ^ i) := ?_
    _ = ∑ i ∈ range k, ‖x‖ ^ n / n.factorial * (‖x‖ ^ i / (n.succ : ℝ) ^ i) := ?_
    _ ≤ ‖x‖ ^ n / ↑n.factorial * 2 := ?_
  · gcongr
    exact mod_cast Nat.factorial_mul_pow_le_factorial
  · simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc]
  · rw [← mul_sum]
    gcongr
    simp_rw [← div_pow]
    rw [geom_sum_eq, div_le_iff_of_neg]
    · trans (-1 : ℝ)
      · linarith
      · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
        positivity
    · linarith
    · linarith

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

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

Tactic:
;

Goal state after:
case hbc
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ↑(Nat.succ 2) * (↑(Nat.factorial 2) * ↑2)⁻¹ ≤ 1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [exp_add, exp_mul_I]

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

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

Tactic:
by
      grw [norm_add_le]
      simp

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 (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.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 : ℝ
⊢ sinh (-x) = -sinh x

Tactic:
by simp [sinh]

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

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 : ℝ
⊢ ↑(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.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 : ℝ
⊢ ↑(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:
;

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

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

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

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