awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this_1 : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
this : IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)
refine : ∀ (x : α) (hkx : k x ≠ 0), ‖k x * k x ^ (z - 1)‖ = ‖k x ^ z‖
⊢ IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
refine this.trans_isBigO <| IsBigO.of_bound' <| hk0.mono fun x hkx => le_of_eq ?_

Premises used: Filter.Eventually.mono, Asymptotics.IsBigO.of_bound', le_of_eq, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this_1 : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
this : IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)
x : α
hkx : k x ≠ 0
⊢ ‖k x * k x ^ (z - 1)‖ = ‖k x ^ z‖

Tactic:
simp [← zpow_one_add₀ hkx]

Premises used: zpow_one_add₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
simp :
  (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ ⊥ →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (i : ℝ≥0), ⊥ < i → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) / egauge 𝕜 V (g x) ∈ ENNReal.ofNNReal '' Iic i
⊢ f =o[𝕜; l] g ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (𝓝 0)

Tactic:
simp only [isLittleOTVS_iff, ← ENNReal.coe_zero, ENNReal.nhds_coe, ← NNReal.bot_eq_zero,
    (nhds_bot_basis_Iic.map _).tendsto_right_iff]

Premises used: NNReal.bot_eq_zero, ENNReal.nhds_coe, Filter.HasBasis.map, ENNReal.coe_zero, Asymptotics.isLittleOTVS_iff, Filter.HasBasis.tendsto_right_iff, nhds_bot_basis_Iic
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ ⊥ →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (i : ℝ≥0), ⊥ < i → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) / egauge 𝕜 V (g x) ∈ ENNReal.ofNNReal '' Iic i

Tactic:
simp +contextual [ENNReal.div_le_iff_le_mul, pos_iff_ne_zero, EventuallyLE]

Premises used: ENNReal.div_le_iff_le_mul, Filter.EventuallyLE, pos_iff_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
obtain :
  ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
    ∃ (V : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) V ∧
        ∀ (ε : ℝ≥0∞),
          ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)

Tactic:
obtain ⟨V, hV₀, hV⟩ := h.exists_eventuallyLE_mul U hU

Premises used: Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)

Tactic:
⟨V, hV₀, fun ε hε ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
refine :
  ∀ (ε : ℝ≥0∞) (hε : ε ≠ 0),
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)

Tactic:
refine ⟨V, hV₀, fun ε hε ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
hε : Ne (α := ℝ≥0∞) ∞ 0
x : α
grw : 1 * egauge 𝕜 V (g x) ≤ 1 * egauge 𝕜 V (g x)
grw₁ : ℝ≥0∞
grw₂ : 1 * egauge 𝕜 V (g x) ≤ 1 * egauge 𝕜 V (g x)
grw₃ : ℝ≥0∞
⊢ 1 * egauge 𝕜 V (g x) ≤ ∞ * egauge 𝕜 V (g x)

Tactic:
grw [← le_top]

Premises used: le_top
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
hε : Ne (α := ℝ≥0∞) ∞ 0
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ∞ * egauge 𝕜 V (g x)

Tactic:
exact (hV 1 one_ne_zero).trans <| .of_forall fun _ ↦ by dsimp; grw [← le_top]

Premises used: one_ne_zero, OfNat.ofNat, Filter.EventuallyLE.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : (↑ε : ℝ≥0∞) ≠ 0
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
hV ε (mod_cast hε)

Premises used: ENNReal.ofNNReal, congrArg, cast, Ne, ENNReal.coe_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : (↑ε : ℝ≥0∞) ≠ 0
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
exact hV ε (mod_cast hε)

Premises used: ENNReal.ofNNReal, congrArg, cast, Ne, ENNReal.coe_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0∞
hε : ε ≠ 0
top :
  ∀ (hε : Ne (α := ℝ≥0∞) ∞ 0),
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ∞ * egauge 𝕜 V (g x)
coe :
  ∀ (ε : ℝ≥0) (hε : (↑ε : ℝ≥0∞) ≠ 0),
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)

Tactic:
cases ε with
  | top => exact (hV 1 one_ne_zero).trans <| .of_forall fun _ ↦ by dsimp; grw [← le_top]
  | coe ε => exact hV ε (mod_cast hε)

Premises used: one_ne_zero, OfNat.ofNat, Filter.EventuallyLE.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
simp :
  (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)
⊢ f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂

Tactic:
simp only [isLittleOTVS_iff_tendsto_div]

Premises used: Asymptotics.isLittleOTVS_iff_tendsto_div
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
h :
  ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U) (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V),
    Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0) ↔
      Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)

Tactic:
peel with U hU V hV
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)

Tactic:
tendsto_congr' (hf.comp₂ (egauge _ _ · / egauge _ _ ·) hg)

Premises used: HDiv.hDiv, Filter.EventuallyEq.comp₂, Filter.tendsto_congr', 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 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)

