awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
⊢ IsBoundedLinearMap.{u_1, u_2, u_3} 𝕜 (F := F) fun (e : E) ↦ f e - g e

Tactic:
simpa [sub_eq_add_neg] using add hf (neg hg)

Premises used: sub_eq_add_neg, IsBoundedLinearMap.add, IsBoundedLinearMap.neg
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E → F
g : F → G
hg : IsBoundedLinearMap 𝕜 g
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left_1 : 0 < Mg
hMg : ∀ (x : F), ‖g x‖ ≤ Mg * ‖x‖
x : E
grw : Mg * ‖f x‖ ≤ Mg * Mf * ‖x‖
grw₁ : Mg * (Mf * ‖x‖) ≤ Mg * Mf * ‖x‖
grw₂ grw₃ : Mg * (Mf * ‖x‖) ≤ Mg * (Mf * ‖x‖)
⊢ ‖g (f x)‖ ≤ Mg * Mf * ‖x‖

Tactic:
grw [hMg, hMf, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
x : E
hf : IsBoundedLinearMap 𝕜 f
⊢ Tendsto f (𝓝 x) (𝓝 (f x))

Tactic:
hf.toContinuousLinearMap.continuous.tendsto x

Premises used: IsBoundedLinearMap.toContinuousLinearMap, Continuous.tendsto, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
hf.toContinuousLinearMap.continuous

Premises used: IsBoundedLinearMap.toContinuousLinearMap, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ Tendsto f (𝓝 0) (𝓝 0)

Tactic:
(hf.1.mk' _).map_zero ▸ hf.tendsto 0

Premises used: LinearMap.map_zero, Eq.rec, IsBoundedLinearMap.toIsLinearMap, IsBoundedLinearMap.tendsto, IsLinearMap.mk', OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
h : IsBoundedLinearMap 𝕜 f
l : Filter E
⊢ IsBigO (F := E) l f fun (x : E) ↦ x

Tactic:
let ⟨_, _, hM⟩ := h.bound
  IsBigO.of_bound _ (mem_of_superset univ_mem fun x _ => hM x)

Premises used: _private.0.IsBoundedLinearMap.isBigO_id.match_1, Asymptotics.IsBigO, IsBoundedLinearMap.bound, Asymptotics.IsBigO.of_bound, Filter.univ_mem, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : SeminormedAddCommGroup G
inst_4 : Module 𝕜 G
E : Type u_5
g : F → G
hg : IsBoundedLinearMap 𝕜 g
f : E → F
l : Filter E
⊢ IsBigO.{u_5, u_4, u_3} (E := G) l (fun (x' : E) ↦ g (f x')) f

Tactic:
(hg.isBigO_id ⊤).comp_tendsto le_top

Premises used: le_top, Asymptotics.IsBigO.comp_tendsto, Top.top, IsBoundedLinearMap.isBigO_id
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
h : IsBoundedLinearMap 𝕜 f
l : Filter E
x : E
⊢ IsBigO.{u_2, u_3, u_2} (E := F) (F := E) l (fun (x' : E) ↦ f (x' - x)) fun (x' : E) ↦ x' - x

Tactic:
isBigO_comp h l

Premises used: IsBoundedLinearMap.isBigO_comp
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
obtain :
  ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖),
    ∃ C > 0, ∀ (x : F) (y : E), ‖f ((x, y).2, (x, y).1)‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∃ C > 0, ∀ (x : F) (y : E), ‖f ((x, y).2, (x, y).1)‖ ≤ C * ‖x‖ * ‖y‖

Tactic:
obtain ⟨C, hC_pos, hC⟩ := h.bound

Premises used: IsBoundedBilinearMap.bound
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x : F
y : E
⊢ C * ‖y‖ * ‖x‖ = C * ‖x‖ * ‖y‖

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∃ C > 0, ∀ (x : F) (y : E), ‖f ((x, y).2, (x, y).1)‖ ≤ C * ‖x‖ * ‖y‖

Tactic:
exact ⟨C, hC_pos, fun x y ↦ (hC y x).trans_eq (by ring)⟩
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
let :
  ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖),
    ∃ (M : ℝ), 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖
⊢ ∃ (M : ℝ), 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖

Tactic:
let ⟨C, hC_pos, hC⟩ := h.bound
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
⊢ 0 < C * max ‖x‖ 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
refine : ∀ (y : F), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
⊢ ∃ (M : ℝ), 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖

Tactic:
refine ⟨C * max ‖x‖ 1, by positivity, fun y ↦ (hC x y).trans ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
inl : ∀ (hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
inr : ∀ (hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

Tactic:
rcases max_cases ‖x‖ 1 with hx | hx

Premises used: Norm.norm, max_cases, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖
inl inl₁ : C * ‖x‖ * ‖y‖ ≤ C * ‖x‖ * ‖y‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

Tactic:
grw [hx.1]

Premises used: And.left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
inr : C * ‖x‖ * ‖y‖ ≤ C * 1 * ‖y‖
inr₁ inr₂ : C * 1 * ‖y‖ ≤ C * 1 * ‖y‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

Tactic:
grw [hx.1, hx.2.le]

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
y : F
⊢ IsBoundedLinearMap.{u_1, u_2, u_4} 𝕜 (F := G) fun (x : E) ↦ f (x, y)

Tactic:
h.symm.isBoundedLinearMap_right y

Premises used: IsBoundedBilinearMap.isBoundedLinearMap_right, IsBoundedBilinearMap.symm
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x y : E
z : F
⊢ f (x - y, z) = f (x, z) - f (y, z)

Tactic:
(h.isBoundedLinearMap_left z).map_sub x y

Premises used: IsBoundedBilinearMap.isBoundedLinearMap_left, IsLinearMap.map_sub, IsBoundedLinearMap.toIsLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
y z : F
⊢ f (x, y - z) = f (x, y) - f (x, z)

Tactic:
(h.isBoundedLinearMap_right x).map_sub y z

Premises used: IsBoundedBilinearMap.isBoundedLinearMap_right, IsLinearMap.map_sub, IsBoundedLinearMap.toIsLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
left : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x_1 : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ C * ‖‖(x, y).1‖ * ‖(x, y).2‖‖

Tactic:
simpa [mul_assoc] using hC x y

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
α : Type u_5
H : IsBoundedBilinearMap 𝕜 f
g : α → E
h : α → F
l : Filter α
⊢ Asymptotics.IsBigO.{u_5, u_4, 0} (E := G) (F := ℝ) l (fun (x : α) ↦ f (g x, h x)) fun (x : α) ↦ ‖g x‖ * ‖h x‖

Tactic:
H.isBigO.comp_tendsto le_top

Premises used: le_top, IsBoundedBilinearMap.isBigO, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ Asymptotics.IsBigO (F := ℝ) ⊤ f fun (p : E × F) ↦ ‖p‖ * ‖p‖

Tactic:
h.isBigO.trans <|
    (@Asymptotics.isBigO_fst_prod' _ E F _ _ _ _).norm_norm.mul
      (@Asymptotics.isBigO_snd_prod' _ E F _ _ _ _).norm_norm

Premises used: Asymptotics.isBigO_fst_prod', Asymptotics.IsBigO.norm_norm, Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Asymptotics.isBigO_snd_prod', IsBoundedBilinearMap.isBigO
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_

Premises used: Iff.mpr, Iff.mp, tendsto_sub_nhds_zero_iff, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
refine : ∀ (x : E × F), Tendsto (β := G) (fun (x_1 : E × F) ↦ f x_1 - f x) (𝓝 x) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_

Premises used: Iff.mpr, Iff.mp, tendsto_sub_nhds_zero_iff, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
this : Tendsto (fun (y : E × F) ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (HAdd.hAdd (α := G) 0 0))
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f x_1 - f x) (𝓝 x) (𝓝 0)

Tactic:
simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this

Premises used: sub_add_sub_cancel, zero_add, IsBoundedBilinearMap.map_sub_left, IsBoundedBilinearMap.map_sub_right
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
suffices : Tendsto (fun (y : E × F) ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (HAdd.hAdd (α := G) 0 0))
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f x_1 - f x) (𝓝 x) (𝓝 0)

Tactic:
suffices Tendsto (fun y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
    simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hf : Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) (𝓝 x) (𝓝 0)
hg : Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)
⊢ Tendsto (fun (y : E × F) ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (HAdd.hAdd (α := G) 0 0))

Tactic:
apply Tendsto.add

Premises used: Filter.Tendsto.add
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hf :
  IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) (𝓝 x) (𝓝 0)

Tactic:
rw [← isLittleO_one_iff ℝ, ← one_mul 1]

Premises used: Real, Asymptotics.isLittleO_one_iff, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
h.isBigO_comp.trans_isLittleO ?_

Premises used: IsBoundedBilinearMap.isBigO_comp, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hf :
  IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.1 - x.1‖ * ‖x_1.2‖) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1
