awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
case case₁ case₂ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case₃ :
  ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g
have case₄ : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖
Tactic: case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
case case₁ case₂ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case₃ :
  ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case₄ : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ f =O[l] g
have h₁ : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖) (x : α) (hx : c * ‖f x‖ ≤ ‖g x‖),
  ‖f x‖ ≤ c⁻¹ * ‖g x‖
Tactic: case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
have rw : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
Tactic: rw [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ < ‖g x‖
have refine : ∀ (x : α), ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖ → ∀ (hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖) (hx₂ : 0 < ‖g x‖), 2⁻¹ * ‖g x‖ < ‖g x‖
Tactic: refine ((h.def (show 0 < 2⁻¹ by simp)).and hg).mono fun x ⟨hx₁, hx₂⟩ ↦ hx₁.trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
h_1 : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
⊢ 2⁻¹ * ‖g x‖ < ‖g x‖
have rw : LT.lt (α := ℝ) 2⁻¹ 1
Tactic: rw [mul_lt_iff_lt_one_left hx₂]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ f =O[l] g
have rw : ∃ (c : ℝ), IsBigOWith c l f g
Tactic: rw [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c c' : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : c ≤ c'
x : α
hx : Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f x‖ ≤ c * ‖g' x‖) x} x
⊢ c * ‖g' x‖ ≤ c' * ‖g' x‖
have ha : 0 ≤ ‖g' x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
have mp : f =o[l] g → ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
mp : f =o[l] g → ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
⊢ f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
have mpr : (∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) → f =o[l] g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
⊢ ∀ᶠ (x : α) in l, (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖
have mp : ∀ (x : α) (h₀' : ‖f x‖ ≤ 1 * ‖g x‖), (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖
Tactic: refine (H.def one_pos).mono fun x h₀' => ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖
have mp : 0 ≤ ‖g x‖
Tactic: rw [Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ 0 ≤ ‖g x‖
have mp : ∀ (hf : ∀ (x : α), 0 ≤ ‖f x‖), ‖f x‖ ≤ ‖g x‖
Tactic: refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ ‖f x‖ ≤ ‖g x‖
have mp : ∀ (h₀' : ‖f x‖ ≤ ‖g x‖) (hf : ∀ (x : α), 0 ≤ ‖f x‖), ‖f x‖ ≤ ‖g x‖
Tactic: rwa [one_mul] at h₀'
Cleared hypotheses: h₀', hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
⊢ ∀ᶠ (x : α) in l, (↑(n + 1) : ℝ) * ‖f x‖ ≤ ‖g x‖
have this : LT.lt (α := ℝ) 0 (↑n.succ : ℝ)
Tactic: have : (0 : ℝ) < n.succ := Nat.cast_pos.2 n.succ_pos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) → f =o[l] g
have mpr : ∀ (H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) (ε : ℝ) (ε0 : 0 < ε), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
Tactic: refine fun H => isLittleO_iff.2 fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
have mpr : ∀ (n : ℕ) (hn : ε⁻¹ < (↑n : ℝ)), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
Tactic: rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
have hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hn₀ : (0 : ℝ) < n := (inv_pos.2 ε0).trans hn
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
have mpr : ∀ (x : α) (hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖), ‖f x‖ ≤ ε * ‖g x‖
Tactic: refine ((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
⊢ ‖f x‖ ≤ ε * ‖g x‖
have mpr : 0 ≤ ‖g x‖
Tactic: refine hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le₀ ε0 hn.le) ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
⊢ 0 ≤ ‖g x‖
have mpr : ∀ (hf : ∀ (x : α), 0 ≤ ‖f x‖), LT.lt (α := ℝ) 0 (↑n : ℝ)⁻¹
Tactic: refine h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂
have simp : (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
Tactic: simp only [IsBigOWith_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
have subst : (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
Tactic: subst c₂
Cleared hypotheses: c₂, hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
have h : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
Tactic: apply Filter.eventually_congr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
have h : ∀ (a : α) (e₁ : f₁ a = f₂ a) (e₂ : g₁ a = g₂ a), ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
Tactic: filter_upwards [hf, hg] with _ e₁ e₂
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a : α
e₁ : f₁ a = f₂ a
e₂ : g₁ a = g₂ a
⊢ ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
have h : ‖f₂ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
Tactic: rw [e₁, e₂]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a : α
e₁ : f₁ a = f₂ a
e₂ : g₁ a = g₂ a
h : ‖f₂ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
⊢ ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
have h₁ : ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
Tactic: rw [e₁, e₂]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =O[l] g₁ ↔ f₂ =O[l] g₂
have simp : (∃ (c : ℝ), IsBigOWith c l f₁ g₁) ↔ ∃ (c : ℝ), IsBigOWith c l f₂ g₂
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[l] g₁ ↔ f₂ =o[l] g₂
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
Tactic: simp only [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ IsBigO.{0, u_3, u_4} (E := E) (F := F) cofinite (fun (n : ℤ) ↦ f (-n)) fun (n : ℤ) ↦ g (-n)
have rw : IsBigO.{0, u_3, u_4} (E := E) (F := F) cofinite (fun (n : ℤ) ↦ f ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)) fun (n : ℤ) ↦
  g ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)
Tactic: rw [← Equiv.neg_apply]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)
have simp : (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖
Tactic: simp only [IsBigOWith_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : IsBigOWith c' l g k
hc : 0 ≤ c
⊢ IsBigOWith (c * c') l f k
have simp : ∀ (hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) (hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖),
  ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖
Tactic: simp only [IsBigOWith_def] at *
Cleared hypotheses: hfg, hgk
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖
have h : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖) (hx' : ‖g x‖ ≤ c' * ‖k x‖), ‖f x‖ ≤ c * c' * ‖k x‖
Tactic: filter_upwards [hfg, hgk] with x hx hx'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ ‖f x‖ ≤ c * c' * ‖k x‖
have c₁ : c * ‖g x‖ ≤ c * (c' * ‖k x‖)
Tactic: calc
    ‖f x‖ ≤ c * ‖g x‖ := hx
    _ ≤ c * (c' * ‖k x‖) := by gcongr
    _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : f =o[l] g
hgk : IsBigOWith c l g k
hc : 0 < c
⊢ f =o[l] k
have simp : ∀ (hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
Tactic: simp only [IsLittleO_def] at *
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k
have this : 0 < c' / c
Tactic: have : 0 < c' / c := div_pos c'pos hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : g =o[l] k
hc : 0 < c
⊢ f =o[l] k
have simp : ∀ (hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
Tactic: simp only [IsLittleO_def] at *
Cleared hypotheses: hgk
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst : Norm E
inst_1 : Norm F
inst_2 : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k
have this : 0 < c' / c
Tactic: have : 0 < c' / c := div_pos c'pos hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ 1 * ‖g x‖
have rw : ‖f x‖ ≤ ‖g x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
⊢ False
have rcases : ∀ (x : α) (hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖) (hne : ‖f' x‖ ≠ 0), False
Tactic: rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖
hne : ‖f' x‖ ≠ 0
⊢ False
have hle₁ : ‖f' x‖ ≤ ‖f' x‖ / 2
Tactic: rw [one_div, ← div_eq_inv_mul] at hle
Cleared hypotheses: hle, hne
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
have simp_rw : (∀ᶠ (x : α) in 𝓝[insert x s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
Tactic: simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
simp_rw : (∀ᶠ (x : α) in 𝓝[insert x s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
have simp_rw₁ : (∀ᶠ (x : α) in pure x ⊔ 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
Tactic: simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
simp_rw : (∀ᶠ (x : α) in 𝓝[insert x s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₁ : (∀ᶠ (x : α) in pure x ⊔ 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
have simp_rw₂ : ((∀ᶠ (x : α) in pure x, ‖g x‖ ≤ C * ‖g' x‖) ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔
  ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
Tactic: simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
simp_rw : (∀ᶠ (x : α) in 𝓝[insert x s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₁ : (∀ᶠ (x : α) in pure x ⊔ 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₂ :
  ((∀ᶠ (x : α) in pure x, ‖g x‖ ≤ C * ‖g' x‖) ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔
    ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
have simp_rw₃ : (‖g x‖ ≤ C * ‖g' x‖ ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
Tactic: simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
inst_2 : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
simp_rw : (∀ᶠ (x : α) in 𝓝[insert x s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₁ : (∀ᶠ (x : α) in pure x ⊔ 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₂ :
  ((∀ᶠ (x : α) in pure x, ‖g x‖ ≤ C * ‖g' x‖) ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔
    ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
simp_rw₃ : (‖g x‖ ≤ C * ‖g' x‖ ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
have simp_rw₄ : (True ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
Tactic: simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'
have simp_rw : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'
Tactic: simp_rw [IsLittleO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'
have refine : ∀ (c : ℝ) (hc : 0 < c), IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'
Tactic: refine forall_congr' fun c => forall_congr' fun hc => ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'
have rw : ‖g x‖ ≤ c * ‖g' x‖
Tactic: rw [isBigOWith_insert]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ ‖g x‖ ≤ c * ‖g' x‖
have rw : 0 ≤ c * ‖g' x‖
Tactic: rw [h, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖g' x‖) ↔ f =O[l] g'
have simp : (∃ (c : ℝ), IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∃ (c : ℝ), IsBigOWith c l f g'
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖g' x‖) ↔ f =o[l] g'
have simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'
Tactic: simp only [IsLittleO_def]