awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
s : Set α
simp_rw : (∃ (c : ℝ), ∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ (c : ℝ), ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[𝓟 s] g ↔ ∃ (c : ℝ), ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp_rw [isBigO_iff, eventually_principal]

Premises used: Asymptotics.isBigO_iff, Filter.eventually_principal
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Tactic:
⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩

Premises used: norm_le_zero_iff, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
refine_1 : ∀ (h : f'' =o[𝓟 s] g') (x : α) (hx : x ∈ s), ‖f'' x‖ ≤ 0
refine_2 : ∀ (h : ∀ x ∈ s, f'' x = 0), f'' =o[𝓟 s] g'
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Tactic:
refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : f'' =o[𝓟 s] g'
x : α
hx : x ∈ s
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖

Tactic:
simp only [isLittleO_iff] at h

Premises used: Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
⊢ Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)

Tactic:
have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
      ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
        inf_le_left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
refine_1 : EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ ‖f'' x‖) fun (c : ℝ) ↦ c * ‖g' x‖
⊢ ‖f'' x‖ ≤ 0

Tactic:
apply le_of_tendsto_of_tendsto tendsto_const_nhds this

Premises used: tendsto_const_nhds, le_of_tendsto_of_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
apply :
  ∀ (c : ℝ) (hc : Membership.mem (γ := Set ℝ) (Ioi 0) c),
    LE.le (α := ℝ) ((fun (x_1 : ℝ) ↦ ‖f'' x‖) c) ((fun (c : ℝ) ↦ c * ‖g' x‖) c)
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ ‖f'' x‖) fun (c : ℝ) ↦ c * ‖g' x‖

Tactic:
apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))

