-- Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
theorem IsBoundedBilinearMap.hasStrictFDerivAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    HasStrictFDerivAt b (h.deriv p) p

Proof state:
case h.mk.mk.mk.mk
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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
⊢ ((fun p => b p.1 - b p.2 - (h.deriv (x, y)) (p.1 - p.2)) ∘ fun x_1 => ((x, y), x, y) + x_1) ((x₁, y₁), x₂, y₂) =
    (h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2)) (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2)

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]

Result:
case h.mk.mk.mk.mk
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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₂)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ((fun p_1 => b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x => (p, p) + x) = fun x =>
    (h.deriv (x.1 - x.2)) (x.2.1, x.1.2)

Tactic:
ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩

Result:
case h.mk.mk.mk
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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
⊢ ((fun p_1 => b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x => (p, p) + x) ((x₁, y₁), x₂, y₂) =
    (h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2)) (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ (fun p_1 => b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) =o[𝓝 (p, p)] fun p => p.1 - p.2

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

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ ((fun p_1 => b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x => (p, p) + x) =o[𝓝 0]
    ((fun p => p.1 - p.2) ∘ fun x => (p, p) + x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => (h.deriv (x.1 - x.2)) (x.2.1, x.1.2)) =o[𝓝 0] fun x => x.1 - x.2

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

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x => x.1 - x.2

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x => 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

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x => ‖x.1 - x.2‖ * 1

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ ((fun p_1 => b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x => (p, p) + x) =o[𝓝 0]
    ((fun p => p.1 - p.2) ∘ fun x => (p, p) + x)

Tactic:
set T := (E × F) × E × F

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ((fun p_1 => b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x => (p, p) + x) =o[𝓝 0]
    ((fun p => p.1 - p.2) ∘ fun x => (p, p) + x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ (fun x => ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x => ‖x.1 - x.2‖ * 1

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

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 => ‖(x.2.1, x.1.2)‖) (𝓝 0) (𝓝 0)