awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m n : ℕ
h : m < n
rcases :
  ∀ (p : ℕ) (hp0 : 0 < p) (h : m < m + p),
    IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ (m + p)) fun (x : 𝕜) ↦ x ^ m
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ n) fun (x : 𝕜) ↦ x ^ m

Tactic:
rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩

Premises used: lt_iff_exists_add, Iff.mp, rfl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ m * x ^ p) fun (x : 𝕜) ↦ x ^ m * HPow.hPow (α := 𝕜) 1 p
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ (m + p)) fun (x : 𝕜) ↦ x ^ m

Tactic:
simpa only [pow_add, one_pow, mul_one]

Premises used: one_pow, pow_add, mul_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
suffices : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ m * x ^ p) fun (x : 𝕜) ↦ x ^ m * HPow.hPow (α := 𝕜) 1 p
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ (m + p)) fun (x : 𝕜) ↦ x ^ m

Tactic:
suffices (fun x : 𝕜 => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p by
    simpa only [pow_add, one_pow, mul_one]
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ m * x ^ p) fun (x : 𝕜) ↦ x ^ m * HPow.hPow (α := 𝕜) 1 p

Tactic:
IsBigO.mul_isLittleO (isBigO_refl _ _)
    (IsLittleO.pow ((isLittleO_one_iff _).2 tendsto_id) hp0)

Premises used: Asymptotics.IsLittleO.pow, Asymptotics.IsBigO.mul_isLittleO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ m * x ^ p) fun (x : 𝕜) ↦ x ^ m * HPow.hPow (α := 𝕜) 1 p

Tactic:
exact IsBigO.mul_isLittleO (isBigO_refl _ _)
    (IsLittleO.pow ((isLittleO_one_iff _).2 tendsto_id) hp0)

Premises used: Asymptotics.IsLittleO.pow, Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
m n : ℕ
h : m < n
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ ‖x‖ ^ m

Tactic:
(isLittleO_pow_pow h).comp_tendsto tendsto_norm_zero

Premises used: Asymptotics.isLittleO_pow_pow, Asymptotics.IsLittleO.comp_tendsto, tendsto_norm_zero
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ n) fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 1

Tactic:
isLittleO_pow_pow h (𝕜 := 𝕜)

Premises used: Asymptotics.isLittleO_pow_pow
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
h₁ : ∀ (x : 𝕜), x = HPow.hPow (β := ℕ) x 1
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (x : 𝕜) ↦ x ^ n) fun (x : 𝕜) ↦ x

Tactic:
convert! isLittleO_pow_pow h (𝕜 := 𝕜)

Premises used: Asymptotics.isLittleO_pow_pow
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
x : 𝕜
⊢ x = HPow.hPow (β := ℕ) x 1

Tactic:
simp only [pow_one]

Premises used: pow_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ HPow.hPow (β := ℕ) ‖x‖ 1

Tactic:
have := @isLittleO_norm_pow_norm_pow E' _ _ _ h
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ HPow.hPow (β := ℕ) ‖x‖ 1
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ ‖x‖

Tactic:
simp only [pow_one] at this

