awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
f : E → F
g : ι → E
hf : f =O[𝓝 0] id
hg : Summable (α := ℝ) fun (x : ι) ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (x : ι) ↦ ‖f (g x)‖

Tactic:
summable_of_isBigO hg <| hf.norm_norm.comp_tendsto <|
    tendsto_zero_iff_norm_tendsto_zero.2 hg.tendsto_cofinite_zero

Premises used: Iff.mpr, Asymptotics.IsBigO.norm_norm, Summable.tendsto_cofinite_zero, tendsto_zero_iff_norm_tendsto_zero, summable_of_isBigO, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
F : Type u_1
ι : Type u_2
inst : NormedRing F
inst_1 : NormMulClass F
inst_2 : NormOneClass F
inst_3 : CompleteSpace F
f g : ι → F
hf : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
c : F
hg : Tendsto g cofinite (𝓝 c)
apply : IsBigO.{u_2, u_1, 0} (E := F) (F := ℝ) cofinite (fun (n : ι) ↦ f n * g n) fun (n : ι) ↦ ‖f n‖
⊢ Summable.{u_1, u_2} (α := F) fun (n : ι) ↦ f n * g n

Tactic:
apply summable_of_isBigO hf

Premises used: summable_of_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
F : Type u_1
ι : Type u_2
inst : NormedRing F
inst_1 : NormMulClass F
inst_2 : NormOneClass F
inst_3 : CompleteSpace F
f g : ι → F
hf : Summable (α := ℝ) fun (n : ι) ↦ ‖f n‖
c : F
hg : Tendsto g cofinite (𝓝 c)
⊢ IsBigO.{u_2, u_1, 0} (E := F) (F := ℝ) cofinite (fun (n : ι) ↦ f n * g n) fun (n : ι) ↦ ‖f n‖

Tactic:
simpa using (isBigO_const_mul_self 1 f _).mul (hg.isBigO_one F)

Premises used: Filter.Tendsto.isBigO_one, Asymptotics.IsBigO.mul, Asymptotics.isBigO_const_mul_self, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
⊢ ContinuousAt (↑e : α → β) ((↑e.symm : β → α) b)

Tactic:
have := e.continuousAt (e.map_target hb)
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e : α → β) ((↑e.symm : β → α) b)
rwa :
  ∀ (this : Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 ((↑e : α → β) ((↑e.symm : β → α) b)))),
    Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)), Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)
⊢ Tendsto (↑e : α → β) (𝓝 ((↑e.symm : β → α) b)) (𝓝 b)

Tactic:
rwa [ContinuousAt, e.rightInvOn hb] at this

Premises used: ContinuousAt, OpenPartialHomeomorph.rightInvOn
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
simp :
  (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
    ∃ (c : ℝ), IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))
⊢ f =O[𝓝 b] g ↔ (f ∘ (↑e : α → β)) =O[𝓝 ((↑e.symm : β → α) b)] (g ∘ (↑e : α → β))

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
    ∃ (c : ℝ), IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))

Tactic:
exists_congr fun C => e.isBigOWith_congr hb

Premises used: exists_congr, OpenPartialHomeomorph.isBigOWith_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
    ∃ (c : ℝ), IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))

Tactic:
exact exists_congr fun C => e.isBigOWith_congr hb

Premises used: exists_congr, OpenPartialHomeomorph.isBigOWith_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))
⊢ f =o[𝓝 b] g ↔ (f ∘ (↑e : α → β)) =o[𝓝 ((↑e.symm : β → α) b)] (g ∘ (↑e : α → β))

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))

Tactic:
forall₂_congr fun c _hc => e.isBigOWith_congr hb

Premises used: forall₂_congr, OpenPartialHomeomorph.isBigOWith_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 ((↑e.symm : β → α) b)) (f ∘ (↑e : α → β)) (g ∘ (↑e : α → β))

Tactic:
exact forall₂_congr fun c _hc => e.isBigOWith_congr hb

