awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l l' : Filter α
h : f =Θ[l] g
hl : l' ≤ l
⊢ f =Θ[l'] g

Tactic:
⟨h.1.mono hl, h.2.mono hl⟩

Premises used: Asymptotics.IsTheta, And.right, And.left, Asymptotics.IsBigO.mono, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l l' : Filter α
h : f' =Θ[l] g'
h' : f' =Θ[l'] g'
⊢ f' =Θ[l ⊔ l'] g'

Tactic:
⟨h.1.sup h'.1, h.2.sup h'.2⟩

Premises used: Asymptotics.IsTheta, And.right, And.left, And.intro, Asymptotics.IsBigO.sup
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l l' : Filter α
⊢ f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g'

Tactic:
⟨fun h ↦ ⟨h.mono le_sup_left, h.mono le_sup_right⟩, fun h ↦ h.1.sup h.2⟩

Premises used: le_sup_left, Asymptotics.IsTheta.mono, le_sup_right, And.right, And.left, And.intro, Iff.intro, Asymptotics.IsTheta.sup
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
l : Filter α
h : f'' =Θ[l] g''
⊢ ∀ᶠ (x : α) in l, f'' x = 0 ↔ g'' x = 0

Tactic:
h.1.eq_zero_imp.mp <| h.2.eq_zero_imp.mono fun _ ↦ Iff.intro

Premises used: Filter.Eventually.mono, Asymptotics.IsBigO.eq_zero_imp, Filter.Eventually.mp, And.right, And.left, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
l : Filter α
h : f'' =Θ[l] g''
⊢ Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)

Tactic:
simp only [← isLittleO_one_iff ℝ, h.isLittleO_congr_left]

Premises used: Real, Asymptotics.IsTheta.isLittleO_congr_left, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop

Tactic:
simp only [Function.comp_def, ← isLittleO_const_left_of_ne (one_ne_zero' ℝ),
    h.isLittleO_congr_right]

Premises used: Real, one_ne_zero', Asymptotics.isLittleO_const_left_of_ne, Function.comp_def, Asymptotics.IsTheta.isLittleO_congr_right
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f') ↔ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ g')

Tactic:
simp only [← isBigO_const_of_ne (one_ne_zero' ℝ), h.isBigO_congr_left]

Premises used: Real, one_ne_zero', Asymptotics.IsTheta.isBigO_congr_left, Asymptotics.isBigO_const_of_ne
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
𝕜 : Type u_14
𝕜' : Type u_15
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : NormedField 𝕜
inst_3 : NormedField 𝕜'
l : Filter α
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedSpace 𝕜' F'
f₁ : α → 𝕜
f₂ : α → 𝕜'
g₁ : α → E'
g₂ : α → F'
hf : f₁ =Θ[l] f₂
hg : g₁ =Θ[l] g₂
⊢ IsTheta.{u_1, u_6, u_7} (E := E') (F := F') l (fun (x : α) ↦ f₁ x • g₁ x) fun (x : α) ↦ f₂ x • g₂ x

Tactic:
⟨hf.1.smul hg.1, hf.2.smul hg.2⟩

Premises used: Asymptotics.IsBigO.smul, Asymptotics.IsTheta, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f₁ x * f₂ x) fun (x : α) ↦ g₁ x * g₂ x

Tactic:
h₁.smul h₂

Premises used: Asymptotics.IsTheta.smul
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
ι : Type u_16
L : List ι
f : ι → α → 𝕜
g : ι → α → 𝕜'
h : ∀ i ∈ L, f i =Θ[l] g i
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
    fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
⟨.listProd fun i hi ↦ (h i hi).isBigO, .listProd fun i hi ↦ (h i hi).symm.isBigO⟩

Premises used: Asymptotics.IsTheta.symm, Asymptotics.IsBigO.listProd, Asymptotics.IsTheta, Asymptotics.IsTheta.isBigO, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
ι : Type u_16
s : Multiset ι
f : ι → α → 𝕜
g : ι → α → 𝕜'
h : ∀ i ∈ s, f i =Θ[l] g i
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) s)) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) s)

Tactic:
⟨.multisetProd fun i hi ↦ (h i hi).isBigO, .multisetProd fun i hi ↦ (h i hi).symm.isBigO⟩

