internlm/Lean-Github huggingface dataset:
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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' : HasFDerivAt g 0 (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
clear dg'
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
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)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases not_local_inj_of_deriv_zero fa.2 dg with ⟨h, ha, h0, e⟩
Proof state after:
case intro.intro.intro
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
refine ⟨fun z ↦ (extChartAt I c).symm (h (extChartAt I c z)), ?_, ?_, ?_⟩
Proof state after:
case intro.intro.intro.refine_1
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c

case intro.intro.intro.refine_2
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c = c

case intro.intro.intro.refine_3
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∀ᶠ (z : S) in 𝓝[≠] c,
    (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) z ≠ z ∧
      f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) z) = f z
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
⊢ mfderiv I I g (↑(extChartAt I c) c) = 0
Tactic:
have fd : MDifferentiableAt I I f ((extChartAt I c).symm (extChartAt I c c)) := by
  rw [PartialEquiv.left_inv]; exact fa.mdifferentiableAt; 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))
⊢ mfderiv I I g (↑(extChartAt I c) c) = 0
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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))
⊢ mfderiv I I g (↑(extChartAt I c) c) = 0
Tactic:
rw [← hg, ←Function.comp_def, mfderiv_comp _ (HolomorphicAt.extChartAt _).mdifferentiableAt _,
  ←Function.comp_def, mfderiv_comp _ fd (HolomorphicAt.extChartAt_symm _).mdifferentiableAt,
  PartialEquiv.left_inv, df, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero]
Proof state after:
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)
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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_target
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))
⊢ 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)
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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:
rw [PartialEquiv.left_inv]
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))
⊢ f c ∈ (extChartAt I (f c)).source

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))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 c ∈ (extChartAt I (f c)).source

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))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
apply mem_extChartAt_source
Proof state after:
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))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
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))
⊢ 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))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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:
exact MDifferentiableAt.comp _ fd
  (HolomorphicAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt
Proof state after:
no goals
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
⊢ MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
Tactic:
rw [PartialEquiv.left_inv]
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
⊢ MDifferentiableAt I I f c

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
⊢ c ∈ (extChartAt I c).source
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
⊢ MDifferentiableAt I I f c

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
⊢ c ∈ (extChartAt I c).source
Tactic:
exact fa.mdifferentiableAt
Proof state after:
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
⊢ c ∈ (extChartAt I c).source
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
⊢ c ∈ (extChartAt I c).source
Tactic:
apply mem_extChartAt_source
Proof state after:
no goals
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro.refine_1
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c
Tactic:
apply (HolomorphicAt.extChartAt_symm (mem_extChartAt_target I c)).comp_of_eq
Proof state after:
case intro.intro.intro.refine_1.gh
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun x => h (↑(extChartAt I c) x)) c

case intro.intro.intro.refine_1.e
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c