Premises used: forall₂_congr, OpenPartialHomeomorph.isBigOWith_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
C : ℝ
⊢ IsBigOWith C (𝓝 b) f g ↔
    IsBigOWith.{u_1, u_3, u_4} (α := α) C (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
      (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
e.toOpenPartialHomeomorph.isBigOWith_congr trivial

Premises used: trivial, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.isBigOWith_congr, Homeomorph.toOpenPartialHomeomorph
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
simp :
  (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
    ∃ (c : ℝ),
      IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
        (g ∘ (⇑e : (a : α) → β) : α → F)
⊢ f =O[𝓝 b] g ↔
    IsBigO.{u_1, u_3, u_4} (α := α) (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
      (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
    ∃ (c : ℝ),
      IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
        (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
exists_congr fun C => e.isBigOWith_congr

Premises used: Homeomorph.isBigOWith_congr, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∃ (c : ℝ), IsBigOWith c (𝓝 b) f g) ↔
    ∃ (c : ℝ),
      IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
        (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
exact exists_congr fun C => e.isBigOWith_congr

Premises used: Homeomorph.isBigOWith_congr, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄,
      0 < c →
        IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
          (g ∘ (⇑e : (a : α) → β) : α → F)
⊢ f =o[𝓝 b] g ↔
    IsLittleO.{u_1, u_3, u_4} (α := α) (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
      (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄,
      0 < c →
        IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
          (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
forall₂_congr fun c _hc => e.isBigOWith_congr

Premises used: Homeomorph.isBigOWith_congr, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
E : Type u_3
inst_2 : Norm E
F : Type u_4
inst_3 : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔
    ∀ ⦃c : ℝ⦄,
      0 < c →
        IsBigOWith.{u_1, u_3, u_4} (α := α) c (𝓝 ((e.symm : (a : β) → α) b) : Filter α) (f ∘ (⇑e : (a : α) → β) : α → E)
          (g ∘ (⇑e : (a : α) → β) : α → F)

Tactic:
exact forall₂_congr fun c _hc => e.isBigOWith_congr

Premises used: Homeomorph.isBigOWith_congr, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
c : F
inst_1 : SeminormedAddGroup E
inst_2 : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
rw : ∀ x ∈ s, ‖f x‖ ≤ sSup (Norm.norm '' f '' s)
⊢ IsBigOWith.{u_1, u_2, u_3} (F := F) (sSup (Norm.norm '' f '' s) / ‖c‖) (𝓟 s) f fun (x : α) ↦ c

Tactic:
rw [isBigOWith_principal, div_mul_cancel₀ _ hc]

Premises used: div_mul_cancel₀, Asymptotics.isBigOWith_principal
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
c : F
inst_1 : SeminormedAddGroup E
inst_2 : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ ∀ x ∈ s, ‖f x‖ ≤ sSup (Norm.norm '' f '' s)

Tactic:
fun x hx ↦ hs.image_of_continuousOn hf |>.image continuous_norm
   |>.isLUB_sSup (Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩)
   |>.left <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Premises used: Iff.mpr, Set.image_nonempty, Norm.norm, IsCompact.isLUB_sSup, And.left, Set.mem_image_of_mem, IsCompact.image_of_continuousOn, Exists.intro, IsCompact.image, continuous_norm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
c : F
inst_1 : SeminormedAddGroup E
inst_2 : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ ∀ x ∈ s, ‖f x‖ ≤ sSup (Norm.norm '' f '' s)

Tactic:
exact fun x hx ↦ hs.image_of_continuousOn hf |>.image continuous_norm
   |>.isLUB_sSup (Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩)
   |>.left <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Premises used: Iff.mpr, Set.image_nonempty, Norm.norm, IsCompact.isLUB_sSup, And.left, Set.mem_image_of_mem, IsCompact.image_of_continuousOn, Exists.intro, IsCompact.image, continuous_norm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
c : F
inst_1 : SeminormedAddGroup E
inst_2 : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ IsBigO.{u_1, u_2, u_3} (F := F) (𝓟 s) f fun (x : α) ↦ c

Tactic:
(hf.isBigOWith_principal hs hc).isBigO

Premises used: ContinuousOn.isBigOWith_principal, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
⊢ IsBigOWith.{u_1, u_3, u_2} (E := F) (‖c‖ / sInf (Norm.norm '' f '' s)) (𝓟 s) (fun (x : α) ↦ c) f

Tactic:
isBigOWith_principal.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Asymptotics.isBigOWith_principal
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
refine : ∀ (x : α) (hx : x ∈ s), ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' f '' s) * ‖f x‖
⊢ IsBigOWith.{u_1, u_3, u_2} (E := F) (‖c‖ / sInf (Norm.norm '' f '' s)) (𝓟 s) (fun (x : α) ↦ c) f

Tactic:
refine isBigOWith_principal.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Asymptotics.isBigOWith_principal
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
rw : ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
⊢ ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' f '' s) * ‖f x‖

Tactic:
rw [mul_comm_div]

Premises used: mul_comm_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)

Tactic:
replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
⊢ IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))

Tactic:
have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))

Tactic:
le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
    h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Premises used: Iff.mpr, And.left, Set.mem_image_of_mem, le_mul_of_one_le_right, one_le_div, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
refine : 0 < sInf (Norm.norm '' f '' s)
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))

Tactic:
refine le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
    h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Premises used: Iff.mpr, And.left, Set.mem_image_of_mem, le_mul_of_one_le_right, one_le_div, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
obtain :
  ∀ (w : E) (hnormCx : Eq (α := ℝ) ((fun (a : E) ↦ ‖a‖) w) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))) (x : α) (hx : x ∈ s)
    (hCx : f x = w), 0 < sInf (Norm.norm '' f '' s)
