Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case pos.hc
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm) s x

pp: case pos.hu
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ V (f y)) s x

pp: case pos.hxs
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 s x

pp: case pos.hc
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm) s x

pp: case pos.hu
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ W (f y)) s x

Tactic:
· exact M_symm_smooth.differentiableWithinAt one_ne_zero

Goal state after:
case pos.hu
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ V (f y)) s x

case pos.hxs
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 s x

case pos.hc
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm) s x

case pos.hu
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (fun y ↦ W (f y)) s x