[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
set e := extChartAt I c
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
have hI : range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
have H₁ : 𝓝[range I] (e c) = 𝓝 (e c) := by rw [hI, nhdsWithin_univ]
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
⊢ 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
[PROOFSTEP]
rw [hI, nhdsWithin_univ]
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
have H₂ : map e.symm (𝓝 (e c)) = 𝓝 c
[GOAL]
case H₂
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
⊢ map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
[PROOFSTEP]
rw [← map_extChartAt_symm_nhdsWithin_range I c, H₁]
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
[PROOFSTEP]
rw [← H₂, eventually_map]
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
⊢ ∀ᶠ (a : E) in 𝓝 (↑e c), ‖f (↑(LocalEquiv.symm e) a)‖ = ‖f c‖
[PROOFSTEP]
replace hd : ∀ᶠ y in 𝓝 (e c), DifferentiableAt ℂ (f ∘ e.symm) y
[GOAL]
case hd
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
⊢ ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm e)) y
[PROOFSTEP]
have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin I c
[GOAL]
case hd
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
⊢ ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm e)) y
[PROOFSTEP]
filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
[GOAL]
case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ (extChartAt I c).target
hy₂ : MDifferentiableAt I 𝓘(ℂ, F) f (↑(LocalEquiv.symm (extChartAt I c)) y)
⊢ DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm (extChartAt I c))) y
[PROOFSTEP]
have hys : e.symm y ∈ (chartAt H c).source
[GOAL]
case hys
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ (extChartAt I c).target
hy₂ : MDifferentiableAt I 𝓘(ℂ, F) f (↑(LocalEquiv.symm (extChartAt I c)) y)
⊢ ↑(LocalEquiv.symm e) y ∈ (chartAt H c).toLocalEquiv.source
[PROOFSTEP]
rw [← extChartAt_source I c]
[GOAL]
case hys
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ (extChartAt I c).target
hy₂ : MDifferentiableAt I 𝓘(ℂ, F) f (↑(LocalEquiv.symm (extChartAt I c)) y)
⊢ ↑(LocalEquiv.symm e) y ∈ (extChartAt I c).source
[PROOFSTEP]
exact (extChartAt I c).map_target hyt
[GOAL]
case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ (extChartAt I c).target
hy₂ : MDifferentiableAt I 𝓘(ℂ, F) f (↑(LocalEquiv.symm (extChartAt I c)) y)
hys : ↑(LocalEquiv.symm e) y ∈ (chartAt H c).toLocalEquiv.source
⊢ DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm (extChartAt I c))) y
[PROOFSTEP]
have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
[GOAL]
case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ (extChartAt I c).target
hy₂ : MDifferentiableAt I 𝓘(ℂ, F) f (↑(LocalEquiv.symm (extChartAt I c)) y)
hys : ↑(LocalEquiv.symm e) y ∈ (chartAt H c).toLocalEquiv.source
hfy : f (↑(LocalEquiv.symm e) y) ∈ (chartAt F 0).toLocalEquiv.source
⊢ DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm (extChartAt I c))) y
[PROOFSTEP]
rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ, e.right_inv hyt] at hy₂ 
[GOAL]
case h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ (extChartAt I c).target
hy₂ :
  ContinuousAt f (↑(LocalEquiv.symm e) y) ∧
    DifferentiableAt ℂ (↑(extChartAt 𝓘(ℂ, F) 0) ∘ f ∘ ↑(LocalEquiv.symm (extChartAt I c))) y
