awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set 𝕜
hV₀ : Membership.mem (γ := Filter 𝕜) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 →
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f⁻¹ x • g x)) fun (x : α) ↦
        (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx :
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f⁻¹ x • g x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
pos :
  ∀ (hx₀ : f x = 0),
    LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
      ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)
neg :
  ∀ (hx₀ : ¬f x = 0),
    LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
      ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)

Tactic:
by_cases hx₀ : f x = 0
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set 𝕜
hV₀ : Membership.mem (γ := Filter 𝕜) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 →
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f⁻¹ x • g x)) fun (x : α) ↦
        (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx :
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f⁻¹ x • g x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
hx₀ : f x = 0
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)

Tactic:
simp [hx₀, egauge_zero_right _ (Filter.nonempty_of_mem hV₀)]

Premises used: Filter.nonempty_of_mem, egauge_zero_right
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set 𝕜
hV₀ : Membership.mem (γ := Filter 𝕜) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 →
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f⁻¹ x • g x)) fun (x : α) ↦
        (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx :
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f⁻¹ x • g x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
hx₀ : ¬f x = 0
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)

Tactic:
simp [hx₀, egauge_zero_right _ (Filter.nonempty_of_mem hV₀)]

Premises used: Filter.nonempty_of_mem, egauge_zero_right
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ g =o[𝕜; l] f ↔ Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩

Premises used: Asymptotics.IsLittleOTVS.tendsto_inv_smul, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
refine : ∀ (h : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)), g =o[𝕜; l] f
⊢ g =o[𝕜; l] f ↔ Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)
⊢ (fun (x : α) ↦ HSMul.hSMul (β := 𝕜) (f x) (1 x)) =ᶠ[l] f

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)
refine : ∀ (x : α) (hx : f x = 0 → g x = 0), (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
⊢ g =o[𝕜; l] f

Tactic:
refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)

