awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup V'
inst_4 : NormedSpace 𝕜 V'
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
inst_7 : NormedAddCommGroup W'
inst_8 : NormedSpace 𝕜 W'
inst_9 : RingHomIsometric σ
inst_10 : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
f' : V →L[𝕜] W
hf :
  IsLittleO.{u_2, u_4, u_2} (E := W) (F := V) (𝓝 0)
    (fun (h : V) ↦
      HSub.hSub (β := W) (f (HAdd.hAdd (α := V) ((R : (a : V') → V) z : V) h) - f ((R : (a : V') → V) z))
        ((f' : (a : V) → W) h : W))
    fun (h : V) ↦ h
this_1 : RingHomIsometric σ'
this :
  IsLittleO.{u_3, u_4, u_2} (α := V') (E := W) (F := V) (𝓝 0)
    ((fun (h : V) ↦
        HSub.hSub (β := W) (f (HAdd.hAdd (α := V) ((R : (a : V') → V) z : V) h) - f ((R : (a : V') → V) z))
          ((f' : (a : V) → W) h : W)) ∘
      (⇑R : (a : V') → V))
    ((fun (h : V) ↦ h) ∘ (⇑R : (a : V') → V))
⊢ IsLittleO.{u_3, u_5, u_3} (E := W') (F := V') (𝓝 0)
    (fun (h : V') ↦
      HSub.hSub (β := W')
        (HSub.hSub (α := W') (((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) (z + h))
          (((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) z))
        ((L ∘SL f' ∘SL R : (a : V') → W') h : W'))
    fun (h : V') ↦ h

Tactic:
simpa using ((L.isBigO_comp _ _).trans_isLittleO this).trans_isBigO (R.isBigO_id _)

Premises used: ContinuousLinearMap.isBigO_comp, ContinuousLinearMap.isBigO_id, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : NormedAddCommGroup V'
inst_4 : NormedSpace 𝕜 V'
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
inst_7 : NormedAddCommGroup W'
inst_8 : NormedSpace 𝕜 W'
inst_9 : RingHomIsometric σ
inst_10 : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
hf : DifferentiableAt 𝕜 f ((R : (a : V') → V) z)
⊢ DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := W') ((⇑L : (a : W) → W') ∘ f ∘ (⇑R : (a : V') → V)) z

Tactic:
simpa using (hf.hasFDerivAt.comp_semilinear L R).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.comp_semilinear
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
simp :
  IsLittleO (E := G) (F := E × F) (𝓝 (p, p))
    (fun (p_1 : (E × F) × E × F) ↦
      HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G))
    fun (p : (E × F) × E × F) ↦ p.1 - p.2
⊢ HasStrictFDerivAt b (h.deriv p) p

Tactic:
simp only [hasStrictFDerivAt_iff_isLittleO]

Premises used: hasStrictFDerivAt_iff_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
simp :
  IsLittleO (α := (E × F) × E × F) (E := G) (F := E × F) (𝓝 0)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
⊢ IsLittleO (E := G) (F := E × F) (𝓝 (p, p))
    (fun (p_1 : (E × F) × E × F) ↦
      HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G))
    fun (p : (E × F) × E × F) ↦ p.1 - p.2

Tactic:
simp only [← map_add_left_nhds_zero (p, p), isLittleO_map]

Premises used: Prod.mk, Asymptotics.isLittleO_map, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
h₁ :
  ∀ (x₁ : E) (y₁ : F) (x₂ : E) (y₂ : F),
    Eq.{u_4 + 1} (α := G)
      (((fun (p_1 : (E × F) × E × F) ↦
              HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
            fun (x : (E × F) × E × F) ↦ (p, p) + x)
          ((x₁, y₁), x₂, y₂) :
        G)
      ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
          (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
        G)
⊢ Eq (α := (x : T) → G)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2)

Tactic:
ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
h₁ :
  ∀ (x : E) (y : F),
    Eq.{u_4 + 1} (α := G)
      (((fun (p : (E × F) × E × F) ↦
              HSub.hSub (β := G) (b p.1 - b p.2) ((h.deriv (x, y) : (a : E × F) → G) (p.1 - p.2) : G)) ∘
            fun (x_1 : (E × F) × E × F) ↦ ((x, y), x, y) + x_1)
          ((x₁, y₁), x₂, y₂) :
        G)
      ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
          (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
        G)
⊢ Eq.{u_4 + 1} (α := G)
    (((fun (p_1 : (E × F) × E × F) ↦
            HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
          fun (x : (E × F) × E × F) ↦ (p, p) + x)
        ((x₁, y₁), x₂, y₂) :
      G)
    ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
        (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
      G)

Tactic:
rcases p with ⟨x, y⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
h₁ :
  b (x, y) + b (x₁, y) + (b (x, y₁) + b (x₁, y₁)) - (b (x, y) + b (x₂, y) + (b (x, y₂) + b (x₂, y₂))) -
      (b (x, y) + b (x, y₁) + (b (x, y) + b (x₁, y)) - (b (x, y) + b (x, y₂) + (b (x, y) + b (x₂, y)))) =
    b (x₁, y₁) - b (x₂, y₂)
⊢ Eq.{u_4 + 1} (α := G)
    (((fun (p : (E × F) × E × F) ↦
            HSub.hSub (β := G) (b p.1 - b p.2) ((h.deriv (x, y) : (a : E × F) → G) (p.1 - p.2) : G)) ∘
          fun (x_1 : (E × F) × E × F) ↦ ((x, y), x, y) + x_1)
        ((x₁, y₁), x₂, y₂) :
      G)
    ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
        (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
      G)

Tactic:
simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]

Premises used: Prod.mk_add_mk, sub_add_sub_cancel, map_sub, IsBoundedBilinearMap.add_right, Prod.mk_sub_mk, IsBoundedBilinearMap.add_left, IsBoundedBilinearMap.map_sub_left, IsBoundedBilinearMap.map_sub_right, IsBoundedBilinearMap.deriv_apply, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
⊢ b (x, y) + b (x₁, y) + (b (x, y₁) + b (x₁, y₁)) - (b (x, y) + b (x₂, y) + (b (x, y₂) + b (x₂, y₂))) -
      (b (x, y) + b (x, y₁) + (b (x, y) + b (x₁, y)) - (b (x, y) + b (x, y₂) + (b (x, y) + b (x₂, y)))) =
    b (x₁, y₁) - b (x₂, y₂)

Tactic:
abel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ IsLittleO (E := G) (F := E × F) (𝓝 0) (fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2))
    fun (x : T) ↦ x.1 - x.2

Tactic:
h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_

Premises used: IsBoundedBilinearMap.toContinuousLinearMap, IsBoundedBilinearMap.isBigO_comp, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.deriv₂, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
refine : IsLittleO (E := ℝ) (F := E × F) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ x.1 - x.2
⊢ IsLittleO (E := G) (F := E × F) (𝓝 0) (fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2))
    fun (x : T) ↦ x.1 - x.2

Tactic:
refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_

Premises used: IsBoundedBilinearMap.toContinuousLinearMap, IsBoundedBilinearMap.isBigO_comp, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.deriv₂, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
this : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ ‖x.1 - x.2‖ * 1
⊢ IsLittleO (E := ℝ) (F := E × F) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ x.1 - x.2

Tactic:
simpa only [mul_one, isLittleO_norm_right] using this

Premises used: Asymptotics.isLittleO_norm_right, mul_one
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
suffices :
  IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ ‖x.1 - x.2‖ * 1
⊢ IsLittleO (E := ℝ) (F := E × F) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ x.1 - x.2

Tactic:
suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ ‖x.1 - x.2‖ * 1

Tactic:
(isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)

Premises used: Iff.mpr, Asymptotics.IsBigO.mul_isLittleO, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
refine : Filter.Tendsto (β := ℝ) (fun (x : T) ↦ ‖(x.2.1, x.1.2)‖) (𝓝 0) (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ ‖x.1 - x.2‖ * 1

Tactic:
refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)

Premises used: Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ norm (E := E × F) (0.2.1, 0.1.2) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ Filter.Tendsto (β := ℝ) (fun (x : T) ↦ ‖(x.2.1, x.1.2)‖) (𝓝 0) (𝓝 0)

Tactic:
exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)

Premises used: Continuous.norm, Continuous.tendsto'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ Eq (α := (x : T) → E × F) (fun (x : T) ↦ x.1 - x.2)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)

Tactic:
simp [T, Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
_ :
  Eq (α := (x : T) → G)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2)
_₁ :
  IsLittleO (E := G) (F := E × F) (𝓝 0) (fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2))
    fun (x : T) ↦ x.1 - x.2
_₂ :
  Eq (α := (x : T) → E × F) (fun (x : T) ↦ x.1 - x.2)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
⊢ IsLittleO (α := (E × F) × E × F) (E := G) (F := E × F) (𝓝 0)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)

Tactic:
calc
    _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) := by
      ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
      rcases p with ⟨x, y⟩
      simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
      abel
    -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
    --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
    -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
    _ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
      -- TODO : add 2 `calc` steps instead of the next 3 lines
      refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
      suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
      refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)
      -- TODO: `continuity` fails
      exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)
    _ = _ := by simp [T, Function.comp_def]

Premises used: HSub.hSub, nhds, Prod.mk, IsBoundedBilinearMap.deriv, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ HasFDerivAt b (h.deriv p) p

Tactic:
(h.hasStrictFDerivAt p).hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, IsBoundedBilinearMap.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ HasFDerivWithinAt b (h.deriv p) u p

Tactic:
(h.hasFDerivAt p).hasFDerivWithinAt

Premises used: IsBoundedBilinearMap.hasFDerivAt, HasFDerivAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ DifferentiableAt 𝕜 b p

Tactic:
(h.hasFDerivAt p).differentiableAt

Premises used: IsBoundedBilinearMap.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ DifferentiableWithinAt 𝕜 b u p

Tactic:
(h.differentiableAt p).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, IsBoundedBilinearMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ fderiv 𝕜 b p = h.deriv p

Tactic:
HasFDerivAt.fderiv (h.hasFDerivAt p)

Premises used: IsBoundedBilinearMap.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
rw : fderiv 𝕜 b p = h.deriv p
⊢ fderivWithin 𝕜 b u p = h.deriv p

Tactic:
rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]

Premises used: DifferentiableAt.fderivWithin, IsBoundedBilinearMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = h.deriv p

Tactic:
h.fderiv p

Premises used: IsBoundedBilinearMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = h.deriv p

Tactic:
exact h.fderiv p

Premises used: IsBoundedBilinearMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
⊢ Differentiable 𝕜 b

Tactic:
fun x => h.differentiableAt x

Premises used: Differentiable, IsBoundedBilinearMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
⊢ DifferentiableOn 𝕜 b u

Tactic:
h.differentiable.differentiableOn

Premises used: Differentiable.differentiableOn, IsBoundedBilinearMap.differentiable