Tactic:
exact tendsto_congr' (hf.comp₂ (egauge _ _ · / egauge _ _ ·) hg)

Premises used: HDiv.hDiv, Filter.EventuallyEq.comp₂, Filter.tendsto_congr', 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 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
h : f₁ =o[𝕜; l] g₁
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₂ =o[𝕜; l] g₂

Tactic:
(isLittleOTVS_congr hf hg).mp h

Premises used: Asymptotics.isLittleOTVS_congr, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
h : f₁ =o[𝕜; l] g₁
hf : ∀ (x : α), f₁ x = f₂ x
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f₂ =o[𝕜; l] g₂

Tactic:
h.congr' (univ_mem' hf) (univ_mem' hg)

Premises used: Asymptotics.IsLittleOTVS.congr', Filter.univ_mem'
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g : α → F
l : Filter α
h : f₁ =o[𝕜; l] g
hf : ∀ (x : α), f₁ x = f₂ x
⊢ f₂ =o[𝕜; l] g

Tactic:
h.congr hf fun _ ↦ rfl

Premises used: Asymptotics.IsLittleOTVS.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g₁ g₂ : α → F
l : Filter α
h : f =o[𝕜; l] g₁
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f =o[𝕜; l] g₂

Tactic:
h.congr (fun _ ↦ rfl) hg

Premises used: Asymptotics.IsLittleOTVS.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
simp :
  (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x)) fun (x : α) ↦ egauge 𝕜 V (g₁ x)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x)) fun (x : α) ↦ egauge 𝕜 V (g₂ x)
⊢ f₁ =O[𝕜; l] g₁ ↔ f₂ =O[𝕜; l] g₂

Tactic:
simp only [isBigOTVS_iff]

Premises used: Asymptotics.isBigOTVS_iff
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
h :
  ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U) (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V),
    (l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x)) fun (x : α) ↦ egauge 𝕜 V (g₁ x)) ↔
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x)) fun (x : α) ↦ egauge 𝕜 V (g₂ x)
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x)) fun (x : α) ↦ egauge 𝕜 V (g₁ x)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x)) fun (x : α) ↦ egauge 𝕜 V (g₂ x)

Tactic:
peel with U hU V hV
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
⊢ (l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x)) fun (x : α) ↦ egauge 𝕜 V (g₁ x)) ↔
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x)) fun (x : α) ↦ egauge 𝕜 V (g₂ x)

Tactic:
eventuallyLE_congr (hf.fun_comp (egauge 𝕜 U)) (hg.fun_comp (egauge 𝕜 V))

Premises used: Filter.eventuallyLE_congr, Filter.EventuallyEq.fun_comp, 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 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
⊢ (l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x)) fun (x : α) ↦ egauge 𝕜 V (g₁ x)) ↔
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x)) fun (x : α) ↦ egauge 𝕜 V (g₂ x)

Tactic:
exact eventuallyLE_congr (hf.fun_comp (egauge 𝕜 U)) (hg.fun_comp (egauge 𝕜 V))

Premises used: Filter.eventuallyLE_congr, Filter.EventuallyEq.fun_comp, 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 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
h : f₁ =O[𝕜; l] g₁
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₂ =O[𝕜; l] g₂

Tactic:
(isBigOTVS_congr hf hg).mp h

Premises used: Asymptotics.isBigOTVS_congr, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
h : f₁ =O[𝕜; l] g₁
hf : ∀ (x : α), f₁ x = f₂ x
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f₂ =O[𝕜; l] g₂

Tactic:
h.congr' (univ_mem' hf) (univ_mem' hg)

Premises used: Asymptotics.IsBigOTVS.congr', Filter.univ_mem'
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f₁ f₂ : α → E
g : α → F
l : Filter α
h : f₁ =O[𝕜; l] g
hf : ∀ (x : α), f₁ x = f₂ x
⊢ f₂ =O[𝕜; l] g

Tactic:
h.congr hf fun _ ↦ rfl

Premises used: Asymptotics.IsBigOTVS.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.TVS
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
f : α → E
g₁ g₂ : α → F
l : Filter α
h : f =O[𝕜; l] g₁
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f =O[𝕜; l] g₂

Tactic:
h.congr (fun _ ↦ rfl) hg

Premises used: Asymptotics.IsBigOTVS.congr, rfl
-- 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
f : α → E
l : Filter α
rw :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (f x)
⊢ f =O[𝕜; l] f

Tactic:
rw [isBigOTVS_iff]

Premises used: Asymptotics.isBigOTVS_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
f : α → E
l : Filter α
⊢ ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (f x)

Tactic:
fun U hU ↦ ⟨U, hU, EventuallyLE.rfl⟩

Premises used: Filter.EventuallyLE.rfl, And.intro, Exists.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
f : α → E
l : Filter α
⊢ ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (f x)

Tactic:
exact fun U hU ↦ ⟨U, hU, EventuallyLE.rfl⟩