Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.right
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
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh :
  ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) =
    ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (↑(extChartAt I c) z)))
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
rw [PartialEquiv.left_inv _ m0] at gh
Proof state after:
case intro.intro.intro.refine_3.intro.right
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
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) = ↑(extChartAt I (f c)) (f z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z