awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₂ g₂
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) c l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

Premises used: div_mul_cancel₀, ne_of_gt, div_pos, Asymptotics.IsBigOWith.mul, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =o[l] g₁
h₂ : f₂ =o[l] g₂
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
h₁.mul_isBigO h₂.isBigO

Premises used: Asymptotics.IsLittleO.isBigO, Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c : ℝ
l : Filter α
inst_3 : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ Nontrivial S

Tactic:
have : Nontrivial S := NormOneClass.nontrivial
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c : ℝ
l : Filter α
inst_3 : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
this : Nontrivial S
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℝ) 0 (norm.{u_13} (E := R) 1) fun (n : ℕ) ↦ c ^ (n + 1)) l
    (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0) fun (x : α) ↦ HPow.hPow (β := ℕ) (g x) 0

Tactic:
simpa using isBigOWith_const_const (1 : R) (one_ne_zero' S) l

Premises used: one_ne_zero', Asymptotics.isBigOWith_const_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c : ℝ
l : Filter α
inst_3 : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℝ) 1 (norm.{u_13} (E := R) 1) fun (n : ℕ) ↦ c ^ (n + 1)) l
    (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 1) fun (x : α) ↦ HPow.hPow (β := ℕ) (g x) 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c : ℝ
l : Filter α
inst_3 : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
n : ℕ
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℝ) (n + 2) (norm.{u_13} (E := R) 1) fun (n : ℕ) ↦ c ^ (n + 1)) l
    (fun (x : α) ↦ f x ^ (n + 2)) fun (x : α) ↦ g x ^ (n + 2)

Tactic:
simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h

Premises used: pow_succ, HAdd.hAdd, OfNat.ofNat, Asymptotics.IsBigOWith.mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c : ℝ
l : Filter α
inst_3 : NormOneClass R
inst_4 : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith.{u_1, u_13, u_17} (E := R) (F := S) (HPow.hPow (β := ℕ) c 0) l (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 0)
    fun (x : α) ↦ HPow.hPow (β := ℕ) (g x) 0

Tactic:
simpa using h.pow' 0

Premises used: Asymptotics.IsBigOWith.pow', OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c c' : ℝ
l : Filter α
inst_3 : 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:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c c' : ℝ
l : Filter α
inst_3 : 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‖
hbc : ‖g x ^ n‖ ≤ ‖g x‖ ^ n
⊢ c' ^ n * ‖g x ^ n‖ ≤ c' ^ n * ‖g x‖ ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c c' : ℝ
l : Filter α
inst_3 : 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:
norm_pow_le' _ hn.bot_lt

Premises used: norm_pow_le', Ne.bot_lt
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
c c' : ℝ
l : Filter α
inst_3 : 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:
exact norm_pow_le' _ hn.bot_lt

Premises used: norm_pow_le', Ne.bot_lt
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
inst_3 : NormOneClass S
f : α → R
g : α → S
h : f =O[l] g
n : ℕ
⊢ IsBigO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n

Tactic:
let ⟨_C, hC⟩ := h.isBigOWith
  isBigO_iff_isBigOWith.2 ⟨_, hC.pow' n⟩

Premises used: Iff.mpr, Norm.norm, _private.0.Asymptotics.IsBigO.mul.match_1, Asymptotics.IsBigO, Asymptotics.IsBigOWith.pow', HPow.hPow, HAdd.hAdd, Exists.intro, Asymptotics.IsBigO.isBigOWith, Asymptotics.isBigO_iff_isBigOWith, OfNat.ofNat, Nat.casesOn
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
hn : 0 < n
obtain :
  ∀ (n : ℕ) (hn : 0 < n.succ),
    IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ Nat.succ 0) fun (x : α) ↦ g x ^ Nat.succ 0

Tactic:
simpa only [pow_one]

Premises used: pow_one
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ * f x) fun (x : α) ↦ g x ^ n.succ * g x

Tactic:
ihn.mul h

Premises used: Asymptotics.IsLittleO.mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
h₁ : ∀ (x : α), f x ^ (n + 1).succ = f x ^ n.succ * f x
h₂ : ∀ (x : α), g x ^ (n + 1).succ = g x ^ n.succ * g x
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ (n + 1).succ) fun (x : α) ↦ g x ^ (n + 1).succ