Premises used: Asymptotics.IsTheta.symm, Asymptotics.IsTheta, Asymptotics.IsBigO.multisetProd, Asymptotics.IsTheta.isBigO, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
ι : Type u_16
s : Finset ι
f : ι → α → 𝕜
g : ι → α → 𝕜'
h : ∀ i ∈ s, f i =Θ[l] g i
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ ∏ i ∈ s, f i x) fun (x : α) ↦ ∏ i ∈ s, g i x

Tactic:
⟨.finsetProd fun i hi ↦ (h i hi).isBigO, .finsetProd fun i hi ↦ (h i hi).symm.isBigO⟩

Premises used: Asymptotics.IsTheta.symm, Asymptotics.IsTheta, Asymptotics.IsBigO.finsetProd, Asymptotics.IsTheta.isBigO, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ (f x)⁻¹) fun (x : α) ↦ (g x)⁻¹

Tactic:
⟨h.2.inv_rev h.1.eq_zero_imp, h.1.inv_rev h.2.eq_zero_imp⟩

Premises used: Asymptotics.IsTheta, Asymptotics.IsBigO.eq_zero_imp, And.right, Asymptotics.IsBigO.inv_rev, And.left, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ (f x)⁻¹) fun (x : α) ↦ (g x)⁻¹
⊢ f =Θ[l] g

Tactic:
simpa only [inv_inv] using h.inv

Premises used: Asymptotics.IsTheta.inv, inv_inv
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f₁ x / f₂ x) fun (x : α) ↦ g₁ x / g₂ x

Tactic:
simpa only [div_eq_mul_inv] using h₁.mul h₂.inv

Premises used: div_eq_mul_inv, Asymptotics.IsTheta.inv, Asymptotics.IsTheta.mul
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℕ
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n

Tactic:
⟨h.1.pow n, h.2.pow n⟩

Premises used: Asymptotics.IsTheta, And.right, And.left, And.intro, Asymptotics.IsBigO.pow
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
ofNat :
  ∀ (a : ℕ),
    IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.ofNat a) fun (x : α) ↦ g x ^ Int.ofNat a
negSucc :
  ∀ (a : ℕ),
    IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.negSucc a) fun (x : α) ↦ g x ^ Int.negSucc a
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ n) fun (x : α) ↦ g x ^ n

Tactic:
cases n
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a : ℕ
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.ofNat a) fun (x : α) ↦ g x ^ Int.ofNat a

Tactic:
simpa only [Int.ofNat_eq_natCast, zpow_natCast] using h.pow _

Premises used: zpow_natCast, Int.ofNat_eq_natCast, Asymptotics.IsTheta.pow
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a : ℕ
⊢ IsTheta.{u_1, u_14, u_15} (E := 𝕜) (F := 𝕜') l (fun (x : α) ↦ f x ^ Int.negSucc a) fun (x : α) ↦ g x ^ Int.negSucc a

Tactic:
simpa only [zpow_negSucc] using (h.pow _).inv

Premises used: zpow_negSucc, Asymptotics.IsTheta.pow, Asymptotics.IsTheta.inv
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
l : Filter α
c₁ : E''
c₂ : F''
h₁ : c₁ ≠ 0
h₂ : c₂ ≠ 0
⊢ IsTheta.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (x : α) ↦ c₁) fun (x : α) ↦ c₂

Tactic:
⟨isBigO_const_const _ h₂ _, isBigO_const_const _ h₁ _⟩

Premises used: Asymptotics.IsTheta, Asymptotics.isBigO_const_const, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
l : Filter α
inst_2 : l.NeBot
c₁ : E''
c₂ : F''
⊢ (IsTheta.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (x : α) ↦ c₁) fun (x : α) ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Tactic:
simpa only [IsTheta, isBigO_const_const_iff, ← iff_def] using Iff.comm

