awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
simp_rw : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'
⊢ g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Tactic:
simp_rw [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'

Tactic:
forall_congr' fun c => forall_congr' fun hc => ?_

Premises used: forall_congr'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
refine : ∀ (c : ℝ) (hc : 0 < c), IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'

Tactic:
refine forall_congr' fun c => forall_congr' fun hc => ?_

Premises used: forall_congr'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
rw : ‖g x‖ ≤ c * ‖g' x‖
⊢ IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'

Tactic:
rw [isBigOWith_insert]

Premises used: Asymptotics.isBigOWith_insert
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
rw : 0 ≤ c * ‖g' x‖
⊢ ‖g x‖ ≤ c * ‖g' x‖

Tactic:
rw [h, norm_zero]

Premises used: norm_zero
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ 0 ≤ c * ‖g' x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
inst_2 : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h1 : g =o[𝓝[s] x] g'
h2 : g x = 0
⊢ g =o[𝓝[insert x s] x] g'

Tactic:
(isLittleO_insert h2).mpr h1

Premises used: Iff.mpr, Asymptotics.isLittleO_insert
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ IsBigOWith c l f g'

Tactic:
simp only [IsBigOWith_def, norm_norm]

Premises used: Asymptotics.IsBigOWith_def, norm_norm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
c : ℝ
f : α → E
l : Filter α
u : α → ℝ
⊢ (IsBigOWith (F := ℝ) c l f fun (x : α) ↦ |u x|) ↔ IsBigOWith c l f u

Tactic:
@isBigOWith_norm_right _ _ _ _ _ _ f u l

Premises used: Asymptotics.isBigOWith_norm_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
simp : (∃ (c : ℝ), IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∃ (c : ℝ), IsBigOWith c l f g'
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖g' x‖) ↔ f =O[l] g'

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∃ (c : ℝ), IsBigOWith c l f g'

Tactic:
exists_congr fun _ => isBigOWith_norm_right

Premises used: Asymptotics.isBigOWith_norm_right, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∃ (c : ℝ), IsBigOWith c l f g'

Tactic:
exact exists_congr fun _ => isBigOWith_norm_right

Premises used: Asymptotics.isBigOWith_norm_right, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
u : α → ℝ
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ |u x|) ↔ f =O[l] u

Tactic:
@isBigO_norm_right _ _ ℝ _ _ _ _ _

Premises used: Asymptotics.isBigO_norm_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ ‖g' x‖) ↔ f =o[l] g'

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
forall₂_congr fun _ _ => isBigOWith_norm_right

Premises used: Asymptotics.isBigOWith_norm_right, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := ℝ) c l f fun (x : α) ↦ ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_norm_right

Premises used: Asymptotics.isBigOWith_norm_right, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
u : α → ℝ
⊢ (IsLittleO (F := ℝ) l f fun (x : α) ↦ |u x|) ↔ f =o[l] u

Tactic:
@isLittleO_norm_right _ _ ℝ _ _ _ _ _

Premises used: Asymptotics.isLittleO_norm_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g ↔ IsBigOWith c l f' g

Tactic:
simp only [IsBigOWith_def, norm_norm]

Premises used: Asymptotics.IsBigOWith_def, norm_norm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
inst : Norm F
c : ℝ
g : α → F
l : Filter α
u : α → ℝ
⊢ IsBigOWith (E := ℝ) c l (fun (x : α) ↦ |u x|) g ↔ IsBigOWith c l u g

Tactic:
@isBigOWith_norm_left _ _ _ _ _ _ g u l

Premises used: Asymptotics.isBigOWith_norm_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
simp : (∃ (c : ℝ), IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =O[l] g

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g

Tactic:
exists_congr fun _ => isBigOWith_norm_left

Premises used: Asymptotics.isBigOWith_norm_left, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g

Tactic:
exact exists_congr fun _ => isBigOWith_norm_left

Premises used: Asymptotics.isBigOWith_norm_left, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
inst : Norm F
g : α → F
l : Filter α
u : α → ℝ
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ |u x|) g ↔ u =O[l] g

Tactic:
@isBigO_norm_left _ _ _ _ _ g u l

Premises used: Asymptotics.isBigO_norm_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
simp : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =o[l] g

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g

Tactic:
forall₂_congr fun _ _ => isBigOWith_norm_left

Premises used: Asymptotics.isBigOWith_norm_left, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := ℝ) c l (fun (x : α) ↦ ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_norm_left

Premises used: Asymptotics.isBigOWith_norm_left, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
inst : Norm F
g : α → F
l : Filter α
u : α → ℝ
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ |u x|) g ↔ u =o[l] g

Tactic:
@isLittleO_norm_left _ _ _ _ _ g u l

