Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case refine_1.hf.hf.hf
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => ↑(extChartAt I c) z) c

case refine_1.hf.hf.hy
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c) c = ↑(extChartAt I c) c

case refine_1.hf.hy
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
exact continuousAt_extChartAt I _
Proof state after:
case refine_1.hf.hf.hy
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c) c = ↑(extChartAt I c) c

case refine_1.hf.hy
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
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
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c