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
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ egauge 𝕜 U (c x • f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)
have h₁ : ‖c x‖ₑ * egauge 𝕜 U (f x) ≤ ‖c x‖ₑ * ((↑ε : ℝ≥0∞) * egauge 𝕜 V (g x))
Tactic: rw [egauge_smul_right, egauge_smul_right, mul_left_comm]
-- 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 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
h₁ : ‖c x‖ₑ * egauge 𝕜 U (f x) ≤ ‖c x‖ₑ * ((↑ε : ℝ≥0∞) * egauge 𝕜 V (g x))
⊢ egauge 𝕜 U (c x • f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)
have h₂ : c x = 0 → V.Nonempty
Tactic: rw [egauge_smul_right, egauge_smul_right, mul_left_comm]
-- 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 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
h₁ : ‖c x‖ₑ * egauge 𝕜 U (f x) ≤ ‖c x‖ₑ * ((↑ε : ℝ≥0∞) * egauge 𝕜 V (g x))
h₂ : c x = 0 → V.Nonempty
⊢ egauge 𝕜 U (c x • f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)
have h₃ : c x = 0 → U.Nonempty
Tactic: rw [egauge_smul_right, egauge_smul_right, mul_left_comm]
-- 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
⊢ IsLittleOTVS 𝕜 (F := 𝕜) l f 1 ↔ Tendsto f l (𝓝 0)
have mp : IsLittleOTVS 𝕜 (F := 𝕜) l f 1 → Tendsto f l (𝓝 0)
Tactic: constructor
-- 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
mp : IsLittleOTVS 𝕜 (F := 𝕜) l f 1 → Tendsto f l (𝓝 0)
⊢ IsLittleOTVS 𝕜 (F := 𝕜) l f 1 ↔ Tendsto f l (𝓝 0)
have mpr : Tendsto f l (𝓝 0) → IsLittleOTVS 𝕜 (F := 𝕜) l f 1
Tactic: constructor
-- 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 : ContinuousSMul 𝕜 E
hf : IsLittleOTVS 𝕜 (F := 𝕜) l f 1
⊢ Tendsto f l (𝓝 0)
have hf₁ : ∀ (i : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) i →
    ∃ (j : ℝ),
      0 < j ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
Tactic: rw [(basis_sets _).isLittleOTVS_iff nhds_basis_ball] at hf
Cleared hypotheses: hf
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
⊢ Tendsto f l (𝓝 0)
have mp : ∀ (i : Set E), Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i → ∀ᶠ (x : α) in l, f x ∈ id i
Tactic: rw [(nhds_basis_balanced 𝕜 E).tendsto_right_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 α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
⊢ ∀ᶠ (x : α) in l, f x ∈ id U
have mp : ∀ (r : ℝ) (hr₀ : 0 < r)
  (hr :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 r) (1 x)),
  ∀ᶠ (x : α) in l, f x ∈ id U
Tactic: rcases hf U hU with ⟨r, hr₀, hr⟩
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ
hr₀ : 0 < r
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 r) (1 x)
⊢ ∀ᶠ (x : α) in l, f x ∈ id U
have mp : ∀ (r : ℝ≥0) (hr₀ : 0 < (↑r : ℝ))
  (hr :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 →
        ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)),
  ∀ᶠ (x : α) in l, f x ∈ id U
Tactic: lift r to ℝ≥0 using hr₀.le
Cleared hypotheses: r, hr₀, hr
-- 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 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ)
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
⊢ ∀ᶠ (x : α) in l, f x ∈ id U
have hr₁ : 0 < r
Tactic: norm_cast at hr₀
Cleared hypotheses: hr₀
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
⊢ ∀ᶠ (x : α) in l, f x ∈ id U
have mp : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∀ᶠ (x : α) in l, f x ∈ id U
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (ε : ℝ≥0), 0 < ε ∧ (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
have h : ∀ᶠ (x : ℝ≥0) in 𝓝 0, (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
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 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ᶠ (x : ℝ≥0) in 𝓝 0, (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
have h : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
Tactic: refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
have funProp : (↑r : ℝ≥0∞) ≠ 0
Tactic: fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | 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 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
funProp : (↑r : ℝ≥0∞) ≠ 0
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
have funProp₁ : (↑‖c‖₊ : ℝ≥0∞) ≠ ∞
Tactic: fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | 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 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ᶠ (x : α) in l, f x ∈ id U
have mp : ∀ (ε : ℝ≥0) (hε₀ : 0 < ε) (hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1), ∀ᶠ (x : α) in l, f x ∈ id U
Tactic: obtain ⟨ε, hε₀, hε⟩ : ∃ ε : ℝ≥0, 0 < ε ∧ (ε * ‖c‖₊ / r : ℝ≥0∞) < 1 := by
      apply Eventually.exists_gt
      refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one
      fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | 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 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
⊢ ∀ᶠ (x : α) in l, f x ∈ id U
have h : ∀ (x : α) (hx : egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)), f x ∈ id U
Tactic: filter_upwards [hr ε hε₀.ne'] with x hx
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
⊢ f x ∈ id U
have h : (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x) < 1
Tactic: refine mem_of_egauge_lt_one hUb (hx.trans_lt ?_)
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
have rw : (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞))
Tactic: rw [mul_div_assoc]
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞))
have bc : egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
Tactic: gcongr
-- 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 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
⊢ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x) < 1
have egauge : (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
Tactic: calc
      (ε : ℝ≥0∞) * egauge 𝕜 (ball (0 : 𝕜) r) 1 ≤ (ε * ‖c‖₊ / r : ℝ≥0∞) := by
        rw [mul_div_assoc]
        gcongr
        simpa using egauge_ball_le_of_one_lt_norm (r := r) (x := (1 : 𝕜)) hc (by simp)
      _ < 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 : ContinuousSMul 𝕜 E
⊢ Tendsto f l (𝓝 0) → IsLittleOTVS 𝕜 (F := 𝕜) l f 1
have mpr : Tendsto f l (𝓝 0) →
  ∀ (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)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)
Tactic: simp only [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 α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf : Tendsto f l (𝓝 0)
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)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (1 x)
have mpr : ∀ (ε : ℝ≥0) (hε : ε ≠ 0),
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
    (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 x)
Tactic: refine ⟨ball 0 1, ball_mem_nhds _ 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
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
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
    (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 x)
have mpr : ∀ (c : 𝕜) (hc₀ : 0 < ‖c‖) (hcε : ‖c‖ < (↑ε : ℝ)),
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
    (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 x)
Tactic: rcases NormedField.exists_norm_lt 𝕜 hε.bot_lt with ⟨c, hc₀, hcε⟩
-- 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 : ContinuousSMul 𝕜 E
hf : Tendsto f l (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
ε : ℝ≥0
hε : ε ≠ 0
c : 𝕜
hc₀ : 0 < ‖c‖
hcε : ‖c‖ < (↑ε : ℝ)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
    (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 x)
have hc₁ : c ≠ 0
Tactic: replace hc₀ : c ≠ 0 := by simpa using hc₀
Cleared hypotheses: hc₀
-- 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
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
    (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 x)
have h : ∀ (a : α) (ha : a ∈ f ⁻¹' (c • U)), egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 a)
Tactic: filter_upwards [hf ((set_smul_mem_nhds_zero_iff hc₀).2 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 : 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)
⊢ (↑ε : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 1) 1
have h : 1 ≤ egauge 𝕜 (E := 𝕜) (ball 0 1) 1
Tactic: apply le_mul_of_one_le_right'