Tactic:
convert! ihn.mul h

Premises used: Asymptotics.IsLittleO.mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
x : α
⊢ f x ^ (n + 1).succ = f x ^ n.succ * f x

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ
x : α
⊢ g x ^ (n + 1).succ = g x ^ n.succ * g x

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
zero : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ Nat.succ 0) fun (x : α) ↦ g x ^ Nat.succ 0
succ :
  ∀ (n : ℕ)
    (ihn : IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ),
    IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ (n + 1).succ) fun (x : α) ↦ g x ^ (n + 1).succ
⊢ IsLittleO.{u_1, u_13, u_17} (E := R) (F := S) l (fun (x : α) ↦ f x ^ n.succ) fun (x : α) ↦ g x ^ n.succ

Tactic:
induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert! ihn.mul h <;> simp [pow_succ]

Premises used: pow_succ, pow_one
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
S : Type u_17
inst_1 : NormedRing S
inst_2 : NormMulClass S
l : Filter α
inst_3 : NormOneClass S
f : α → S
g : α → R
n : ℕ
h : (f ^ n) =o[l] (g ^ n)
hn : n ≠ 0
⊢ f =o[l] g

Tactic:
IsLittleO.of_isBigOWith fun _c hc => (h.def' <| pow_pos hc _).of_pow hn le_rfl hc.le

Premises used: pow_pos, le_rfl, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.of_pow, LT.lt.le, Asymptotics.IsLittleO.def'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsBigOWith.{u_1, u_16, u_15} (E := 𝕜') (F := 𝕜) c l (fun (x : α) ↦ (g x)⁻¹) fun (x : α) ↦ (f x)⁻¹

Tactic:
IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => ?_))

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Asymptotics.IsBigOWith.bound, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
refine : ∀ (x : α) (h₀ : f x = 0 → g x = 0) (hle : ‖f x‖ ≤ c * ‖g x‖), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
⊢ IsBigOWith.{u_1, u_16, u_15} (E := 𝕜') (F := 𝕜) c l (fun (x : α) ↦ (g x)⁻¹) fun (x : α) ↦ (f x)⁻¹

Tactic:
refine IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => ?_))

Premises used: Filter.Eventually.mono, Filter.Eventually.mp, Asymptotics.IsBigOWith.bound, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
inl : ∀ (hx : f x = 0), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
inr : ∀ (hx : f x ≠ 0), ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
rcases eq_or_ne (f x) 0 with hx | hx

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x = 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
simp only [hx, h₀ hx, inv_zero, norm_zero, mul_zero, le_rfl]

Premises used: le_rfl, inv_zero, norm_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
⊢ 0 < c

Tactic:
have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
hc : 0 < c
⊢ (c * ‖g x‖)⁻¹ ≤ ‖f x‖⁻¹

Tactic:
replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀_1 : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hx : f x ≠ 0
hc : 0 < c
hle : (c * ‖g x‖)⁻¹ ≤ ‖f x‖⁻¹
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
simpa only [norm_inv, mul_inv, ← div_eq_inv_mul, div_le_iff₀ hc] using hle