Premises used: Asymptotics.isBigO_const_const_iff, iff_def, Asymptotics.IsTheta, Iff.comm
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
F'' : Type u_10
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ IsTheta.{u_1, u_6, u_10} (E := E') l (fun (x : α) ↦ 0) g'' ↔ g'' =ᶠ[l] 0

Tactic:
simp only [IsTheta, isBigO_zero, isBigO_zero_right_iff, true_and]

Premises used: Asymptotics.isBigO_zero_right_iff, Asymptotics.isBigO_zero, Asymptotics.IsTheta, true_and
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
f'' : α → E''
l : Filter α
⊢ (IsTheta.{u_1, u_9, u_7} (F := F') l f'' fun (x : α) ↦ 0) ↔ f'' =ᶠ[l] 0

Tactic:
isTheta_comm.trans isTheta_zero_left

Premises used: Asymptotics.isTheta_comm, Iff.trans, Asymptotics.isTheta_zero_left
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_14
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedField 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : NormedSpace 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ IsTheta.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =Θ[l] g

Tactic:
and_congr (isBigO_const_smul_left hc) (isBigO_const_smul_right hc)

Premises used: Asymptotics.isBigO_const_smul_right, Asymptotics.IsTheta, Asymptotics.isBigO_const_smul_left, and_congr
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
𝕜 : Type u_14
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
inst_2 : NormedField 𝕜
f : α → E
g' : α → F'
l : Filter α
inst_3 : NormedSpace 𝕜 F'
c : 𝕜
hc : c ≠ 0
⊢ (IsTheta.{u_1, u_3, u_7} (F := F') l f fun (x : α) ↦ c • g' x) ↔ f =Θ[l] g'

Tactic:
and_congr (isBigO_const_smul_right hc) (isBigO_const_smul_left hc)

Premises used: Asymptotics.isBigO_const_smul_right, Asymptotics.IsTheta, Asymptotics.isBigO_const_smul_left, and_congr
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
F : Type u_4
𝕜 : Type u_14
inst : Norm F
inst_1 : NormedField 𝕜
g : α → F
l : Filter α
c : 𝕜
f : α → 𝕜
hc : c ≠ 0
⊢ IsTheta.{u_1, u_14, u_4} (E := 𝕜) l (fun (x : α) ↦ c * f x) g ↔ f =Θ[l] g

Tactic:
simpa only [← smul_eq_mul] using isTheta_const_smul_left hc

Premises used: Asymptotics.isTheta_const_smul_left, smul_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_14
inst : Norm E
inst_1 : NormedField 𝕜
f : α → E
l : Filter α
c : 𝕜
g : α → 𝕜
hc : c ≠ 0
⊢ (IsTheta.{u_1, u_3, u_14} (F := 𝕜) l f fun (x : α) ↦ c * g x) ↔ f =Θ[l] g

Tactic:
simpa only [← smul_eq_mul] using isTheta_const_smul_right hc

Premises used: smul_eq_mul, Asymptotics.isTheta_const_smul_right
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
h : f₁ =o[l] f₂
⊢ f₂ =Θ[l] (f₁ + f₂)

Tactic:
⟨h.right_isBigO_add, h.add_isBigO (isBigO_refl _ _)⟩

Premises used: Asymptotics.IsLittleO.add_isBigO, Asymptotics.IsTheta, And.intro, Asymptotics.IsLittleO.right_isBigO_add, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
h : f₁ =o[l] f₂
⊢ f₂ =Θ[l] (f₂ + f₁)

Tactic:
add_comm f₁ f₂ ▸ h.right_isTheta_add

Premises used: Asymptotics.IsLittleO.right_isTheta_add, Eq.rec, add_comm
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g : α → F
hΘ : f₁ =Θ[l] g
ho : f₂ =o[l] g
⊢ (f₁ + f₂) =Θ[l] g

Tactic:
(ho.trans_isTheta hΘ.symm).right_isTheta_add'.symm.trans hΘ

Premises used: Asymptotics.IsTheta.symm, Asymptotics.IsLittleO.trans_isTheta, Asymptotics.IsTheta.trans, Asymptotics.IsLittleO.right_isTheta_add'
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g : α → F
ho : f₁ =o[l] g
hΘ : f₂ =Θ[l] g
⊢ (f₁ + f₂) =Θ[l] g

Tactic:
add_comm f₁ f₂ ▸ hΘ.add_isLittleO ho

Premises used: Asymptotics.IsTheta.add_isLittleO, Eq.rec, add_comm, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ f =Θ[l] g

Tactic:
⟨isBigO_of_div_tendsto_nhds_of_ne_zero h hc,
    isBigO_of_div_tendsto_nhds_of_ne_zero ?_ (inv_ne_zero hc)⟩

Premises used: Asymptotics.IsTheta, Asymptotics.isBigO_of_div_tendsto_nhds_of_ne_zero, And.intro, inv_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
refine : Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 c⁻¹)
⊢ f =Θ[l] g

Tactic:
refine ⟨isBigO_of_div_tendsto_nhds_of_ne_zero h hc,
    isBigO_of_div_tendsto_nhds_of_ne_zero ?_ (inv_ne_zero hc)⟩
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ Tendsto (fun (x : α) ↦ (g x / f x)⁻¹) l (𝓝 c⁻¹)

Tactic:
h.inv₀ hc

Premises used: Filter.Tendsto.inv₀
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
h₁ : Eq (α := α → 𝕜) (fun (x : α) ↦ f x / g x) fun (x : α) ↦ (g x / f x)⁻¹
⊢ Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 c⁻¹)

Tactic:
convert! h.inv₀ hc using 1

Premises used: Filter.Tendsto.inv₀
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
h₁ : ∀ (x : α), f x / g x = (g x / f x)⁻¹
⊢ Eq (α := α → 𝕜) (fun (x : α) ↦ f x / g x) fun (x : α) ↦ (g x / f x)⁻¹

Tactic:
ext
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
𝕜 : Type u_14
inst : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun (x : α) ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
x : α
⊢ f x / g x = (g x / f x)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
simp :
  f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : α) in l,
        IsBigO.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x_1 : β) ↦ f (x, x_1)) fun (x_1 : β) ↦ g (x, x_1)) ∧
      ∀ᶠ (x : α) in l,
        IsBigO.{u_2, u_4, u_3} (E := F) (F := E) l' (fun (x_1 : β) ↦ g (x, x_1)) fun (x_1 : β) ↦ f (x, x_1)