Premises used: pow_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ ‖x‖
⊢ IsLittleO (E := ℝ) (F := E') (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ x

Tactic:
isLittleO_norm_right.mp this

Premises used: Asymptotics.isLittleO_norm_right, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ ‖x‖
⊢ IsLittleO (E := ℝ) (F := E') (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ x

Tactic:
exact isLittleO_norm_right.mp this

Premises used: Asymptotics.isLittleO_norm_right, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : E'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : IsBigO (F := ℝ) (𝓝[s] x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
simp_rw : norm.{u_9} (E := E'') 0 ^ n = 0
simp_rw₁ : HPow.hPow (α := ℝ) 0 n = 0
⊢ ‖x₀ - x₀‖ ^ n = 0

Tactic:
simp_rw [sub_self, norm_zero, zero_pow hn]

Premises used: sub_self, norm_zero, zero_pow
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : IsBigO (F := ℝ) (𝓝 x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n

Tactic:
rw [← nhdsWithin_univ] at h

Premises used: nhdsWithin_univ
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : IsBigO (F := ℝ) (𝓝 x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
h₁ : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
⊢ n ≠ 0

Tactic:
rw [← nhdsWithin_univ] at h

Premises used: nhdsWithin_univ
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
h.eq_zero_of_norm_pow_within (mem_univ _) hn

Premises used: Asymptotics.IsBigO.eq_zero_of_norm_pow_within, Set.mem_univ
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
exact h.eq_zero_of_norm_pow_within (mem_univ _) hn

Premises used: Asymptotics.IsBigO.eq_zero_of_norm_pow_within, Set.mem_univ
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
x₀ : E'
n m : ℕ
h : n < m
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x₀) (fun (x : E') ↦ ‖x - x₀‖ ^ m) fun (x : E') ↦ ‖x - x₀‖ ^ n

Tactic:
(isLittleO_pow_pow h).comp_tendsto (tendsto_norm_sub_self x₀)

Premises used: Asymptotics.isLittleO_pow_pow, tendsto_norm_sub_self, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E' : Type u_6
inst : SeminormedAddCommGroup E'
x₀ : E'
m : ℕ
h : 1 < m
⊢ IsLittleO (E := ℝ) (F := E') (𝓝 x₀) (fun (x : E') ↦ ‖x - x₀‖ ^ m) fun (x : E') ↦ x - x₀

Tactic:
simpa only [isLittleO_norm_right, pow_one] using isLittleO_pow_sub_pow_sub x₀ h

Premises used: Asymptotics.isLittleO_norm_right, Asymptotics.isLittleO_pow_sub_pow_sub, pow_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
rw : ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖
rw₁ : 0 < 1 - c
⊢ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖

Tactic:
rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]

Premises used: mul_sub, div_eq_mul_inv, one_div, mul_comm, mul_one, le_div_iff₀
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖

Tactic:
le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _)

Premises used: norm_sub_norm_le, sub_le_sub_left, le_trans
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖

Tactic:
exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _)

Premises used: norm_sub_norm_le, sub_le_sub_left, le_trans
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Tactic:
sub_pos.2 hc

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Tactic:
exact sub_pos.2 hc

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
rw : f₁ x - -f₂ x = f₁ x + f₂ x
rw₁ rw₂ : f₁ x + f₂ x = f₁ x + f₂ x
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x

Tactic:
rw [neg_sub, sub_neg_eq_add]

Premises used: neg_sub, sub_neg_eq_add
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
h : f₁ =o[l] f₂
⊢ IsBigO (F := E') l f₂ fun (x : α) ↦ f₂ x - f₁ x

Tactic:
((h.def' one_half_pos).right_le_sub_of_lt_one one_half_lt_one).isBigO

Premises used: Asymptotics.IsBigOWith.right_le_sub_of_lt_one, one_half_lt_one, one_half_pos, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsLittleO.def'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
h : f₁ =o[l] f₂
⊢ IsBigO (F := E') l f₂ fun (x : α) ↦ f₁ x + f₂ x

Tactic:
((h.def' one_half_pos).right_le_add_of_lt_one one_half_lt_one).isBigO

Premises used: one_half_lt_one, one_half_pos, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigOWith.right_le_add_of_lt_one, Asymptotics.IsLittleO.def'
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
h : f₁ =o[l] f₂
⊢ f₂ =O[l] (f₂ + f₁)

Tactic:
add_comm f₁ f₂ ▸ h.right_isBigO_add

Premises used: Eq.rec, add_comm, Asymptotics.IsLittleO.right_isBigO_add
-- 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''
h : f =O[cofinite] g''
rcases : ∀ (C : ℝ) (C₀ : C > 0) (hC : IsBigOWith C cofinite f g''), ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
rcases h.exists_pos with ⟨C, C₀, hC⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : IsBigOWith C cofinite f g''
⊢ Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}

Tactic:
rw [IsBigOWith_def, eventually_cofinite] at hC

Premises used: Asymptotics.IsBigOWith_def, Filter.eventually_cofinite
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
rcases :
  ∀ (C' : ℝ)
    (hC' :
      ∀ (i : ℝ),
        Membership.mem (γ := Finset ℝ)
            (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
          i ≤ C'),
    ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
rcases (hC.toFinset.image fun x => ‖f x‖ / ‖g'' x‖).exists_le with ⟨C', hC'⟩

Premises used: Norm.norm, HDiv.hDiv, Finset.exists_le, Set.Finite.toFinset, Finset.image
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
⊢ ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'

Tactic:
simpa using hC'
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
⊢ ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'

Tactic:
have : ∀ x, C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C' := by simpa using hC'
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩

Premises used: Iff.mpr, Max.max, And.intro, Exists.intro, Or.inl, lt_max_iff
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
refine : ∀ (x : α) (h₀ : g'' x ≠ 0), ‖f x‖ ≤ max C C' * ‖g'' x‖
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
refine ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
rw : C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖
⊢ ‖f x‖ ≤ max C C' * ‖g'' x‖

Tactic:
rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le]

Premises used: not_le, max_mul_of_nonneg, Classical.or_iff_not_imp_left, le_max_iff, norm_nonneg
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖

Tactic:
fun hx => (div_le_iff₀ (norm_pos_iff.2 h₀)).1 (this _ hx)

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, Iff.mp
-- 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''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' :
  ∀ (i : ℝ),
    Membership.mem (γ := Finset ℝ)
        (Finset.image (fun (x : α) ↦ ‖f x‖ / ‖g'' x‖) (hC.toFinset (s := {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}))) i →
      i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖

Tactic:
exact fun hx => (div_le_iff₀ (norm_pos_iff.2 h₀)).1 (this _ hx)

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff, Iff.mp
-- 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''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
h' : f'' =O[cofinite] g''
C : ℝ
_C₀ : C > 0
hC : ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f'' x‖ ≤ C * ‖g'' x‖
x : α
hx : g'' x = 0
⊢ ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
simp [h _ hx, hx]
-- 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''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ (C : ℝ), ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
exact ⟨fun h' =>
    let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
    ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
    fun h => (isBigO_top.2 h).mono le_top⟩
-- 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''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ (C : ℝ), ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
classical
  exact ⟨fun h' =>
    let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
    ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
    fun h => (isBigO_top.2 h).mono le_top⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E : Type u_3
E'' : Type u_9
inst : Norm E
inst_1 : NormedAddCommGroup E''
f : ℕ → E
g'' : ℕ → E''
h rwa rwa₁ rwa₂ rwa₃ : f =O[atTop] g''
⊢ f =O[cofinite] g''

Tactic:
rwa [Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ (x : ℕ), g x = 0 → f x = 0
rw : f =O[cofinite] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
rw₁ rw₂ : (∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖) ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
⊢ f =O[atTop] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

Tactic:
rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]

Premises used: Asymptotics.isBigO_cofinite_iff, Nat.cofinite_eq_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
inst : NormedAddCommGroup E''
f : ℕ → E''
⊢ (∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * norm (E := ℝ) 1) ↔ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
simp only [norm_one, mul_one]

Premises used: NormOneClass.norm_one, mul_one
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
obtain : ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖), f =O[l] g
⊢ f =O[l] g

Tactic:
obtain ⟨C, hC_pos, hC⟩ := bound_of_isBigO_nat_atTop hfg

Premises used: Asymptotics.bound_of_isBigO_nat_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
⊢ f =O[l] g

Tactic:
isBigO_iff.mpr ⟨C, ?_⟩

Premises used: Iff.mpr, Asymptotics.isBigO_iff, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
refine : ∀ᶠ (x : ℕ) in l, ‖f x‖ ≤ C * ‖g x‖
⊢ f =O[l] g

Tactic:
refine isBigO_iff.mpr ⟨C, ?_⟩

Premises used: Iff.mpr, Asymptotics.isBigO_iff, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
h₁ : ∀ (x : ℕ) (h : g x = 0 → f x = 0), ‖f x‖ ≤ C * ‖g x‖
⊢ ∀ᶠ (x : ℕ) in l, ‖f x‖ ≤ C * ‖g x‖

Tactic:
filter_upwards [h] with x h
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h_1 : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
pos : ∀ (hf : f x = 0), ‖f x‖ ≤ C * ‖g x‖
neg : ∀ (hf : ¬f x = 0), ‖f x‖ ≤ C * ‖g x‖
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
by_cases hf : f x = 0
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h_1 : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
hf : f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp [hf, hC_pos]
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h_1 : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
hC fun a ↦ hf (h a)
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h_1 : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
exact hC fun a ↦ hf (h a)
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
x : α
⊢ 0 ≤ C * ‖g' x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
⊢ ∀ (x : α), 0 ≤ C * ‖g' x‖

Tactic:
have this (x) : 0 ≤ C * ‖g' x‖ := by positivity