Premises used: Iff.mpr, Filter.Eventually.of_forall, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
c : ℝ
hc : Membership.mem (γ := Set ℝ) (Ioi 0) c
⊢ LE.le (α := ℝ) ((fun (x_1 : ℝ) ↦ ‖f'' x‖) c) ((fun (c : ℝ) ↦ c * ‖g' x‖) c)

Tactic:
eventually_principal.1 (h hc) x hx

Premises used: Filter.eventually_principal, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
c : ℝ
hc : Membership.mem (γ := Set ℝ) (Ioi 0) c
⊢ LE.le (α := ℝ) ((fun (x_1 : ℝ) ↦ ‖f'' x‖) c) ((fun (c : ℝ) ↦ c * ‖g' x‖) c)

Tactic:
exact eventually_principal.1 (h hc) x hx

Premises used: Filter.eventually_principal, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
apply : (fun (_x : α) ↦ 0) =ᶠ[𝓟 s] f''
⊢ f'' =o[𝓟 s] g'

Tactic:
apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl

Premises used: Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.congr', Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ (fun (_x : α) ↦ 0) =ᶠ[𝓟 s] f''

Tactic:
fun x hx ↦ (h x hx).symm

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.Subset, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ (fun (_x : α) ↦ 0) =ᶠ[𝓟 s] f''

Tactic:
exact fun x hx ↦ (h x hx).symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
rw : (∀ᶠ (x : α) in ⊤, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
rw₁ rw₂ : (∀ (x : α), ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def, eventually_top]

Premises used: Asymptotics.IsBigOWith_def, Filter.eventually_top
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
simp_rw : (∃ (c : ℝ), ∀ᶠ (x : α) in ⊤, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
⊢ f =O[⊤] g ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp_rw [isBigO_iff, eventually_top]

Premises used: Asymptotics.isBigO_iff, Filter.eventually_top
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
⊢ f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0

Tactic:
simp only [← principal_univ, isLittleO_principal, mem_univ, forall_true_left]

Premises used: forall_true_left, Filter.principal_univ, Asymptotics.isLittleO_principal, Set.mem_univ
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : One F
inst_3 : NormOneClass F
c : E
l : Filter α
⊢ IsBigOWith.{u_1, u_3, u_4} (E := E) (F := F) ‖c‖ l (fun (_x : α) ↦ c) fun (_x : α) ↦ 1

Tactic:
simp [isBigOWith_iff]

Premises used: Asymptotics.isBigOWith_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : One F
inst_3 : NormOneClass F
c : E
l : Filter α
⊢ IsBigO.{u_1, u_3, u_4} (E := E) (F := F) l (fun (_x : α) ↦ c) fun (_x : α) ↦ 1

Tactic:
(isBigOWith_const_one F c l).isBigO

Premises used: Asymptotics.IsBigOWith.isBigO, Asymptotics.isBigOWith_const_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
F'' : Type u_10
inst : Norm E
inst_1 : Norm F
inst_2 : NormedAddCommGroup F''
f : α → E
l : Filter α
inst_3 : One F
inst_4 : NormOneClass F
c : F''
hc : c ≠ 0
⊢ (IsLittleO.{u_1, u_3, u_10} (F := F'') l f fun (_x : α) ↦ c) ↔ IsLittleO.{u_1, u_3, u_4} (F := F) l f fun (_x : α) ↦ 1

Tactic:
⟨fun h => h.trans_isBigOWith (isBigOWith_const_one _ _ _) (norm_pos_iff.2 hc),
   fun h => h.trans_isBigO <| isBigO_const_const _ hc _⟩

Premises used: Iff.mpr, norm_pos_iff, Asymptotics.IsLittleO.trans_isBigOWith, Asymptotics.isBigO_const_const, Iff.intro, OfNat.ofNat, Asymptotics.IsLittleO.trans_isBigO, Asymptotics.isBigOWith_const_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E''' : Type u_12
inst : Norm F
inst_1 : SeminormedAddGroup E'''
l : Filter α
inst_2 : One F
inst_3 : NormOneClass F
f : α → E'''
⊢ (IsLittleO.{u_1, u_12, u_4} (F := F) l f fun (_x : α) ↦ 1) ↔ Tendsto f l (𝓝 0)

Tactic:
simp only [isLittleO_iff, norm_one, mul_one, Metric.nhds_basis_closedBall.tendsto_right_iff,
    Metric.mem_closedBall, dist_zero_right]

Premises used: NormOneClass.norm_one, Metric.mem_closedBall, Asymptotics.isLittleO_iff, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall, mul_one, dist_zero_right
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
l : Filter α
inst_2 : One F
inst_3 : NormOneClass F
⊢ (IsBigO.{u_1, u_3, u_4} (F := F) l f fun (_x : α) ↦ 1) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x‖

Tactic:
simp only [isBigO_iff, norm_one, mul_one, IsBoundedUnder, IsBounded, eventually_map]

Premises used: Asymptotics.isBigO_iff, NormOneClass.norm_one, Filter.IsBounded, Filter.eventually_map, mul_one, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
l : Filter α
inst_2 : One F
inst_3 : NormOneClass F
_x : α
⊢ 0 ≤ norm.{u_4} (E := F) 1

Tactic:
simp only [norm_one, zero_le_one]

Premises used: NormOneClass.norm_one, zero_le_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
l : Filter α
inst_2 : One F
inst_3 : NormOneClass F
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * norm.{u_4} (E := F) 1 ≤ ‖f x‖) ↔
    ∀ (n : ℕ), True → ∀ᶠ (x : α) in l, Membership.mem (γ := Set ℝ) (Ici (↑n : ℝ)) ‖f x‖

Tactic:
simp only [norm_one, mul_one, true_imp_iff, mem_Ici]

Premises used: NormOneClass.norm_one, true_imp_iff, Set.mem_Ici, mul_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
inst_2 : One F
inst_3 : NormOneClass F
c : E'
h : Tendsto f' l (𝓝 c)
⊢ IsBigO.{u_1, u_6, u_4} (F := F) l f' fun (_x : α) ↦ 1

Tactic:
h.norm.isBoundedUnder_le.isBigO_one F

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.Tendsto.norm, Filter.IsBoundedUnder.isBigO_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
F' : Type u_7
inst : Norm E
inst_1 : Norm F
inst_2 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
inst_3 : One F
inst_4 : NormOneClass F
hfg : f =O[l] g'
y : F'
hg : Tendsto g' l (𝓝 y)
⊢ IsBigO.{u_1, u_3, u_4} (F := F) l f fun (_x : α) ↦ 1

Tactic:
hfg.trans <| hg.isBigO_one F

Premises used: Filter.Tendsto.isBigO_one, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
⊢ (IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1) ↔ IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.mono nhdsWithin_le_nhds⟩

Premises used: nhdsWithin_le_nhds, Asymptotics.IsBigO.mono, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
refine :
  ∀ (h : IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1),
    IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1
⊢ (IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1) ↔ IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.mono nhdsWithin_le_nhds⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
h : IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1
simp : ∀ (h : ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b), ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
⊢ IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1

Tactic:
simp only [isBigO_one_iff, IsBoundedUnder, IsBounded, eventually_map] at h ⊢

Premises used: Asymptotics.isBigO_one_iff, Filter.IsBounded, Filter.eventually_map, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
h : ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b
obtain : ∀ (c : ℝ) (hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c), ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
⊢ ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
h : ∀ᶠ (a_1 : α) in 𝓝 a, ‖f a_1‖ ≤ max c ‖f a‖
⊢ ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b

Tactic:
use max c ‖f a‖

Premises used: Norm.norm, Max.max
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
h : ∀ (b : α) (hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c), ‖f b‖ ≤ max c ‖f a‖
⊢ ∀ᶠ (a_1 : α) in 𝓝 a, ‖f a_1‖ ≤ max c ‖f a‖

Tactic:
filter_upwards [eventually_nhdsWithin_iff.mp hc] with b hb

Premises used: eventually_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c
h : ∀ (hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c) (hb : Membership.mem (γ := Set α) {b}ᶜ b → ‖f b‖ ≤ c), ‖f b‖ ≤ max c ‖f b‖
h₁ : ∀ (hb' : b ≠ a), ‖f b‖ ≤ max c ‖f a‖
⊢ ‖f b‖ ≤ max c ‖f a‖

Tactic:
rcases eq_or_ne b a with rfl | hb'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
c : ℝ
b : α
hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c
hb : Membership.mem (γ := Set α) {b}ᶜ b → ‖f b‖ ≤ c
⊢ ‖f b‖ ≤ max c ‖f b‖

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c
hb' : b ≠ a
⊢ ‖f b‖ ≤ max c ‖f a‖

Tactic:
(hb hb').trans (le_max_left ..)

Premises used: LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c
hb' : b ≠ a
⊢ ‖f b‖ ≤ max c ‖f a‖

Tactic:
exact (hb hb').trans (le_max_left ..)

Premises used: LE.le.trans, le_max_left
-- 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''
l : Filter α
c : F''
hc : c ≠ 0
⊢ (IsLittleO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c) ↔ Tendsto f'' l (𝓝 0)

Tactic:
(isLittleO_const_iff_isLittleO_one ℝ hc).trans (isLittleO_one_iff _)

Premises used: Real, Asymptotics.isLittleO_const_iff_isLittleO_one, Iff.trans, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
c : F''
hc : c ≠ 0
⊢ IsLittleO.{u_9, u_9, u_10} (E := E'') (F := F'') (𝓝 0) (fun (x : E'') ↦ x) fun (_x : E'') ↦ c

Tactic:
(isLittleO_const_iff hc).mpr (continuous_id.tendsto 0)

Premises used: Iff.mpr, Asymptotics.isLittleO_const_iff, Continuous.tendsto, continuous_id, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
f : α → E
l : Filter α
h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
c : F''
hc : c ≠ 0
⊢ IsBigO.{u_1, u_3, u_10} (F := F'') l f fun (_x : α) ↦ c

Tactic:
(h.isBigO_one ℝ).trans (isBigO_const_const _ hc _)

Premises used: Real, Asymptotics.isBigO_const_const, Asymptotics.IsBigO.trans, Filter.IsBoundedUnder.isBigO_one
-- 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''
l : Filter α
y : E''
h : Tendsto f'' l (𝓝 y)
c : F''
hc : c ≠ 0
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c

Tactic:
h.norm.isBoundedUnder_le.isBigO_const hc

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.IsBoundedUnder.isBigO_const, Filter.Tendsto.norm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
l : Filter α
c : F
h : IsBigO.{u_1, u_3, u_4} (F := F) l f fun (_x : α) ↦ c
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)

Tactic:
let ⟨c', hc'⟩ := h.bound
  ⟨c' * ‖c‖, eventually_map.2 hc'⟩

Premises used: Iff.mpr, Norm.norm, HMul.hMul, _private.0.Asymptotics.IsBigO.isBoundedUnder_le.match_1, Function.comp, LE.le, Filter.eventually_map, Asymptotics.IsBigO.bound, Exists.intro, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
f : α → E
l : Filter α
c : F''
hc : c ≠ 0
⊢ (IsBigO.{u_1, u_3, u_10} (F := F'') l f fun (_x : α) ↦ c) ↔ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)

Tactic:
⟨fun h => h.isBoundedUnder_le, fun h => h.isBigO_const hc⟩

Premises used: Filter.IsBoundedUnder.isBigO_const, Iff.intro, Asymptotics.IsBigO.isBoundedUnder_le
-- 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''
l : Filter α
c : F''
h : IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
hc : c = 0
rwa rwa₁ rwa₂ rwa₃ : IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ 0

Tactic:
rwa [← hc]
-- 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''
l : Filter α
c : F''
refine :
  ((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖) →
    IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
⊢ (IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c) ↔
    (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖

Tactic:
refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩
-- 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''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
inl : ∀ (hc : c = 0), IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
inr : ∀ (hc : c ≠ 0), IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c

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

Premises used: eq_or_ne, OfNat.ofNat
-- 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''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
hc : c = 0
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c

Tactic:
(hcf hc).trans_isBigO (isBigO_zero _ _)

Premises used: Asymptotics.isBigO_zero, Filter.EventuallyEq.trans_isBigO
-- 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''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
hc : c ≠ 0
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c

Tactic:
hf.isBigO_const hc

Premises used: Filter.IsBoundedUnder.isBigO_const
-- 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''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
hc : c = 0
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c

Tactic:
exacts [(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc]

Premises used: Asymptotics.isBigO_zero, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
simp : (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g'' x‖) ↔ ∃ (b : ℝ), ∀ᶠ (a : α) in l, ‖f a‖ / ‖g'' a‖ ≤ b
⊢ f =O[l] g'' ↔ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x‖ / ‖g'' x‖

Tactic:
simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]

Premises used: Asymptotics.isBigO_iff, Filter.IsBounded, Filter.eventually_map, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g'' x‖) ↔ ∃ (b : ℝ), ∀ᶠ (a : α) in l, ‖f a‖ / ‖g'' a‖ ≤ b

Tactic:
exists_congr fun c =>
      eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, Filter.Eventually.mono, exists_congr, Filter.eventually_congr, Iff.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g'' x‖) ↔ ∃ (b : ℝ), ∀ᶠ (a : α) in l, ‖f a‖ / ‖g'' a‖ ≤ b

Tactic:
exact
    exists_congr fun c =>
      eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, Filter.Eventually.mono, exists_congr, Filter.eventually_congr, Iff.symm
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
mp : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f' → ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
mpr : (∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
⊢ IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f' ↔ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
constructor