Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
apply mem_extChartAt_source
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)