internlm/Lean-Github huggingface dataset:
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
Tactic:
apply (ha.holomorphicAt I I).comp_of_eq
  (HolomorphicAt.extChartAt (mem_extChartAt_source I c)) rfl
Proof state after:
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
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
Tactic:
exact h0
Proof state after:
no goals
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
Tactic:
simp only [h0, PartialEquiv.left_inv _ (mem_extChartAt_source I c)]
Proof state after:
no goals
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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
Tactic:
rw [eventually_nhdsWithin_iff] at e ⊢
Proof state after:
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 : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ {c}ᶜ →
      (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
        f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ {c}ᶜ →
      (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
        f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
apply ((continuousAt_extChartAt I c).eventually e).mp
Proof state after:
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 : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
        h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
      x ∈ {c}ᶜ →
        (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
          f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
        h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
      x ∈ {c}ᶜ →
        (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
          f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
apply ((isOpen_extChartAt_source I c).eventually_mem (mem_extChartAt_source I c)).mp
Proof state after:
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 : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (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
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
have m2 : ∀ᶠ z in 𝓝 c, f z ∈ (extChartAt I (f c)).source :=
  fa.1.eventually_mem (extChartAt_source_mem_nhds I _)
Proof state after:
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 : ∀ᶠ (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
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (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
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
refine m1.mp (m2.mp (m3.mp (eventually_of_forall ?_)))
Proof state after:
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 : ∀ᶠ (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
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ∈ {c}ᶜ →
                (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
                  f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (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
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ∈ {c}ᶜ →
                (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
                  f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
simp only [mem_compl_singleton_iff]
Proof state after:
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 : ∀ᶠ (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
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ≠ ↑(extChartAt I c) c →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ≠ c →
                ↑(extChartAt I c).symm (h (↑(extChartAt I c) x)) ≠ x ∧
                  f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) = f x
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (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
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ≠ ↑(extChartAt I c) c →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ≠ c →
                ↑(extChartAt I c).symm (h (↑(extChartAt I c) x)) ≠ x ∧
                  f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) = f x
Tactic:
intro z m3 m2 m1 m0 even zc
Proof state after:
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 : ∀ᶠ (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
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
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 : ∀ᶠ (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
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
rcases even ((PartialEquiv.injOn _).ne m0 (mem_extChartAt_source I c) zc) with ⟨hz, gh⟩
Proof state after:
case intro.intro.intro.refine_3.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 : ∀ᶠ (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 : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z