Premises used: Iff.mpr, Asymptotics.isLittleOTVS_one, Asymptotics.IsLittleOTVS.smul_left, Asymptotics.IsLittleOTVS.congr', Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
pos : ∀ (h : f x = 0), (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
neg : ∀ (h : ¬f x = 0), (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
⊢ (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x

Tactic:
by_cases h : f x = 0
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h_1 : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
h : f x = 0
⊢ (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x

Tactic:
simp [h, hx]
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h_1 : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
h : ¬f x = 0
⊢ (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x

Tactic:
simp [h, hx]
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto f l (𝓝 x)
⊢ Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)

Tactic:
simpa [sub_eq_add_neg] using h.add (tendsto_const_nhds (x := -x))

Premises used: tendsto_const_nhds, sub_eq_add_neg, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto f l (𝓝 x)
⊢ Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)

Tactic:
replace h : Tendsto (f · - x) l (𝓝 0) := by
    simpa [sub_eq_add_neg] using h.add (tendsto_const_nhds (x := -x))
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
rw :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i →
      ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id i + id i) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 j) 1
⊢ IsBigOTVS 𝕜 (F := 𝕜) l f fun (x : α) ↦ 1

Tactic:
rw [(nhds_basis_balanced 𝕜 E).add_self.isBigOTVS_iff nhds_basis_ball]

Premises used: Filter.HasBasis.add_self, nhds_basis_balanced, Filter.HasBasis.isBigOTVS_iff, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
h₁ : ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, x_1 ≤ 1 ∧ (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
⊢ ∃ (r : ℝ≥0), 0 < r ∧ r ≤ 1 ∧ (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹

Tactic:
apply Eventually.exists_gt

Premises used: Filter.Eventually.exists_gt
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
⊢ ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, x_1 ≤ 1 ∧ (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹

Tactic:
.and (eventually_le_nhds one_pos) ?_

Premises used: Filter.Eventually.and, eventually_le_nhds, one_pos
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
h₁ : ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
⊢ ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, x_1 ≤ 1 ∧ (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹

Tactic:
refine .and (eventually_le_nhds one_pos) ?_
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
⊢ ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹

Tactic:
(ENNReal.tendsto_coe.mpr tendsto_id).eventually_le_const ?_

Premises used: Iff.mpr, Filter.tendsto_id, Filter.Tendsto.eventually_le_const, ENNReal.tendsto_coe
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
h₁ : (↑0 : ℝ≥0∞) < (egauge 𝕜 U x)⁻¹
⊢ ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹

Tactic:
refine (ENNReal.tendsto_coe.mpr tendsto_id).eventually_le_const ?_

Premises used: Iff.mpr, Filter.tendsto_id, Filter.Tendsto.eventually_le_const, ENNReal.tendsto_coe
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
this : ∃ (c : 𝕜), x ∈ c • U
⊢ (↑0 : ℝ≥0∞) < (egauge 𝕜 U x)⁻¹

Tactic:
simpa [egauge_eq_top]

Premises used: egauge_eq_top
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
h₁ : ∃ (c : 𝕜), x ∈ c • U
⊢ (↑0 : ℝ≥0∞) < (egauge 𝕜 U x)⁻¹

Tactic:
suffices ∃ c : 𝕜, x ∈ c • U by simpa [egauge_eq_top]
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
⊢ ∃ (c : 𝕜), x ∈ c • U

Tactic:
simpa using (absorbent_nhds_zero (𝕜 := 𝕜) hU₀ x).exists

Premises used: absorbent_nhds_zero, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
obtain :
  ∀ (r : ℝ≥0) (hr₀ : 0 < r) (hr₁ : r ≤ 1) (hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹),
    ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 j) 1
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 j) 1

Tactic:
obtain ⟨r, hr₀, hr₁, hr⟩ : ∃ r : ℝ≥0, 0 < r ∧ r ≤ 1 ∧ (r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹ := by
    apply Eventually.exists_gt
    refine .and (eventually_le_nhds one_pos) ?_
    refine (ENNReal.tendsto_coe.mpr tendsto_id).eventually_le_const ?_
    suffices ∃ c : 𝕜, x ∈ c • U by simpa [egauge_eq_top]
    simpa using (absorbent_nhds_zero (𝕜 := 𝕜) hU₀ x).exists

Premises used: egauge
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
⊢ 0 < (↑r : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
right : ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 j) 1

Tactic:
use r, by positivity
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
h₁ : ∀ (a : α) (ha : f a - x ∈ U), egauge 𝕜 (id U + id U) (f a) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1

Tactic:
filter_upwards [h.eventually_mem hU₀] with a ha

Premises used: Filter.Tendsto.eventually_mem
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
⊢ egauge 𝕜 (U + U) (f a) ≤ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x)

Tactic:
simpa using egauge_add_add_le hUb hUb (f a - x) x

Premises used: egauge_add_add_le, HSub.hSub
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
h₁ : egauge 𝕜 U (f a - x) ≤ (↑r : ℝ≥0∞)⁻¹
h₂ : egauge 𝕜 U x ≤ (↑r : ℝ≥0∞)⁻¹
⊢ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x) ≤ (↑r : ℝ≥0∞)⁻¹

Tactic:
apply max_le

Premises used: max_le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
⊢ egauge 𝕜 U (f a - x) ≤ (↑r : ℝ≥0∞)⁻¹

Tactic:
(egauge_le_one _ ha).trans ?_

Premises used: egauge_le_one, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
h₁ : 1 ≤ (↑r : ℝ≥0∞)⁻¹
⊢ egauge 𝕜 U (f a - x) ≤ (↑r : ℝ≥0∞)⁻¹

Tactic:
refine (egauge_le_one _ ha).trans ?_

Premises used: egauge_le_one, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
⊢ 1 ≤ (↑r : ℝ≥0∞)⁻¹

Tactic:
simp [hr₁]
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
h₂ h₃ h₄ h₅ : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
⊢ egauge 𝕜 U x ≤ (↑r : ℝ≥0∞)⁻¹

Tactic:
rwa [ENNReal.le_inv_iff_le_inv]

Premises used: ENNReal.le_inv_iff_le_inv
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
⊢ (↑r : ℝ≥0∞)⁻¹ ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1

Tactic:
simpa using div_le_egauge_ball 𝕜 r (1 : 𝕜)

Premises used: div_le_egauge_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
x : E
h : Tendsto.{u_1, u_4} (β := E) (fun (x_1 : α) ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : (↑r : ℝ≥0∞) ≤ (_root_.egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
egauge : _root_.egauge 𝕜 (U + U) (f a) ≤ max (_root_.egauge 𝕜 U (f a - x)) (_root_.egauge 𝕜 U x)
egauge₁ : max (_root_.egauge 𝕜 U (f a - x)) (_root_.egauge 𝕜 U x) ≤ (↑r : ℝ≥0∞)⁻¹
egauge₂ : (↑r : ℝ≥0∞)⁻¹ ≤ _root_.egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
⊢ _root_.egauge 𝕜 (id U + id U) (f a) ≤ _root_.egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1

Tactic:
calc
    egauge 𝕜 (U + U) (f a) ≤ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x) := by
      simpa using egauge_add_add_le hUb hUb (f a - x) x
    _ ≤ (r : ℝ≥0∞)⁻¹ := by
      apply max_le
      · refine (egauge_le_one _ ha).trans ?_
        simp [hr₁]
      · rwa [ENNReal.le_inv_iff_le_inv]
    _ ≤ egauge 𝕜 (ball (0 : 𝕜) _) 1 := by simpa using div_le_egauge_ball 𝕜 r (1 : 𝕜)

Premises used: ENNReal.ofNNReal, HSub.hSub, Metric.ball, HAdd.hAdd, Max.max, OfNat.ofNat, egauge
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖₊), f =o[𝕜; l] g ↔ f =o[l] g
⊢ f =o[𝕜; l] g ↔ f =o[l] g

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
⊢ 0 < ‖c‖₊

Tactic:
have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
simp :
  (∀ (i : ℝ),
      0 < i →
        ∃ (j : ℝ),
          0 < j ∧
            ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =o[𝕜; l] g ↔ f =o[l] g

Tactic:
simp only [isLittleO_iff, nhds_basis_ball.isLittleOTVS_iff nhds_basis_ball]

Premises used: Filter.HasBasis.isLittleOTVS_iff, Metric.nhds_basis_ball, Asymptotics.isLittleO_iff