awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (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)
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
h₂ : f i =o[l] g i ∨ ∃ x ∈ L, f x =o[l] g x
cons :
  ∀ (hi : f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
cons₁ :
  ∀ (hL : ∃ x ∈ L, f x =o[l] g x),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
    (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
    g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

Premises used: Asymptotics.IsBigO.mul_isLittleO, And.left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
L : List ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ L, f i =O[l] g i
h₂ : ∃ i ∈ L, f i =o[l] g i
nil :
  ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i =O[l] g i)
    (h₂ : ∃ (i : ι), Membership.mem (γ := List ι) [] i ∧ f i =o[l] g i),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) []))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) [])
cons :
  ∀ (i : ι) (L : List ι)
    (ihL :
      ∀ (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i),
        IsLittleO.{u_1, u_13, u_15} (E := R) (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))
    (h₁ : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1) (h₂ : ∃ i_1 ∈ i :: L, f i_1 =o[l] g i_1),
    IsLittleO.{u_1, u_13, u_15} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (i :: L))) fun (x : α) ↦
      List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) (i :: L))
⊢ IsLittleO.{u_1, u_13, u_15} (E := R) (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:
induction L with
  | nil => simp at h₂
  | cons i L ihL =>
    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢
    cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

Premises used: List.map_cons, List.forall_mem_cons, List.prod_cons, List.exists_mem_cons_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
⊢ ∃ (l : List ι), (↑l : Multiset ι) = s

Tactic:
Quotient.mk_surjective s

Premises used: Multiset, Multiset.ofList, Quotient.mk_surjective
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
obtain :
  ∀ (l_1 : List ι) (h₁ : ∀ i ∈ (↑l_1 : Multiset ι), f i =O[l] g i) (h₂ : ∃ i ∈ (↑l_1 : Multiset ι), f i =o[l] g i),
    IsLittleO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l
      (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l_1 : Multiset ι))) fun (x : α) ↦
      Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l_1 : Multiset ι))
⊢ IsLittleO.{u_1, u_18, u_19} (E := R) (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:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s

Premises used: List, Quotient.mk_surjective, rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l_1 : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
h₁ : ∀ i ∈ (↑l : Multiset ι), f i =O[l_1] g i
h₂ : ∃ i ∈ (↑l : Multiset ι), f i =o[l_1] g i
⊢ IsLittleO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l_1
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l : Multiset ι))) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l : Multiset ι))

Tactic:
mod_cast IsLittleO.listProd h₁ h₂

Premises used: Multiset.map, Multiset.prod, cast, Multiset.ofList, Asymptotics.IsLittleO.listProd, Asymptotics.IsLittleO, Eq.refl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l_1 : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
h₁ : ∀ i ∈ (↑l : Multiset ι), f i =O[l_1] g i
h₂ : ∃ i ∈ (↑l : Multiset ι), f i =o[l_1] g i
⊢ IsLittleO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l_1
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l : Multiset ι))) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l : Multiset ι))

Tactic:
exact mod_cast IsLittleO.listProd h₁ h₂

Premises used: Asymptotics.IsLittleO.listProd
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst : SeminormedCommRing R
inst_1 : NormedField 𝕜
s : Finset ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
⊢ IsLittleO.{u_1, u_18, u_19} (E := R) (F := 𝕜) l (fun (x : α) ↦ ∏ i ∈ s, f i x) fun (x : α) ↦ ∏ i ∈ s, g i x

Tactic:
.multisetProd h₁ h₂

Premises used: Asymptotics.IsLittleO.multisetProd, Finset.prod
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
⊢ IsLittleO.{u_1, u_15, u_15} (E := 𝕜) (F := 𝕜) l (fun (x : α) ↦ f x / g x) fun (x : α) ↦ g x / g x

Tactic:
simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)

Premises used: div_eq_mul_inv, Asymptotics.IsLittleO.mul_isBigO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
x : α
⊢ ‖g x / g x‖ ≤ norm.{u_15} (E := 𝕜) 1

