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 α
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‖
⊢ (↑‖c‖₊ : ℝ≥0∞) ≠ ∞

Tactic:
first | apply ENNReal.coe_ne_top | positivity

Premises used: ENNReal.coe_ne_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 : 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
funProp₁ : (↑‖c‖₊ : ℝ≥0∞) ≠ ∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)

Tactic:
fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | positivity)

Premises used: ENNReal.coe_ne_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 : 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‖
mp : ∀ (ε : ℝ≥0) (hε₀ : 0 < ε) (hε : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1), ∀ᶠ (x : α) in l, f x ∈ id U
⊢ ∀ᶠ (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)
-- 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 : 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
h :
  ∀ (x : α) (hx : egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)),
    f x ∈ id U
⊢ ∀ᶠ (x : α) in l, f x ∈ id U

Tactic:
filter_upwards [hr ε hε₀.ne'] with x hx

Premises used: LT.lt.ne'
-- 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 : 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

Tactic:
mem_of_egauge_lt_one hUb (hx.trans_lt ?_)

Premises used: LE.le.trans_lt, mem_of_egauge_lt_one
-- 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 : 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)
h : (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x) < 1
⊢ f x ∈ id U

Tactic:
refine mem_of_egauge_lt_one hUb (hx.trans_lt ?_)

Premises used: LE.le.trans_lt, mem_of_egauge_lt_one
-- 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 : 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)
rw : (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞))
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)

Tactic:
rw [mul_div_assoc]

Premises used: mul_div_assoc
-- 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 : 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)
bc : egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞))

Tactic:
gcongr
-- 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 : 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)
⊢ r ≠ 0 ∨ norm.{u_3} (E := 𝕜) 1 ≠ 0

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
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)
⊢ egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)

Tactic:
simpa using egauge_ball_le_of_one_lt_norm (r := r) (x := (1 : 𝕜)) hc (by simp)

Premises used: egauge_ball_le_of_one_lt_norm
-- 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 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              ∀ᶠ (x : α) in l,
                _root_.egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * _root_.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,
        _root_.egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * _root_.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 : _root_.egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * _root_.egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
egauge : (↑ε : ℝ≥0∞) * _root_.egauge 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) 1 ≤ (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
egauge₁ : (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
⊢ (↑ε : ℝ≥0∞) * _root_.egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x) < 1

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 := ‹_›

Premises used: ENNReal.ofNNReal, HMul.hMul, NNNorm.nnnorm, HDiv.hDiv, Metric.ball, OfNat.ofNat, egauge, NNReal.toReal
-- 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 : ContinuousSMul 𝕜 E
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)
⊢ Tendsto f l (𝓝 0) → IsLittleOTVS 𝕜 (F := 𝕜) l f 1

Tactic:
simp only [isLittleOTVS_iff]

Premises used: Asymptotics.isLittleOTVS_iff
-- 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 : 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)

Tactic:
⟨ball 0 1, ball_mem_nhds _ one_pos, fun ε hε ↦ ?_⟩

Premises used: Metric.ball, Metric.ball_mem_nhds, And.intro, Exists.intro, OfNat.ofNat, 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 : ContinuousSMul 𝕜 E
hf : Tendsto f l (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
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)
⊢ ∃ (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:
refine ⟨ball 0 1, ball_mem_nhds _ one_pos, 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
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
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)
⊢ 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ε⟩

Premises used: NormedField.exists_norm_lt, Ne.bot_lt
-- 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 : 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‖ < (↑ε : ℝ)
⊢ c ≠ 0

Tactic:
simpa using hc₀
-- 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 : 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‖ < (↑ε : ℝ)
⊢ c ≠ 0

Tactic:
replace hc₀ : c ≠ 0 := by simpa using hc₀
-- 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 : 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
h : ∀ (a : α) (ha : a ∈ f ⁻¹' (c • U)), egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 a)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
    (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 x)

Tactic:
filter_upwards [hf ((set_smul_mem_nhds_zero_iff hc₀).2 hU)] with a ha

Premises used: Iff.mpr, set_smul_mem_nhds_zero_iff
-- 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 : 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) ≤ (↑‖c‖₊ : ℝ≥0∞)

Tactic:
egauge_le_of_mem_smul ha

Premises used: egauge_le_of_mem_smul
-- 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 : 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)
⊢ (↑‖c‖₊ : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞)

Tactic:
mod_cast hcε.le

Premises used: cast, LT.lt.le, ENNReal.coe_le_coe._simp_1, Eq.symm
-- 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 : 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)
h : 1 ≤ egauge 𝕜 (E := 𝕜) (ball 0 1) 1
⊢ (↑ε : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (E := 𝕜) (ball 0 1) 1

Tactic:
apply le_mul_of_one_le_right'

Premises used: le_mul_of_one_le_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 α
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)
⊢ 1 ≤ egauge 𝕜 (E := 𝕜) (ball 0 1) 1

Tactic:
simpa using le_egauge_ball_one 𝕜 (1 : 𝕜)

Premises used: le_egauge_ball_one, 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 : 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 : (↑ε : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞) * _root_.egauge 𝕜 (E := 𝕜) (ball 0 1) 1
⊢ _root_.egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * _root_.egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 1) (1 a)

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 : 𝕜)

Premises used: LT.lt.le, Metric.ball, egauge_le_of_mem_smul, OfNat.ofNat, 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 α
inst_4 : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜; l] f
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)
⊢ Tendsto.{u_1, u_4} (β := E) (fun (x : α) ↦ (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
rw [← isLittleOTVS_one (𝕜 := 𝕜), isLittleOTVS_iff]

Premises used: Asymptotics.isLittleOTVS_one, Asymptotics.isLittleOTVS_iff
-- 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
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)
⊢ ∃ (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⟩

Premises used: Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul, Asymptotics.IsLittleOTVS.smul_left, Inv.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 α
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)

Tactic:
⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩

Premises used: Filter.Eventually.mono, And.intro, Exists.intro, 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 α
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)
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)
⊢ ∃ (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:
refine ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