⊢ f =Θ[l ×ˢ l'] g →
    ∀ᶠ (x : α) in l,
      IsTheta.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x_1 : β) ↦ f (x, x_1)) fun (x_1 : β) ↦ g (x, x_1)

Tactic:
simp only [IsTheta, eventually_and]

Premises used: Filter.eventually_and, Asymptotics.IsTheta
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : α) in l,
        IsBigO.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x_1 : β) ↦ f (x, x_1)) fun (x_1 : β) ↦ g (x, x_1)) ∧
      ∀ᶠ (x : α) in l,
        IsBigO.{u_2, u_4, u_3} (E := F) (F := E) l' (fun (x_1 : β) ↦ g (x, x_1)) fun (x_1 : β) ↦ f (x, x_1)

Tactic:
fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_right, h₂.fiberwise_right⟩

Premises used: Filter.Eventually, Asymptotics.IsBigO, _private.0.Asymptotics.IsTheta.fiberwise_right.match_1, Prod.mk, And, And.intro, Asymptotics.IsBigO.fiberwise_right
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : α) in l,
        IsBigO.{u_2, u_3, u_4} (E := E) (F := F) l' (fun (x_1 : β) ↦ f (x, x_1)) fun (x_1 : β) ↦ g (x, x_1)) ∧
      ∀ᶠ (x : α) in l,
        IsBigO.{u_2, u_4, u_3} (E := F) (F := E) l' (fun (x_1 : β) ↦ g (x, x_1)) fun (x_1 : β) ↦ f (x, x_1)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_right, h₂.fiberwise_right⟩
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
simp :
  f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : β) in l',
        IsBigO.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x_1 : α) ↦ f (x_1, x)) fun (x_1 : α) ↦ g (x_1, x)) ∧
      ∀ᶠ (x : β) in l',
        IsBigO.{u_1, u_4, u_3} (E := F) (F := E) l (fun (x_1 : α) ↦ g (x_1, x)) fun (x_1 : α) ↦ f (x_1, x)