⊢ IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
refine h.isBigO_comp.trans_isLittleO ?_

Premises used: IsBoundedBilinearMap.isBigO_comp, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.1 - x.1‖ * ‖x_1.2‖) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
(IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsLittleO.norm_left, Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hf : IsLittleO (E := E) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ x_1.1 - x.1) fun (_x : E × F) ↦ 1
hf₁ : IsBigO (F := ℝ) (𝓝 x) Prod.snd fun (_x : E × F) ↦ 1
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.1 - x.1‖ * ‖x_1.2‖) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsLittleO.norm_left, Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := E) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ x_1.1 - x.1) fun (_x : E × F) ↦ 1

Tactic:
(isLittleO_one_iff _).2 (tendsto_sub_nhds_zero_iff.2 (continuous_fst.tendsto _))

Premises used: Iff.mpr, continuous_fst, Continuous.tendsto, Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := E) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ x_1.1 - x.1) fun (_x : E × F) ↦ 1

Tactic:
exact (isLittleO_one_iff _).2 (tendsto_sub_nhds_zero_iff.2 (continuous_fst.tendsto _))

Premises used: Iff.mpr, continuous_fst, Continuous.tendsto, Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsBigO (F := ℝ) (𝓝 x) Prod.snd fun (_x : E × F) ↦ 1

Tactic:
(continuous_snd.tendsto _).isBigO_one ℝ

Premises used: Filter.Tendsto.isBigO_one, Real, continuous_snd, Continuous.tendsto
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsBigO (F := ℝ) (𝓝 x) Prod.snd fun (_x : E × F) ↦ 1

Tactic:
exact (continuous_snd.tendsto _).isBigO_one ℝ

Premises used: Filter.Tendsto.isBigO_one, Real, continuous_snd, Continuous.tendsto
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hg : IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) fun (_x : E × F) ↦ 1
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)

Tactic:
rw [← isLittleO_one_iff ℝ]

Premises used: Real, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) fun (_x : E × F) ↦ 1

Tactic:
h.isBigO_comp.trans_isLittleO ?_

Premises used: IsBoundedBilinearMap.isBigO_comp, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hg : IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x.1‖ * ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1
⊢ IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) fun (_x : E × F) ↦ 1

Tactic:
refine h.isBigO_comp.trans_isLittleO ?_

Premises used: IsBoundedBilinearMap.isBigO_comp, Asymptotics.IsBigO.trans_isLittleO