Tactic:
simp [div_self_le_one]

Premises used: div_self_le_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
x : IsLittleO.{u_1, u_15, u_15} (E := 𝕜) (F := 𝕜) l (fun (x : α) ↦ f x / g x) fun (x : α) ↦ g x / g x
⊢ IsLittleO.{u_1, u_15, u_15} (E := 𝕜) (F := 𝕜) l (fun (x : α) ↦ f x / g x) fun (_x : α) ↦ 1

Tactic:
calc
      (fun x => f x / g x) =o[l] fun x => g x / g x := by
        simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)
      _ =O[l] fun _x => (1 : 𝕜) := isBigO_of_le _ fun x => by simp [div_self_le_one]

Premises used: HDiv.hDiv, Asymptotics.isBigO_of_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst : SeminormedAddCommGroup E'
inst_1 : NormedDivisionRing 𝕜
inst_2 : Module 𝕜 E'
inst_3 : NormSMulClass 𝕜 E'
f : α → E'
g : α → 𝕜
l : Filter α
h : f =o[l] g
⊢ Tendsto.{u_1, u_6} (β := E') (fun (x : α) ↦ (g x)⁻¹ • f x) l (𝓝 0)

Tactic:
simpa only [div_eq_inv_mul, ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero] using
    h.norm_norm.tendsto_div_nhds_zero

Premises used: norm_smul, Asymptotics.IsLittleO.tendsto_div_nhds_zero, norm_inv, tendsto_zero_iff_norm_tendsto_zero, Asymptotics.IsLittleO.norm_norm, div_eq_inv_mul
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =o[l] g ↔ Tendsto.{u_1, u_15} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)

Tactic:
⟨IsLittleO.tendsto_div_nhds_zero, fun h =>
    (((isLittleO_one_iff _).mpr h).mul_isBigO (isBigO_refl g l)).congr'
      (hgf.mono fun _x => div_mul_cancel_of_imp) (Eventually.of_forall fun _x => one_mul _)⟩

Premises used: Iff.mpr, div_mul_cancel_of_imp, Asymptotics.IsLittleO.tendsto_div_nhds_zero, Filter.Eventually.of_forall, Filter.Eventually.mono, Asymptotics.IsLittleO.congr', Iff.intro, Asymptotics.isLittleO_one_iff, Asymptotics.IsLittleO.mul_isBigO, one_mul, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
hgf : ∀ (x : α), g x = 0 → f x = 0
⊢ f =o[l] g ↔ Tendsto.{u_1, u_15} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)

Tactic:
isLittleO_iff_tendsto' (Eventually.of_forall hgf)

Premises used: Filter.Eventually.of_forall, Asymptotics.isLittleO_iff_tendsto'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst : Norm F
inst_1 : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
simp : IsLittleO.{u_1, u_9, u_4} (E := E'') l (fun (_x : α) ↦ c) g ↔ IsLittleO (E := ℝ) l (fun (_x : α) ↦ 1) g
⊢ IsLittleO.{u_1, u_9, u_4} (E := E'') l (fun (_x : α) ↦ c) g ↔ Tendsto (β := ℝ) (fun (x : α) ↦ ‖g x‖) l atTop

Tactic:
simp only [← isLittleO_one_left_iff ℝ]

Premises used: Real, Asymptotics.isLittleO_one_left_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst : Norm F
inst_1 : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ IsLittleO.{u_1, u_9, u_4} (E := E'') l (fun (_x : α) ↦ c) g ↔ IsLittleO (E := ℝ) l (fun (_x : α) ↦ 1) g

Tactic:
⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
    (isBigO_const_one ℝ c l).trans_isLittleO⟩