Premises used: Asymptotics.isLittleO_norm_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
c : ℝ
f' : α → E'
g' : α → F'
l : Filter α
⊢ (IsBigOWith (E := ℝ) (F := ℝ) c l (fun (x : α) ↦ ‖f' x‖) fun (x : α) ↦ ‖g' x‖) ↔ IsBigOWith c l f' g'

Tactic:
isBigOWith_norm_left.trans isBigOWith_norm_right

Premises used: Asymptotics.isBigOWith_norm_right, Asymptotics.isBigOWith_norm_left, Iff.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
c : ℝ
l : Filter α
u v : α → ℝ
⊢ (IsBigOWith (E := ℝ) (F := ℝ) c l (fun (x : α) ↦ |u x|) fun (x : α) ↦ |v x|) ↔ IsBigOWith c l u v

Tactic:
isBigOWith_abs_left.trans isBigOWith_abs_right

Premises used: Asymptotics.isBigOWith_abs_left, Iff.trans, Asymptotics.isBigOWith_abs_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ (IsBigO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ ‖f' x‖) fun (x : α) ↦ ‖g' x‖) ↔ f' =O[l] g'

Tactic:
isBigO_norm_left.trans isBigO_norm_right

Premises used: Asymptotics.isBigO_norm_right, Asymptotics.isBigO_norm_left, Iff.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
l : Filter α
u v : α → ℝ
⊢ (IsBigO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ |u x|) fun (x : α) ↦ |v x|) ↔ u =O[l] v

Tactic:
isBigO_abs_left.trans isBigO_abs_right

Premises used: Asymptotics.isBigO_abs_left, Iff.trans, Asymptotics.isBigO_abs_right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ (IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ ‖f' x‖) fun (x : α) ↦ ‖g' x‖) ↔ f' =o[l] g'

Tactic:
isLittleO_norm_left.trans isLittleO_norm_right

Premises used: Asymptotics.isLittleO_norm_right, Asymptotics.isLittleO_norm_left, Iff.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
l : Filter α
u v : α → ℝ
⊢ (IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ |u x|) fun (x : α) ↦ |v x|) ↔ u =o[l] v

Tactic:
isLittleO_abs_left.trans isLittleO_abs_right

Premises used: Asymptotics.isLittleO_abs_right, Iff.trans, Asymptotics.isLittleO_abs_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔ IsBigOWith c l f g'

Tactic:
simp only [IsBigOWith_def, norm_neg]

Premises used: Asymptotics.IsBigOWith_def, norm_neg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
simp : (∃ (c : ℝ), IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔ ∃ (c : ℝ), IsBigOWith c l f g'
⊢ (IsBigO.{u_1, u_3, u_7} (F := F') l f fun (x : α) ↦ -g' x) ↔ f =O[l] g'

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔ ∃ (c : ℝ), IsBigOWith c l f g'

Tactic:
exists_congr fun _ => isBigOWith_neg_right

Premises used: Asymptotics.isBigOWith_neg_right, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔ ∃ (c : ℝ), IsBigOWith c l f g'

Tactic:
exact exists_congr fun _ => isBigOWith_neg_right

Premises used: Asymptotics.isBigOWith_neg_right, exists_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'
⊢ (IsLittleO.{u_1, u_3, u_7} (F := F') l f fun (x : α) ↦ -g' x) ↔ f =o[l] g'

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
forall₂_congr fun _ _ => isBigOWith_neg_right

Premises used: Asymptotics.isBigOWith_neg_right, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_3, u_7} (F := F') c l f fun (x : α) ↦ -g' x) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_neg_right

Premises used: Asymptotics.isBigOWith_neg_right, forall₂_congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g ↔ IsBigOWith c l f' g

Tactic:
simp only [IsBigOWith_def, norm_neg]

Premises used: Asymptotics.IsBigOWith_def, norm_neg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
simp : (∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ -f' x) g ↔ f' =O[l] g

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g

Tactic:
exists_congr fun _ => isBigOWith_neg_left

Premises used: exists_congr, Asymptotics.isBigOWith_neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ (c : ℝ), IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔ ∃ (c : ℝ), IsBigOWith c l f' g

Tactic:
exact exists_congr fun _ => isBigOWith_neg_left

Premises used: exists_congr, Asymptotics.isBigOWith_neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ -f' x) g ↔ f' =o[l] g

Tactic:
simp only [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g

Tactic:
forall₂_congr fun _ _ => isBigOWith_neg_left

Premises used: forall₂_congr, Asymptotics.isBigOWith_neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_6, u_4} (E := E') c l (fun (x : α) ↦ -f' x) g) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_neg_left

Premises used: forall₂_congr, Asymptotics.isBigOWith_neg_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ IsBigOWith (F := E' × F') 1 l f' fun (x : α) ↦ (f' x, g' x)

Tactic:
isBigOWith_of_le l fun _x => le_max_left _ _

Premises used: Norm.norm, Prod.mk, Asymptotics.isBigOWith_of_le, le_max_left, Prod.snd
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ IsBigOWith (F := E' × F') 1 l g' fun (x : α) ↦ (f' x, g' x)

Tactic:
isBigOWith_of_le l fun _x => le_max_right _ _

Premises used: le_max_right, Norm.norm, Prod.mk, Asymptotics.isBigOWith_of_le, Prod.fst
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ IsBigO (F := E' × F') l f' fun (x : α) ↦ (f' x, g' x)

Tactic:
isBigOWith_fst_prod.isBigO

Premises used: Asymptotics.IsBigOWith.isBigO, Asymptotics.isBigOWith_fst_prod
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
⊢ IsBigO (F := E' × F') l g' fun (x : α) ↦ (f' x, g' x)

Tactic:
isBigOWith_snd_prod.isBigO

Premises used: Asymptotics.isBigOWith_snd_prod, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
l : Filter α
f' : α → E' × F'
⊢ IsBigO (E := E') l (fun (x : α) ↦ (f' x).1) f'

Tactic:
simpa [IsBigO_def, IsBigOWith_def] using isBigO_fst_prod (E' := E') (F' := F')

Premises used: Asymptotics.IsBigOWith_def, Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
l : Filter α
f' : α → E' × F'
⊢ IsBigO (E := F') l (fun (x : α) ↦ (f' x).2) f'