Premises used: div_le_iff₀, mul_inv, norm_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =O[l] g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsBigO.{u_1, u_16, u_15} (E := 𝕜') (F := 𝕜) l (fun (x : α) ↦ (g x)⁻¹) fun (x : α) ↦ (f x)⁻¹

Tactic:
let ⟨_c, hc⟩ := h.isBigOWith
  (hc.inv_rev h₀).isBigO

Premises used: Asymptotics.IsBigO, _private.0.Asymptotics.IsBigO.inv_rev.match_1, Inv.inv, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigO.isBigOWith, Asymptotics.IsBigOWith.inv_rev
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =o[l] g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsLittleO.{u_1, u_16, u_15} (E := 𝕜') (F := 𝕜) l (fun (x : α) ↦ (g x)⁻¹) fun (x : α) ↦ (f x)⁻¹

Tactic:
IsLittleO.of_isBigOWith fun _c hc => (h.def' hc).inv_rev h₀

Premises used: Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.inv_rev, Asymptotics.IsLittleO.def'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ ∅, C i) l (fun (x : α) ↦ ∑ i ∈ ∅, A i x) g

Tactic:
simp only [isBigOWith_zero', Finset.sum_empty]

Premises used: Asymptotics.isBigOWith_zero', Finset.sum_empty
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s_1 : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g
cons :
  ∀ (h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (C i + ∑ i ∈ s, C i) l (fun (x : α) ↦ A i x + ∑ i ∈ s, A i x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ Finset.cons i s is, C i) l (fun (x : α) ↦ ∑ i ∈ Finset.cons i s is, A i x)
    g

Tactic:
simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢

Premises used: Finset.sum_cons, Finset.forall_mem_cons
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s_1 : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (C i + ∑ i ∈ s, C i) l (fun (x : α) ↦ A i x + ∑ i ∈ s, A i x) g

Tactic:
h.1.add (IH h.2)

Premises used: Asymptotics.IsBigOWith.add, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s_1 : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (C i + ∑ i ∈ s, C i) l (fun (x : α) ↦ A i x + ∑ i ∈ s, A i x) g

Tactic:
exact h.1.add (IH h.2)

Premises used: Asymptotics.IsBigOWith.add, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ ∅, C i) l (fun (x : α) ↦ ∑ i ∈ ∅, A i x) g
cons :
  ∀ (i : ι) (s : Finset ι) (is : i ∉ s)
    (IH :
      ∀ (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
        IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g)
    (h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g),
    IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ Finset.cons i s is, C i) l
      (fun (x : α) ↦ ∑ i ∈ Finset.cons i s is, A i x) g
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') (∑ i ∈ s, C i) l (fun (x : α) ↦ ∑ i ∈ s, A i x) g

Tactic:
induction s using Finset.cons_induction with
  | empty => simp only [isBigOWith_zero', Finset.sum_empty]
  | cons i s is IH =>
    simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
    exact h.1.add (IH h.2)

Premises used: Finset.sum_cons, Asymptotics.isBigOWith_zero', Finset.forall_mem_cons, Finset.sum_empty
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =O[l] g
simp :
  ∀ (h : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) g),
    ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ ∑ i ∈ s, A i x) g

Tactic:
simp only [IsBigO_def] at *

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) g
choose! :
  ∀ (C : (i : ι) → ℝ) (hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g),
    ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g
⊢ ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g

Tactic:
choose! C hC using h
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
C : (i : ι) → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g

Tactic:
⟨_, IsBigOWith.sum hC⟩

Premises used: Asymptotics.IsBigOWith.sum, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
C : (i : ι) → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ ∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ ∑ i ∈ s, A i x) g

Tactic:
exact ⟨_, IsBigOWith.sum hC⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
simp : IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ (∑ c ∈ s, A c) x) g'
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ ∑ i ∈ s, A i x) g'

Tactic:
simp only [← Finset.sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ (∑ c ∈ s, A c) x) g'

Tactic:
Finset.sum_induction A (· =o[l] g') (fun _ _ ↦ .add) (isLittleO_zero ..) h

Premises used: Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.add, Asymptotics.IsLittleO, Finset.sum_induction
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =o[l] g'
⊢ IsLittleO.{u_1, u_6, u_7} (E := E') l (fun (x : α) ↦ (∑ c ∈ s, A c) x) g'

Tactic:
exact Finset.sum_induction A (· =o[l] g') (fun _ _ ↦ .add) (isLittleO_zero ..) h

Premises used: Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.add, Asymptotics.IsLittleO, Finset.sum_induction
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
inl :
  ∀ (hAB : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) (B i)),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑∅ : Set ι))) l (fun (H : α) ↦ ∑ i ∈ ∅, A i H)
      fun (H : α) ↦ ∑ i ∈ ∅, ‖B i H‖
inr :
  ∀ (hs : s.Nonempty),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H)
      fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦
    ∑ i ∈ s, ‖B i H‖

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
B : ι → α → ℝ
hAB : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBigOWith (C i) l (A i) (B i)
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑∅ : Set ι))) l (fun (H : α) ↦ ∑ i ∈ ∅, A i H) fun (H : α) ↦
    ∑ i ∈ ∅, ‖B i H‖

Tactic:
simp [isBigOWith_zero]

Premises used: Asymptotics.isBigOWith_zero