⊢ 0 < sInf (Norm.norm '' f '' s)

Tactic:
obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty

Premises used: IsCompact.sInf_mem, IsGLB.nonempty
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x_1 : α
hx_1 : x_1 ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
w : E
hnormCx : Eq (α := ℝ) ((fun (a : E) ↦ ‖a‖) w) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
x : α
hx : x ∈ s
hCx : f x = w
rw : LT.lt (α := ℝ) 0 ((fun (a : E) ↦ ‖a‖) (f x))
⊢ 0 < sInf (Norm.norm '' f '' s)

Tactic:
rw [← hnormCx, ← hCx]
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x_1 : α
hx_1 : x_1 ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
w : E
hnormCx : Eq (α := ℝ) ((fun (a : E) ↦ ‖a‖) w) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
x : α
hx : x ∈ s
hCx : f x = w
⊢ LT.lt (α := ℝ) 0 ((fun (a : E) ↦ ‖a‖) (f x))

Tactic:
(norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)

Premises used: Iff.mpr, Ne.symm, norm_ne_zero_iff, Ne.lt_of_le, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x_1 : α
hx_1 : x_1 ∈ s
hs : IsCompact (X := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB (α := ℝ) ((fun (a : E) ↦ ‖a‖) '' f '' s) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
w : E
hnormCx : Eq (α := ℝ) ((fun (a : E) ↦ ‖a‖) w) (sInf ((fun (a : E) ↦ ‖a‖) '' f '' s))
x : α
hx : x ∈ s
hCx : f x = w
⊢ LT.lt (α := ℝ) 0 ((fun (a : E) ↦ ‖a‖) (f x))

Tactic:
exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)

Premises used: Iff.mpr, Ne.symm, norm_ne_zero_iff, Ne.lt_of_le, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace α
s : Set α
f : α → E
inst_1 : NormedAddGroup E
inst_2 : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
⊢ IsBigO.{u_1, u_3, u_2} (E := F) (𝓟 s) (fun (x : α) ↦ c) f

Tactic:
(hf.isBigOWith_rev_principal hs hC c).isBigO

