[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f✝ g✝ : G → E
f'✝ g'✝ : G →L[ℝ] E
s✝ : Set G
x✝ : G
n : ℕ∞
f g : ℝ → E
f' g' : E
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
⊢ HasDerivWithinAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) s x
[PROOFSTEP]
simpa using (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).hasDerivWithinAt
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f✝ g✝ : G → E
f'✝ g'✝ : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
f g : ℝ → E
f' g' : E
x : ℝ
⊢ HasDerivAt f f' x →
    HasDerivAt g g' x → HasDerivAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) x
[PROOFSTEP]
simpa only [← hasDerivWithinAt_univ] using HasDerivWithinAt.inner 𝕜
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ ↑(fderiv ℝ (fun t => inner (f t) (g t)) x) y = inner (f x) (↑(fderiv ℝ g x) y) + inner (↑(fderiv ℝ f x) y) (g x)
[PROOFSTEP]
rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ ↑(ContinuousLinearMap.comp (fderivInnerClm 𝕜 (f x, g x)) (ContinuousLinearMap.prod (fderiv ℝ f x) (fderiv ℝ g x))) y =
    inner (f x) (↑(fderiv ℝ g x) y) + inner (↑(fderiv ℝ f x) y) (g x)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
⊢ ContDiff ℝ n fun x => ‖x‖ ^ 2
[PROOFSTEP]
convert (reClm : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))
[GOAL]
case h.e'_10.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
x✝ : E
⊢ ‖x✝‖ ^ 2 = (↑reClm ∘ fun x => inner (id x) (id x)) x✝
[PROOFSTEP]
exact (inner_self_eq_norm_sq _).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
[PROOFSTEP]
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
[PROOFSTEP]
simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => Dist.dist (f y) (g y)) x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => ‖f y - g y‖) x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => Dist.dist (f y) (g y)) s x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => ‖f y - g y‖) s x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
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
[PROOFSTEP]
simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
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
[PROOFSTEP]
convert (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)
[GOAL]
case h.e'_10.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
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))
[PROOFSTEP]
ext y
[GOAL]
case h.e'_10.h.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
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
[PROOFSTEP]
simp [two_smul, real_inner_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => Dist.dist (f y) (g y)) x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => ‖f y - g y‖) x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => Dist.dist (f y) (g y)) s x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => ‖f y - g y‖) s x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiableWithinAt_iff, differentiableWithinAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiableAt_iff, differentiableAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableAt 𝕜 (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiableOn_iff, differentiableOn_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableOn 𝕜 (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => f x i
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiable_iff, differentiable_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), Differentiable 𝕜 fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable 𝕜 fun x => f x i
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_pi']
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i)
        (comp (proj i) (comp (↑(EuclideanSpace.equiv ι 𝕜)) f')) y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') t y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_pi']
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i)
        (comp (proj i) (comp (↑(EuclideanSpace.equiv ι 𝕜)) f')) t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') t y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiffWithinAt_iff, contDiffWithinAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiffAt_iff, contDiffAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiffAt 𝕜 n (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiffOn_iff, contDiffOn_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiffOn 𝕜 n (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiff_iff, contDiff_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
[PROOFSTEP]
rfl
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n ↑univUnitBall
[PROOFSTEP]
suffices ContDiff ℝ n fun x : E => ((1 : ℝ) + ‖x‖ ^ 2).sqrt⁻¹ from this.smul contDiff_id
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
[PROOFSTEP]
have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
[PROOFSTEP]
refine' ContDiff.inv _ fun x => Real.sqrt_ne_zero'.mpr (h x)
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffWithinAt ℝ n (↑(LocalHomeomorph.symm univUnitBall)) (ball 0 1) y
[PROOFSTEP]
apply ContDiffAt.contDiffWithinAt
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ n (↑(LocalHomeomorph.symm univUnitBall)) y
[PROOFSTEP]
suffices ContDiffAt ℝ n (fun y : E => ((1 : ℝ) - ‖y‖ ^ 2).sqrt⁻¹) y from this.smul contDiffAt_id
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
[PROOFSTEP]
have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by
  rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy 
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2
[PROOFSTEP]
rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy 
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
[PROOFSTEP]
refine' ContDiffAt.inv _ (Real.sqrt_ne_zero'.mpr h)
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => sqrt (1 - ‖y‖ ^ 2)) y
[PROOFSTEP]
refine' (contDiffAt_sqrt h.ne').comp y _
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => 1 - ‖y‖ ^ 2) y
[PROOFSTEP]
exact contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ n ↑(univBall c r)
[PROOFSTEP]
unfold univBall
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ n
    ↑(if h : 0 < r then
        LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
      else Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiff ℝ n
    ↑(LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
        (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target))
[PROOFSTEP]
exact (contDiff_unitBallBall h).comp contDiff_univUnitBall
[GOAL]
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ n ↑(Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))
[PROOFSTEP]
exact contDiff_id.add contDiff_const
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ n (↑(LocalHomeomorph.symm (univBall c r))) (ball c r)
[PROOFSTEP]
unfold univBall
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ n
    (↑(LocalHomeomorph.symm
        (if h : 0 < r then
          LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
            (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
        else Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    (ball c r)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ n
    (↑(LocalHomeomorph.symm
        (LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target))))
    (ball c r)
[PROOFSTEP]
refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ball c r ⊆ (fun x => ↑(LocalEquiv.symm (unitBallBall c r h).toLocalEquiv) x) ⁻¹' ball 0 1
[PROOFSTEP]
rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ (unitBallBall c r h).toLocalEquiv.target ⊆
    (fun x => ↑(LocalEquiv.symm (unitBallBall c r h).toLocalEquiv) x) ⁻¹' (unitBallBall c r h).toLocalEquiv.source
[PROOFSTEP]
apply LocalHomeomorph.symm_mapsTo
[GOAL]
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ n
    (↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    (ball c r)
[PROOFSTEP]
exact contDiffOn_id.sub contDiffOn_const
