awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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 := E') (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ x
have this₁ : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : E') ↦ ‖x‖ ^ n) fun (x : E') ↦ ‖x‖
Tactic: simp only [pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ‖x₀ - x₀‖ ^ n = 0
have simp_rw : norm.{u_9} (E := E'') 0 ^ n = 0
Tactic: simp_rw [sub_self, norm_zero, zero_pow hn]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ‖x₀ - x₀‖ ^ n = 0
have simp_rw₁ : HPow.hPow (α := ℝ) 0 n = 0
Tactic: simp_rw [sub_self, norm_zero, zero_pow hn]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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
⊢ f x₀ = 0
have h₁ : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E'') ↦ ‖x - x₀‖ ^ n
Tactic: rw [← nhdsWithin_univ] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖
have rw : ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖
Tactic: rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖
have rw₁ : 0 < 1 - c
Tactic: rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 : α
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x
have rw : f₁ x - -f₂ x = f₁ x + f₂ x
Tactic: rw [neg_sub, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x
have rw₁ : f₁ x + f₂ x = f₁ x + f₂ x
Tactic: rw [neg_sub, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
have rcases : ∀ (C : ℝ) (C₀ : C > 0) (hC : IsBigOWith C cofinite f g''), ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
Tactic: rcases h.exists_pos with ⟨C, C₀, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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''
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
have hC₁ : Set.Finite.{u_1} (α := α) {x : α | ¬‖f x‖ ≤ C * ‖g'' x‖}
Tactic: rw [IsBigOWith_def, eventually_cofinite] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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 > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
have 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‖
Tactic: rcases (hC.toFinset.image fun x => ‖f x‖ / ‖g'' x‖).exists_le with ⟨C', hC'⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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'
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
have this : ∀ (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'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
have refine : ∀ (x : α) (h₀ : g'' x ≠ 0), ‖f x‖ ≤ max C C' * ‖g'' x‖
Tactic: refine ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ‖f x‖ ≤ max C C' * ‖g'' x‖
have rw : C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ f =O[atTop] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
have rw : f =O[cofinite] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
Tactic: rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ f =O[atTop] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
have rw₁ : (∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖) ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
Tactic: rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ f =O[l] g
have obtain : ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖), f =O[l] g
Tactic: obtain ⟨C, hC_pos, hC⟩ := bound_of_isBigO_nat_atTop hfg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
have refine : ∀ᶠ (x : ℕ) in l, ‖f x‖ ≤ C * ‖g x‖
Tactic: refine isBigO_iff.mpr ⟨C, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ∀ᶠ (x : ℕ) in l, ‖f x‖ ≤ C * ‖g x‖
have h₁ : ∀ (x : ℕ) (h : g x = 0 → f x = 0), ‖f x‖ ≤ C * ‖g x‖
Tactic: filter_upwards [h] with x h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ ‖f x‖ ≤ C * ‖g x‖
have pos : ∀ (hf : f x = 0), ‖f x‖ ≤ C * ‖g x‖
Tactic: by_cases hf : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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‖
⊢ ‖f x‖ ≤ C * ‖g x‖
have neg : ∀ (hf : ¬f x = 0), ‖f x‖ ≤ C * ‖g x‖
Tactic: by_cases hf : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
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
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) C l (fun (x : α) ↦ f x i) g'
have this : ∀ (x : α), 0 ≤ C * ‖g' x‖
Tactic: have this (x) : 0 ≤ C * ‖g' x‖ := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ f =O[l] g' ↔ ∀ (i : ι), IsBigO.{u_1, u_18, u_7} (E := E' i) l (fun (x : α) ↦ f x i) g'
have simp : (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔
  ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) x l (fun (x : α) ↦ f x i) g'
Tactic: simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
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
⊢ f =o[l] g' ↔ ∀ (i : ι), IsLittleO.{u_1, u_18, u_7} (E := E' i) l (fun (x : α) ↦ f x i) g'
have simp : (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g') ↔
  ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g'
Tactic: simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → E
g : α → F
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
have rw : (∃ (c : ℝ), ∀ᶠ (x : α) in atTop, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
Tactic: rw [isBigO_iff, exists_eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → E
g : α → F
rw : (∃ (c : ℝ), ∀ᶠ (x : α) in atTop, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
have rw₁ : (∀ᶠ (a₀ : α) in atTop, ∃ (b : ℝ), ∀ a ≥ a₀, ‖f a‖ ≤ b * ‖g a‖) ↔
  ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
Tactic: rw [isBigO_iff, exists_eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
G : Type u_5
G' : Type u_8
inst : Norm G
inst_1 : SeminormedAddCommGroup G'
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → G
g : α → G'
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
have simp_rw : (∃ c > 0, ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
Tactic: simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
G : Type u_5
G' : Type u_8
inst : Norm G
inst_1 : SeminormedAddCommGroup G'
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → G
g : α → G'
simp_rw : (∃ c > 0, ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
have simp_rw₁ : (∃ (c : ℝ) (_ : c > 0), ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔
  ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ) (_ : c > 0), ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
Tactic: simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
G : Type u_5
G' : Type u_8
inst : Norm G
inst_1 : SeminormedAddCommGroup G'
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → G
g : α → G'
simp_rw : (∃ c > 0, ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
simp_rw₁ :
  (∃ (c : ℝ) (_ : c > 0), ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ) (_ : c > 0), ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
have simp_rw₂ : (∃ (x : { a : ℝ // a > 0 }), ∀ᶠ (x_1 : α) in atTop, (↑x : ℝ) * ‖f x_1‖ ≤ ‖g x_1‖) ↔
  ∀ᶠ (n₀ : α) in atTop, ∃ (x : { a : ℝ // a > 0 }), ∀ n ≥ n₀, (↑x : ℝ) * ‖f n‖ ≤ ‖g n‖
Tactic: simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h ↔ IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x
have rw : (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Tactic: rw [isBigOWith_iff, isBigOWith_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
have refine_1 : ∀ (h_1 : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖), ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
refine_1 : ∀ (h_1 : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖), ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
have refine_2 : ∀ (h_1 : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖), ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
have refine_1 : ∀ (x : α) (hx : f x ≠ 0), ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
Tactic: refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
x : α
hx : f x ≠ 0
⊢ ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
have refine_1 : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
x : α
hx : f x ≠ 0
refine_1 : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
⊢ ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
have refine_1₁ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖)
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
x : α
hx : f x ≠ 0
refine_1 : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
refine_1₁ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖)
⊢ ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
have refine_1₂ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x‖ / ‖f x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
x : α
hx : f x ≠ 0
refine_1 : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
refine_1₁ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖)
refine_1₂ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x‖ / ‖f x‖
⊢ ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
have refine_1₃ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
have refine_2 : ∀ (x : α) (hx : f x ≠ 0), ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖
Tactic: refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖
have refine_2 : ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
x : α
hx : f x ≠ 0
refine_2 : ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
⊢ ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖
have refine_2₁ : ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖) ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
x : α
hx : f x ≠ 0
refine_2 : ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
refine_2₁ : ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖) ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
⊢ ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖
have refine_2₂ : ‖g x‖ ≤ c * ‖h_1 x‖ / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
x : α
hx : f x ≠ 0
refine_2 : ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
refine_2₁ : ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖) ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
refine_2₂ : ‖g x‖ ≤ c * ‖h_1 x‖ / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
⊢ ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖
have refine_2₃ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
Tactic: rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsBigO (E := 𝕜) l (fun (x : α) ↦ f x * g x) h ↔ IsBigO (F := 𝕜) l g fun (x : α) ↦ h x / f x
have rw : (∃ (c : ℝ), IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h) ↔
  ∃ (c : ℝ), IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x
Tactic: rw [isBigO_iff_isBigOWith, isBigO_iff_isBigOWith]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsLittleO (E := 𝕜) l (fun (x : α) ↦ f x * g x) h ↔ IsLittleO (F := 𝕜) l g fun (x : α) ↦ h x / f x
have rw : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h) ↔
  ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x
Tactic: rw [isLittleO_iff_forall_isBigOWith, isLittleO_iff_forall_isBigOWith]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g
have h₁ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
Tactic: rw [← eventually_forall_ge_atTop] at h
Cleared hypotheses: h, hrec
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g
have obtain : ∀ (n₀ : ℕ) (h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0)
  (hrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖),
  f =O[atTop] g
Tactic: obtain ⟨n₀, h, hrec⟩ := h.and hrec |>.exists