mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
inst✝ : Module R E₃
⊢ ∀ (x : (E × E₂) × E₃), ‖(LinearEquiv.prodAssoc R E E₂ E₃) x‖ = ‖x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : IsBigOWith c₁ l f₁ g₁
h₂ : IsBigOWith c₂ l f₂ g₂
⊢ IsBigOWith (max c₁ c₂) l (fun x ↦ f₁ x + f₂ x) fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
⊢ (fun x ↦ f₁ x + f₂ x) =O[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range n = []

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range n = n' ::ₘ Multiset.range n'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ insert a s = Finset.cons a s h

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

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

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ ∅.sum f = ↑0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → F'
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ (fun x ↦ f₁ x + f₂ x) =o[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ ∅.prod f = ↑1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x ↦ f₁ x - f₂ x) g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : f₂ =o[l] g
hc : c₁ < c₂
⊢ IsBigOWith c₂ l (fun x ↦ f₁ x - f₂ x) g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
h₂ : f₂ =O[l] g
⊢ (fun x ↦ f₁ x - f₂ x) =O[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
h₂ : f₂ =o[l] g
⊢ (fun x ↦ f₁ x - f₂ x) =o[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h : (fun x ↦ f₁ x - f₂ x) =o[l] g
⊢ (fun x ↦ f₂ x - f₁ x) =o[l] g

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial (l + m) = a * b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: «$n» «$l» «$en» «$el» «$m» : ℕ
«$em» : ℕ := «$el» / 2
«$r» : ℕ
«$er» : ℕ := «$el» - «$em»
«$this» : «$el» = «$em» + «$er»
«$nm» : ℕ
«$enm» : ℕ := «$en» + «$em»
«$a» «$ea» : ℕ
«$a_prf» : «$en».ascFactorial «$em» = «$ea»
«$b» «$eb» : ℕ
«$b_prf» : «$enm».ascFactorial «$er» = «$eb»
«$eab» : ℕ := «$ea» * «$eb»
⊢ «$en».ascFactorial «$el» = «$eab»

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
⊢ IsNat n ! a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ IsNat (n.ascFactorial l) a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : x = z + y
a : ℕ
p : (z + 1).ascFactorial y = a
⊢ IsNat (n.descFactorial l) a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ IsNat (n.descFactorial l) 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
c : ℝ
hc : 0 < c
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
c : ℝ
g' : α → F'
l : Filter α
hc : 0 ≤ c
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ 0 * ‖g x‖) x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
c : ℝ
f'' : α → E''
l : Filter α
⊢ (IsBigOWith c l f'' fun _x ↦ 0) ↔ f'' =ᶠ[l] 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ IsBigOWith (‖c‖ / ‖c'‖) l (fun _x ↦ c) fun _x ↦ c'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst✝ : l.NeBot
⊢ ((fun _x ↦ c) =O[l] fun _x ↦ c') ↔ c' = 0 → c = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
c : S
hc : c ≠ 0
f : α → S
l : Filter α
⊢ IsBigOWith ‖c‖⁻¹ l f fun x ↦ c * f x

Tactic:
by

Goal state after:
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₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : IsBigOWith c₁ l f₁ g₁
h₂ : IsBigOWith c₂ l f₂ g₂
⊢ IsBigOWith (c₁ * c₂) l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
by

Goal state after:
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₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : f₂ =o[l] g₂
⊢ (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

Goal state after:
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₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =o[l] g₁
h₂ : f₂ =O[l] g₂
⊢ (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i + -∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k + -∑ k ∈ range (max n i), a k
⊢ n ≤ k + max n i

Tactic:
by

Goal state after:
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
c : ℝ
l : Filter α
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 0 ‖1‖ fun n ↦ c ^ (n + 1)) l (fun x ↦ f x ^ 0) fun x ↦ g x ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖

Tactic:
by

Goal state after:
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
c : ℝ
l : Filter α
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 1 ‖1‖ fun n ↦ c ^ (n + 1)) l (fun x ↦ f x ^ 1) fun x ↦ g x ^ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
⊢ f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
inst✝¹ : One F
inst✝ : NormOneClass F
c : E
l : Filter α
⊢ IsBigOWith ‖c‖ l (fun _x ↦ c) fun _x ↦ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E''' : Type u_12
inst✝³ : Norm F
inst✝² : SeminormedAddGroup E'''
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
f : α → E'''
⊢ (f =o[l] fun _x ↦ 1) ↔ Tendsto f l (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (f =O[l] fun _x ↦ 1) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x‖

Tactic:
by

Goal state after:
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
c : ℝ
l : Filter α
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
n : ℕ
⊢ IsBigOWith (Nat.casesOn (n + 2) ‖1‖ fun n ↦ c ^ (n + 1)) l (fun x ↦ f x ^ (n + 2)) fun x ↦ g x ^ (n + 2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
_x : α
⊢ 0 ≤ ‖1‖

Tactic:
by

Goal state after:
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
c : ℝ
l : Filter α
inst✝¹ : NormOneClass R
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith (c ^ 0) l (fun x ↦ f x ^ 0) fun x ↦ g x ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖1‖ ≤ ‖f x‖) ↔ ∀ (n : ℕ), True → ∀ᶠ (x : α) in l, ‖f x‖ ∈ Ici ↑n

Tactic:
by

Goal state after:
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
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‖
⊢ 0 ≤ c' * ‖g x‖

Tactic:
by

Goal state after:
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
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‖
⊢ c' ^ n * ‖g x ^ n‖ ≤ c' ^ n * ‖g x‖ ^ n

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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
⊢ (IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i) → IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i

Tactic:
by

Goal state after:
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
⊢ (fun x ↦ f x ^ n) =o[l] fun x ↦ g x ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
⊢ (f =O[𝓝[≠] a] fun x ↦ 1) ↔ f =O[𝓝 a] fun x ↦ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
h : f'' =O[l] fun _x ↦ c
hc : c = 0
⊢ f'' =O[l] fun _x ↦ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ (f'' =O[l] fun _x ↦ c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ f =O[l] g'' ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x‖ / ‖g'' x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsBigOWith c l (fun x ↦ (g x)⁻¹) fun x ↦ (f x)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
by

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

Goal state before:
pp: F : Type u_4
inst✝⁴ : Norm F
α : Type u_17
E : Type u_18
inst✝³ : NormedRing E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
f : α → E
x : α
⊢ ContinuousAt f x ↔ (fun x_1 ↦ f x_1 - f x) =o[𝓝 x] fun x ↦ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
⊢ f =O[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =O[l] g
⊢ (∑ i ∈ s, A i) =O[l] g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ (∑ i ∈ s, A i) =o[l] g'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
x : α
hx : 1 x ≤ f x
⊢ ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ (f ^ n) =O[l] (f ^ m)

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)
⊢ ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n

Tactic:
by

Goal state after:
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
⊢ (fun x ↦ c • f' x) =O[l] g ↔ f' =O[l] g

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
⊢ (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k

Tactic:
by

Goal state after:
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
⊢ (fun x ↦ c • f' x) =o[l] g ↔ f' =o[l] g

Tactic:
by

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
⊢ (f =O[l] fun x ↦ c • f' x) ↔ f =O[l] f'

Tactic:
by

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

Tactic:
by

Goal state after: