𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
⊢ HasStrictFDerivAt (fun x => ↑re (inner x x)) (2 • ↑(innerSL ℝ) x) x
𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • ↑(innerSL ℝ) x) x
simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]
case h.e'_10.h.h
𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ 2 • ↑(innerSL ℝ) x =
    ContinuousLinearMap.comp (fderivInnerClm ℝ (id x, id x))
      (ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F))
𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
⊢ HasStrictFDerivAt (fun x => ↑re (inner x x)) (2 • ↑(innerSL ℝ) x) x
convert (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)
case h.e'_10.h.h.h
𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'
y : F
⊢ ↑(2 • ↑(innerSL ℝ) x) y =
    ↑(ContinuousLinearMap.comp (fderivInnerClm ℝ (id x, id x))
          (ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)))
      y
case h.e'_10.h.h
𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ 2 • ↑(innerSL ℝ) x =
    ContinuousLinearMap.comp (fderivInnerClm ℝ (id x, id x))
      (ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F))
ext y
no goals
case h.e'_10.h.h.h
𝕜 : Type ?u.299226
E : Type ?u.299229
F : Type u_1
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.299361
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'
y : F
⊢ ↑(2 • ↑(innerSL ℝ) x) y =
    ↑(ContinuousLinearMap.comp (fderivInnerClm ℝ (id x, id x))
          (ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)))
      y
simp [two_smul, real_inner_comm]