Premises used: ContinuousOn.isBigOWith_rev_principal, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
l : Filter ι
ε : ι → 𝕜
f : ι → E
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
rw :
  ∀ (hε : IsLittleO (F := 𝕜) l ε fun (_x : ι) ↦ 1) (hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)),
    IsLittleO.{u_1, u_3, u_2} (F := 𝕜) l (ε • f) fun (_x : ι) ↦ 1
⊢ Tendsto (ε • f) l (𝓝 0)

Tactic:
rw [← isLittleO_one_iff 𝕜] at hε ⊢

Premises used: Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
l : Filter ι
ε : ι → 𝕜
f : ι → E
hε : IsLittleO (F := 𝕜) l ε fun (_x : ι) ↦ 1
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
⊢ IsLittleO.{u_1, u_3, u_2} (F := 𝕜) l (ε • f) fun (_x : ι) ↦ 1

Tactic:
simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))

Premises used: Filter.IsBoundedUnder.isBigO_const, Asymptotics.IsLittleO.smul_isBigO, one_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
R : Type u_1
inst : ConditionallyCompleteLattice R
inst_1 : Div R
inst_2 : NatCast R
u v : ℕ → R
h : u =ᶠ[atTop] v
⊢ linearGrowthInf u = linearGrowthInf v

Tactic:
liminf_congr (h.mono fun _ uv ↦ uv ▸ rfl)

Premises used: Eq.rec, Filter.liminf_congr, Filter.Eventually.mono, LinearGrowth.linearGrowthInf, rfl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
R : Type u_1
inst : ConditionallyCompleteLattice R
inst_1 : Div R
inst_2 : NatCast R
u v : ℕ → R
h : u =ᶠ[atTop] v
⊢ linearGrowthSup u = linearGrowthSup v

Tactic:
limsup_congr (h.mono fun _ uv ↦ uv ▸ rfl)

Premises used: Eq.rec, Filter.Eventually.mono, LinearGrowth.linearGrowthSup, Filter.limsup_congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
R : Type u_1
inst : ConditionallyCompleteLattice R
inst_1 : Div R
inst_2 : NatCast R
u : ℕ → R
h : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ u n / (↑n : R)
h' : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ u n / (↑n : R)
⊢ linearGrowthInf u ≤ linearGrowthSup u

Tactic:
liminf_le_limsup h h'

Premises used: LinearGrowth.linearGrowthSup, LinearGrowth.linearGrowthInf, Filter.liminf_le_limsup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : u ≤ᶠ[atTop] v
⊢ linearGrowthInf u ≤ linearGrowthInf v

Tactic:
liminf_le_liminf (h.mono fun n u_v ↦ EReal.monotone_div_right_of_nonneg n.cast_nonneg' u_v)

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Filter.Eventually.mono, LinearGrowth.linearGrowthInf, Filter.liminf_le_liminf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : u ≤ v
⊢ linearGrowthInf u ≤ linearGrowthInf v

Tactic:
linearGrowthInf_eventually_monotone (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, LinearGrowth.linearGrowthInf_eventually_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : u ≤ᶠ[atTop] v
⊢ linearGrowthSup u ≤ linearGrowthSup v

Tactic:
limsup_le_limsup (h.mono fun n u_v ↦ monotone_div_right_of_nonneg n.cast_nonneg' u_v)

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Filter.Eventually.mono, LinearGrowth.linearGrowthSup, Filter.limsup_le_limsup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : u ≤ v
⊢ linearGrowthSup u ≤ linearGrowthSup v

Tactic:
linearGrowthSup_eventually_monotone (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, LinearGrowth.linearGrowthSup_eventually_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
h₁ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ u n / (↑n : EReal) ≤ v n / (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
rw : (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
⊢ linearGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)

Tactic:
rw [linearGrowthInf, liminf_le_iff']

Premises used: Filter.liminf_le_iff', LinearGrowth.linearGrowthInf