awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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 : ContinuousSMul 𝕜 E
hf : Tendsto f l (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
ε : ℝ≥0
hε : ε ≠ 0
c : 𝕜
hcε : ‖c‖ < (↑ε : ℝ)
hc₀ : c ≠ 0
a : α
ha : a ∈ f ⁻¹' (c • U)
⊢ egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 a)
have egauge : (↑ε : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 1) 1
Tactic: calc
      egauge 𝕜 U (f a) ≤ ‖c‖₊ := egauge_le_of_mem_smul ha
      _ ≤ ε := mod_cast hcε.le
      _ ≤ ε * egauge 𝕜 (ball (0 : 𝕜) 1) 1 := by
        apply le_mul_of_one_le_right'
        simpa using le_egauge_ball_one 𝕜 (1 : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
⊢ Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)
have rw : ∀ (U : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) U →
    ∃ (V : Set 𝕜),
      Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U ((f x)⁻¹ • g x)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)
Tactic: rw [← isLittleOTVS_one (𝕜 := 𝕜), isLittleOTVS_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U ((f x)⁻¹ • g x)) fun (x : α) ↦
            (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)
have rcases : ∀ (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)),
  ∃ (V : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U ((f x)⁻¹ • g x)) fun (x : α) ↦
            (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)
Tactic: rcases (h.smul_left f⁻¹).1 U hU with ⟨V, hV₀, hV⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ ∃ (V : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U ((f x)⁻¹ • g x)) fun (x : α) ↦
            (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)
have refine : ∀ (ε : ℝ≥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)),
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)
Tactic: refine ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)
have 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)
Tactic: by_cases hx₀ : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (f⁻¹ x • f x)) x)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)) x)
have 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)
Tactic: by_cases hx₀ : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
have refine : ∀ (h : Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)), g =o[𝕜; l] f
Tactic: refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ g =o[𝕜; l] f
have refine : ∀ (x : α) (hx : f x = 0 → g x = 0), (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
Tactic: refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
⊢ (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
have pos : ∀ (h : f x = 0), (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
Tactic: by_cases h : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
⊢ (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
have neg : ∀ (h : ¬f x = 0), (fun (x : α) ↦ f x • (f x)⁻¹ • g x) x = g x
Tactic: by_cases h : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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)
⊢ IsBigOTVS 𝕜 (F := 𝕜) l f fun (x : α) ↦ 1
have h₁ : 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))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ IsBigOTVS 𝕜 (F := 𝕜) l f fun (x : α) ↦ 1
have 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
Tactic: rw [(nhds_basis_balanced 𝕜 E).add_self.isBigOTVS_iff nhds_basis_ball]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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), 0 < r ∧ r ≤ 1 ∧ (↑r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
have h₁ : ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, x_1 ≤ 1 ∧ (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
Tactic: apply Eventually.exists_gt
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)⁻¹
have h₁ : ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, (↑x_1 : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹
Tactic: refine .and (eventually_le_nhds one_pos) ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)⁻¹
have h₁ : (↑0 : ℝ≥0∞) < (egauge 𝕜 U x)⁻¹
Tactic: refine (ENNReal.tendsto_coe.mpr tendsto_id).eventually_le_const ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
⊢ (↑0 : ℝ≥0∞) < (egauge 𝕜 U x)⁻¹
have h₁ : ∃ (c : 𝕜), x ∈ c • U
Tactic: suffices ∃ c : 𝕜, x ∈ c • U by simpa [egauge_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 j) 1
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)⁻¹
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 j) 1
have right : ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
Tactic: use r, by positivity
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)⁻¹
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) (f x) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
have h₁ : ∀ (a : α) (ha : f a - x ∈ U), egauge 𝕜 (id U + id U) (f a) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
Tactic: filter_upwards [h.eventually_mem hU₀] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
⊢ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x) ≤ (↑r : ℝ≥0∞)⁻¹
have h₁ : egauge 𝕜 U (f a - x) ≤ (↑r : ℝ≥0∞)⁻¹
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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∞)⁻¹
⊢ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x) ≤ (↑r : ℝ≥0∞)⁻¹
have h₂ : egauge 𝕜 U x ≤ (↑r : ℝ≥0∞)⁻¹
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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∞)⁻¹
have h₁ : 1 ≤ (↑r : ℝ≥0∞)⁻¹
Tactic: refine (egauge_le_one _ ha).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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 𝕜 (id U + id U) (f a) ≤ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
have egauge : egauge 𝕜 (U + U) (f a) ≤ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x)
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 : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ _root_.egauge 𝕜 (id U + id U) (f a) ≤ _root_.egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
have egauge₁ : max (_root_.egauge 𝕜 U (f a - x)) (_root_.egauge 𝕜 U x) ≤ (↑r : ℝ≥0∞)⁻¹
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 : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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∞)⁻¹
⊢ _root_.egauge 𝕜 (id U + id U) (f a) ≤ _root_.egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1
have egauge₂ : (↑r : ℝ≥0∞)⁻¹ ≤ _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 : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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 α
⊢ f =o[𝕜; l] g ↔ f =o[l] g
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖₊), f =o[𝕜; l] g ↔ f =o[l] g
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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‖₊
⊢ f =o[𝕜; l] g ↔ f =o[l] g
have hc₀ : 0 < ‖c‖₊
Tactic: have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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‖₊
⊢ f =o[𝕜; l] g ↔ f =o[l] g
have 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‖
Tactic: simp only [isLittleO_iff, nhds_basis_ball.isLittleOTVS_iff nhds_basis_ball]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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‖₊
⊢ (∀ (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‖
have refine_1 : ∀
  (h :
    ∀ (i : ℝ),
      0 < i →
        ∃ (j : ℝ),
          0 < j ∧
            ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x))
  (ε : ℝ) (hε : 0 < ε), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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‖₊
refine_1 :
  ∀
    (h :
      ∀ (i : ℝ),
        0 < i →
          ∃ (j : ℝ),
            0 < j ∧
              ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x))
    (ε : ℝ) (hε : 0 < ε), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
⊢ (∀ (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‖
have refine_2 : ∀ (h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) (ε : ℝ) (hε : 0 < ε) (δ : ℝ≥0) (hδ : δ ≠ 0),
  ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