⊢ f =Θ[l ×ˢ l'] g →
    ∀ᶠ (y : β) in l', IsTheta.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x : α) ↦ f (x, y)) fun (x : α) ↦ g (x, y)

Tactic:
simp only [IsTheta, eventually_and]

Premises used: Filter.eventually_and, Asymptotics.IsTheta
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : β) in l',
        IsBigO.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x_1 : α) ↦ f (x_1, x)) fun (x_1 : α) ↦ g (x_1, x)) ∧
      ∀ᶠ (x : β) in l',
        IsBigO.{u_1, u_4, u_3} (E := F) (F := E) l (fun (x_1 : α) ↦ g (x_1, x)) fun (x_1 : α) ↦ f (x_1, x)

Tactic:
fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

Premises used: Filter.Eventually, Asymptotics.IsBigO, _private.0.Asymptotics.IsTheta.fiberwise_right.match_1, Prod.mk, And, And.intro, Asymptotics.IsBigO.fiberwise_left
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : β) in l',
        IsBigO.{u_1, u_3, u_4} (E := E) (F := F) l (fun (x_1 : α) ↦ f (x_1, x)) fun (x_1 : α) ↦ g (x_1, x)) ∧
      ∀ᶠ (x : β) in l',
        IsBigO.{u_1, u_4, u_3} (E := F) (F := E) l (fun (x_1 : α) ↦ g (x_1, x)) fun (x_1 : α) ↦ f (x_1, x)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) ∧ (g ∘ Prod.fst) =O[l ×ˢ l'] (f ∘ Prod.fst)

Tactic:
fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_fst l', h₂.comp_fst l'⟩

Premises used: SProd.sprod, Asymptotics.IsBigO, Asymptotics.IsBigO.comp_fst, Function.comp, Prod.fst, And, And.intro, _private.0.Asymptotics.IsTheta.comp_fst.match_1
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) ∧ (g ∘ Prod.fst) =O[l ×ˢ l'] (f ∘ Prod.fst)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_fst l', h₂.comp_fst l'⟩
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) ∧ (g ∘ Prod.snd) =O[l' ×ˢ l] (f ∘ Prod.snd)

Tactic:
fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_snd l', h₂.comp_snd l'⟩

Premises used: SProd.sprod, Asymptotics.IsBigO, Asymptotics.IsBigO.comp_snd, Function.comp, And, And.intro, _private.0.Asymptotics.IsTheta.comp_fst.match_1, Prod.snd
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) ∧ (g ∘ Prod.snd) =O[l' ×ˢ l] (f ∘ Prod.snd)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_snd l', h₂.comp_snd l'⟩
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddGroup E
inst_1 : SeminormedAddGroup F
inst_2 : TopologicalSpace α
s : Set α
f : α → E
c : F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
hC : ∀ i ∈ s, f i ≠ 0
⊢ Asymptotics.IsTheta.{u_1, u_2, u_3} (F := F) (𝓟 s) f fun (x : α) ↦ c

Tactic:
⟨hf.isBigO_principal hs hc, hf.isBigO_rev_principal hs hC c⟩

Premises used: ContinuousOn.isBigO_principal, ContinuousOn.isBigO_rev_principal, Asymptotics.IsTheta, And.intro
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
f : ℝ → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
⊢ ∃ (p : ℝ → ℝ) (q : ℝ → ℝ), MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Tactic:
h.exists_monotoneOn_sub_monotoneOn

Premises used: LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
f : ℝ → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
obtain :
  ∀ (p q : ℝ → ℝ) (hp : MonotoneOn p s) (hq : MonotoneOn q s) (h : LocallyBoundedVariationOn (p - q) s),
    ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
obtain ⟨p, q, hp, hq, rfl⟩ : ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q :=
    h.exists_monotoneOn_sub_monotoneOn

Premises used: LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn, rfl
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
h₁ :
  ∀ (x : ℝ) (hxp : x ∈ s → DifferentiableWithinAt ℝ p s x) (hxq : x ∈ s → DifferentiableWithinAt ℝ q s x) (xs : x ∈ s),
    DifferentiableWithinAt ℝ (p - q) s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x

Tactic:
filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem] with
    x hxp hxq xs

Premises used: MonotoneOn.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
x : ℝ
hxp : x ∈ s → DifferentiableWithinAt ℝ p s x
hxq : x ∈ s → DifferentiableWithinAt ℝ q s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ (p - q) s x

Tactic:
(hxp xs).sub (hxq xs)

Premises used: DifferentiableWithinAt.sub