Premises used: Real, Asymptotics.isBigO_const_one, Asymptotics.isBigO_const_const, Iff.intro, Asymptotics.IsBigO.trans_isLittleO, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst : Norm F
inst_1 : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ IsLittleO.{u_1, u_9, u_4} (E := E'') l (fun (_x : α) ↦ c) g ↔ IsLittleO (E := ℝ) l (fun (_x : α) ↦ 1) g

Tactic:
exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
    (isBigO_const_one ℝ c l).trans_isLittleO⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
inl :
  IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ 0) g'' ↔
    Eq.{u_9 + 1} (α := E'') 0 0 ∨ Tendsto (norm ∘ g'') l atTop
inr :
  ∀ (hc : c ≠ 0), IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop
⊢ IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ 0) g'' ↔
    Eq.{u_9 + 1} (α := E'') 0 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
simp only [isLittleO_zero, true_or]

Premises used: true_or, Asymptotics.isLittleO_zero
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
inr : Tendsto (β := ℝ) (fun (x : α) ↦ ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop
⊢ IsLittleO.{u_1, u_9, u_10} (E := E'') l (fun (_x : α) ↦ c) g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
simp only [hc, false_or, isLittleO_const_left_of_ne hc]

Premises used: false_or, Asymptotics.isLittleO_const_left_of_ne
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop

Tactic:
rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
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
d : E''
c : F''
⊢ ¬Tendsto (Function.const α ‖c‖) l atTop

Tactic:
have : ¬Tendsto (Function.const α ‖c‖) l atTop :=
    not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
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
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
simp : Tendsto (Function.comp.{u_1 + 1, u_10 + 1, 1} (β := F'') norm fun (_x : α) ↦ c) l atTop → d = 0
⊢ (IsLittleO.{u_1, u_9, u_10} (E := E'') (F := F'') l (fun (_x : α) ↦ d) fun (_x : α) ↦ c) ↔ d = 0

Tactic:
simp only [isLittleO_const_left, or_iff_left_iff_imp]

Premises used: Asymptotics.isLittleO_const_left, or_iff_left_iff_imp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
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
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ Tendsto (Function.comp.{u_1 + 1, u_10 + 1, 1} (β := F'') norm fun (_x : α) ↦ c) l atTop → d = 0

Tactic:
fun h => (this h).elim

Premises used: False.elim
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
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
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ Tendsto (Function.comp.{u_1 + 1, u_10 + 1, 1} (β := F'') norm fun (_x : α) ↦ c) l atTop → d = 0

Tactic:
exact fun h => (this h).elim

Premises used: False.elim
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
x : α
⊢ f'' =o[pure x] g'' ↔ f'' x = 0

Tactic:
calc
    f'' =o[pure x] g'' ↔ (fun _y : α => f'' x) =o[pure x] fun _ => g'' x := isLittleO_congr rfl rfl
    _ ↔ f'' x = 0 := isLittleO_const_const_iff

Premises used: Asymptotics.isLittleO_congr, Trans.trans, Asymptotics.isLittleO_const_const_iff, rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
c : F''
⊢ IsLittleO.{u_9, u_10, u_9} (E := F'') (Bornology.cobounded E'') (fun (x : E'') ↦ c) id

Tactic:
isLittleO_const_left.2 <| .inr tendsto_norm_cobounded_atTop

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, tendsto_norm_cobounded_atTop, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
inst : NormedAddCommGroup E''
c : E''
⊢ IsLittleO.{0, u_9, 0} (E := E'') atTop (fun (_x : ℝ) ↦ c) id

Tactic:
isLittleO_const_left.2 <| Or.inr tendsto_abs_atTop_atTop

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, Filter.tendsto_abs_atTop_atTop, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
inst : NormedAddCommGroup E''
c : E''
⊢ IsLittleO.{0, u_9, 0} (E := E'') atBot (fun (_x : ℝ) ↦ c) id

Tactic:
isLittleO_const_left.2 <| Or.inr tendsto_abs_atBot_atTop

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, Filter.tendsto_abs_atBot_atTop, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
a : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)
⊢ f =o[l] g