Tactic:
simpa [IsBigO_def, IsBigOWith_def] using isBigO_snd_prod (E' := E') (F' := F')

Premises used: Asymptotics.IsBigOWith_def, Asymptotics.IsBigO_def, Asymptotics.isBigO_snd_prod
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
G' : Type u_8
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
c : ℝ
f : α → E
g' : α → F'
k' : α → G'
l : Filter α
h : IsBigOWith c l f g'
hc : 0 ≤ c
⊢ IsBigOWith (F := F' × G') c l f fun (x : α) ↦ (g' x, k' x)

Tactic:
(h.trans isBigOWith_fst_prod hc).congr_const (mul_one c)

Premises used: Asymptotics.IsBigOWith.trans, mul_one, Asymptotics.isBigOWith_fst_prod, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
G' : Type u_8
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f : α → E
g' : α → F'
k' : α → G'
l : Filter α
h : f =O[l] g'
⊢ IsBigO (F := F' × G') l f fun (x : α) ↦ (g' x, k' x)

Tactic:
let ⟨_c, cnonneg, hc⟩ := h.exists_nonneg
  (hc.prod_rightl k' cnonneg).isBigO

Premises used: _private.0.Asymptotics.IsBigO.prod_rightl.match_1, Asymptotics.IsBigO, Prod.mk, Asymptotics.IsBigO.exists_nonneg, Asymptotics.IsBigOWith.prod_rightl, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
G' : Type u_8
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f : α → E
g' : α → F'
k' : α → G'
l : Filter α
h : f =o[l] g'
⊢ IsLittleO (F := F' × G') l f fun (x : α) ↦ (g' x, k' x)

Tactic:
IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).prod_rightl k' cpos.le

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, LT.lt.le, Asymptotics.IsBigOWith.prod_rightl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
c : ℝ
f : α → E
f' : α → E'
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : 0 ≤ c
⊢ IsBigOWith (F := E' × F') c l f fun (x : α) ↦ (f' x, g' x)

Tactic:
(h.trans isBigOWith_snd_prod hc).congr_const (mul_one c)

Premises used: Asymptotics.IsBigOWith.trans, Asymptotics.isBigOWith_snd_prod, mul_one, Asymptotics.IsBigOWith.congr_const
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
f : α → E
f' : α → E'
g' : α → F'
l : Filter α
h : f =O[l] g'
⊢ IsBigO (F := E' × F') l f fun (x : α) ↦ (f' x, g' x)

Tactic:
let ⟨_c, cnonneg, hc⟩ := h.exists_nonneg
  (hc.prod_rightr f' cnonneg).isBigO

Premises used: _private.0.Asymptotics.IsBigO.prod_rightl.match_1, Asymptotics.IsBigO, Prod.mk, Asymptotics.IsBigO.exists_nonneg, Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigOWith.prod_rightr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
f : α → E
f' : α → E'
g' : α → F'
l : Filter α
h : f =o[l] g'
⊢ IsLittleO (F := E' × F') l f fun (x : α) ↦ (f' x, g' x)

Tactic:
IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).prod_rightr f' cpos.le

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, LT.lt.le, Asymptotics.IsBigOWith.prod_rightr