hys : ↑(LocalEquiv.symm e) y ∈ (chartAt H c).toLocalEquiv.source
hfy : f (↑(LocalEquiv.symm e) y) ∈ (chartAt F 0).toLocalEquiv.source
⊢ DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm (extChartAt I c))) y
[PROOFSTEP]
exact hy₂.2
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm e)) y
⊢ ∀ᶠ (a : E) in 𝓝 (↑e c), ‖f (↑(LocalEquiv.symm e) a)‖ = ‖f c‖
[PROOFSTEP]
convert norm_eventually_eq_of_isLocalMax hd _
[GOAL]
case h.e'_2.h.h.e'_3.h.e'_3
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm e)) y
x✝ : E
⊢ f c = (f ∘ ↑(LocalEquiv.symm e)) (↑e c)
[PROOFSTEP]
exact congr_arg f (extChartAt_to_inv _ _).symm
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : LocalEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑(LocalEquiv.symm e)) (𝓝 (↑e c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑(LocalEquiv.symm e)) y
⊢ IsLocalMax (norm ∘ f ∘ ↑(LocalEquiv.symm e)) (↑e c)
[PROOFSTEP]
simpa only [IsLocalMax, IsMaxFilter, ← H₂, (· ∘ ·), extChartAt_to_inv] using hc
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
⊢ EqOn (norm ∘ f) (const M ‖f c‖) U
[PROOFSTEP]
set V := {z ∈ U | ‖f z‖ = ‖f c‖}
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ EqOn (norm ∘ f) (const M ‖f c‖) U
[PROOFSTEP]
suffices : U ⊆ V
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
this : U ⊆ V
⊢ EqOn (norm ∘ f) (const M ‖f c‖) U
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ U ⊆ V
[PROOFSTEP]
exact fun x hx => (this hx).2
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ U ⊆ V
[PROOFSTEP]
have hVo : IsOpen V
[GOAL]
case hVo
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
⊢ IsOpen V
[PROOFSTEP]
refine isOpen_iff_mem_nhds.2 fun x hx ↦ inter_mem (ho.mem_nhds hx.1) ?_
[GOAL]
case hVo
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
x : M
hx : x ∈ V
⊢ (fun z => ‖f z‖ = ‖f c‖) ∈ 𝓝 x
[PROOFSTEP]
replace hm : IsLocalMax (‖f ·‖) x := mem_of_superset (ho.mem_nhds hx.1) fun z hz ↦ (hm hz).out.trans_eq hx.2.symm
[GOAL]
case hVo
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
x : M
hx : x ∈ V
hm : IsLocalMax (fun x => ‖f x‖) x
⊢ (fun z => ‖f z‖ = ‖f c‖) ∈ 𝓝 x
[PROOFSTEP]
replace hd : ∀ᶠ y in 𝓝 x, MDifferentiableAt I 𝓘(ℂ, F) f y :=
  (eventually_mem_nhds.2 (ho.mem_nhds hx.1)).mono fun z ↦ hd.mdifferentiableAt
[GOAL]
case hVo
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
x : M
hx : x ∈ V
hm : IsLocalMax (fun x => ‖f x‖) x
hd : ∀ᶠ (y : M) in 𝓝 x, MDifferentiableAt I 𝓘(ℂ, F) f y
⊢ (fun z => ‖f z‖ = ‖f c‖) ∈ 𝓝 x
[PROOFSTEP]
exact (Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax hd hm).mono fun _ ↦ (Eq.trans · hx.2)
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen V
⊢ U ⊆ V
[PROOFSTEP]
have hVne : (U ∩ V).Nonempty := ⟨c, hcU, hcU, rfl⟩
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
⊢ U ⊆ V
[PROOFSTEP]
set W := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
⊢ U ⊆ V
[PROOFSTEP]
have hWo : IsOpen W := hd.continuousOn.norm.preimage_open_of_open ho isOpen_ne
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen W
⊢ U ⊆ V
[PROOFSTEP]
have hdVW : Disjoint V W := disjoint_compl_right.mono inf_le_right inf_le_right
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen W
hdVW : Disjoint V W
⊢ U ⊆ V
[PROOFSTEP]
have hUVW : U ⊆ V ∪ W := fun x hx => (eq_or_ne ‖f x‖ ‖f c‖).imp (.intro hx) (.intro hx)
[GOAL]
case this
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen V
hVne : Set.Nonempty (U ∩ V)
W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen W
hdVW : Disjoint V W
hUVW : U ⊆ V ∪ W
⊢ U ⊆ V
[PROOFSTEP]
exact hc.subset_left_of_subset_union hVo hWo hdVW hUVW hVne
[GOAL]
E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℂ E
F : Type u_2
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℂ F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁵ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : StrictConvexSpace ℝ F
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
x : M
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
hd' : MDifferentiableOn I 𝓘(ℂ, F) (fun x => f x + f c) U
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + const M (f c) x‖ = ‖f x‖ + ‖const M (f c) x‖
[PROOFSTEP]
simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
a b : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
⊢ f a = f b
[PROOFSTEP]
refine
  ?_
    -- Subtract `f b` to avoid the assumption `[StrictConvexSpace ℝ F]`
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
a b : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
⊢ f a = f b
[PROOFSTEP]
wlog hb₀ : f b = 0 generalizing f
[GOAL]
case inr
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
a b : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
this : ∀ {f : M → F}, MDifferentiableOn I 𝓘(ℂ, F) f U → f b = 0 → f a = f b
hb₀ : ¬f b = 0
⊢ f a = f b
[PROOFSTEP]
have hd' : MDifferentiableOn I 𝓘(ℂ, F) (f · - f b) U := fun x hx ↦
  ⟨(hd x hx).1.sub continuousWithinAt_const, (hd x hx).2.sub_const _⟩
[GOAL]
case inr
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
f : M → F
U : Set M
a b : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
this : ∀ {f : M → F}, MDifferentiableOn I 𝓘(ℂ, F) f U → f b = 0 → f a = f b
hb₀ : ¬f b = 0
hd' : MDifferentiableOn I 𝓘(ℂ, F) (fun x => f x - f b) U
⊢ f a = f b
[PROOFSTEP]
simpa [sub_eq_zero] using this hd' (sub_self _)
[GOAL]
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
U : Set M
a b : M
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hb₀ : f b = 0
⊢ f a = f b
[PROOFSTEP]
rcases hc.exists_isMaxOn ⟨a, ha⟩ hd.continuousOn.norm with ⟨c, hcU, hc⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
U : Set M
a b : M
hpc : IsPreconnected U
hc✝ : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (fun x => ‖f x‖) U c
⊢ f a = f b
[PROOFSTEP]
have : ∀ x ∈ U, ‖f x‖ = ‖f c‖ := norm_eqOn_of_isPreconnected_of_isMaxOn hd hpc ho hcU hc
[GOAL]
case intro.intro
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : ModelWithCorners.Boundaryless I
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : CompactSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
U : Set M
a b : M
hpc : IsPreconnected U
hc✝ : IsCompact U
ho : IsOpen U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (fun x => ‖f x‖) U c
this : ∀ (x : M), x ∈ U → ‖f x‖ = ‖f c‖
⊢ f a = f b
[PROOFSTEP]
rw [hb₀, ← norm_eq_zero, this a ha, ← this b hb, hb₀, norm_zero]