Tactic:
apply Asymptotics.isLittleO_of_tendsto'

Premises used: Asymptotics.isLittleO_of_tendsto'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
hgf : ∀ (x : α), 1 ≤ g x / f x → g x = 0 → f x = 0
⊢ ∀ᶠ (x : α) in l, g x = 0 → f x = 0

Tactic:
apply (Filter.Tendsto.eventually_ge_atTop h 1).mono

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h_1 : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
x : α
h : 1 ≤ g x / f x
h0 : g x = 0
⊢ LE.le.{u_17} (α := 𝕜) 1 0

Tactic:
simp only [h0, zero_div] at h

Premises used: zero_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h_1 : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
x : α
h0 : g x = 0
h : LE.le.{u_17} (α := 𝕜) 1 0
⊢ f x = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
⊢ Tendsto.{u_1, u_17} (β := 𝕜) ((fun (r : 𝕜) ↦ r⁻¹) ∘ fun (x : α) ↦ g x / f x) l (𝓝 0)

Tactic:
Tendsto.comp tendsto_inv_atTop_zero h

Premises used: tendsto_inv_atTop_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
h₁ : ∀ (x : α), f x / g x = ((fun (r : 𝕜) ↦ r⁻¹) ∘ fun (x : α) ↦ g x / f x) x
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ f x / g x) l (𝓝 0)

Tactic:
convert! Tendsto.comp tendsto_inv_atTop_zero h

Premises used: tendsto_inv_atTop_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atTop
x : α
⊢ f x / g x = ((fun (r : 𝕜) ↦ r⁻¹) ∘ fun (x : α) ↦ g x / f x) x

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
⊢ f =o[l] g

Tactic:
IsLittleO.of_neg_left (IsLittleO.of_tendsto_div_atTop ?_)

Premises used: Asymptotics.IsLittleO.of_neg_left, Asymptotics.IsLittleO.of_tendsto_div_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
refine : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / -f x) l atTop
⊢ f =o[l] g

Tactic:
refine IsLittleO.of_neg_left (IsLittleO.of_tendsto_div_atTop ?_)

Premises used: Asymptotics.IsLittleO.of_neg_left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
rw : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ -(g x / -f x)) l atBot
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / -f x) l atTop

Tactic:
rw [← tendsto_neg_atBot_iff]

Premises used: Filter.tendsto_neg_atBot_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot

Tactic:
h
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
h₁ : ∀ (x : α), -(g x / -f x) = g x / f x
⊢ Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ -(g x / -f x)) l atBot

Tactic:
convert! h using 2
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_17
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto.{u_1, u_17} (β := 𝕜) (fun (x : α) ↦ g x / f x) l atBot
x : α
⊢ -(g x / -f x) = g x / f x

Tactic:
simp [div_neg_eq_neg_div]

Premises used: div_neg_eq_neg_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
simp : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ IsBigOWith c l u v

Tactic:
simp only [IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖

Tactic:
h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)

Premises used: Norm.norm, HMul.hMul, LE.le, Filter.Eventually.mono, Filter.EventuallyEq.rw, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
refine : ∀ (x : α) (hx : ‖φ x‖ ≤ c), (fun (x : α) (a : R) ↦ ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖

Tactic:
refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)

Premises used: Norm.norm, HMul.hMul, LE.le, Filter.Eventually.mono, Filter.EventuallyEq.rw, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
simp : ‖φ x * v x‖ ≤ c * ‖v x‖
⊢ (fun (x : α) (a : R) ↦ ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)

Tactic:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x * v x‖ ≤ c * ‖v x‖

Tactic:
(norm_mul_le _ _).trans ?_

Premises used: LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
refine : ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖
⊢ ‖φ x * v x‖ ≤ c * ‖v x‖

Tactic:
refine (norm_mul_le _ _).trans ?_

Premises used: LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
R : Type u_13
inst : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
ha : 0 ≤ ‖v x‖
⊢ ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖

Tactic:
gcongr