internlm/Lean-Github huggingface dataset:
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z
Tactic:
rcases h zc with ⟨gz, ff⟩
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_zero
Proof state before:
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z ∧ f (g (z - c) + c) = f z
Tactic:
constructor
Proof state after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ g (z - c) + c ≠ z

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
contrapose gz
Proof state after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : ¬g (z - c) + c ≠ z
⊢ ¬g (z - c) ≠ z - c

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : ¬g (z - c) + c ≠ z
⊢ ¬g (z - c) ≠ z - c

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
simp only [not_not] at gz ⊢
Proof state after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = z - c

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = z - c

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
nth_rw 2 [← gz]
Proof state after:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = g (z - c) + c - c

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.left
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
ff : f' (g (z - c)) = f' (z - c)
gz : g (z - c) + c = z
⊢ g (z - c) = g (z - c) + c - c

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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
ring
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f' (g (z - c)) = f' (z - c)
⊢ f (g (z - c) + c) = f z
Tactic:
simp only [sub_left_inj, sub_add_cancel, f'] at ff
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f (g (z - c) + c) = f z
⊢ f (g (z - c) + c) = f z
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h✝ : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
sc : Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
z : ℂ
h : z ≠ c → g (z - c) ≠ z - c ∧ f' (g (z - c)) = f' (z - c)
zc : z ≠ c
gz : g (z - c) ≠ z - c
ff : f (g (z - c) + c) = f z
⊢ f (g (z - c) + c) = f z
Tactic:
exact ff
Proof state after:
no goals
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ Tendsto (fun z => z - c) (𝓝 c) (𝓝 0)
Tactic:
rw [← sub_self c]
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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ Tendsto (fun z => z - c) (𝓝 c) (𝓝 (c - c))
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
c : ℂ
f' : ℂ → ℂ := fun z => f (z + c) - f c
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → g x ≠ x ∧ f' (g x) = f' x
⊢ Tendsto (fun z => z - c) (𝓝 c) (𝓝 (c - c))
Tactic:
exact continuousAt_id.sub continuousAt_const
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, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
generalize hg : (fun z ↦ extChartAt I (f c) (f ((extChartAt I c).symm z))) = g
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
⊢ ∃ 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
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
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have dg : mfderiv I I g (extChartAt I c c) = 0 := by
  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
  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]
  apply mem_extChartAt_source; apply mem_extChartAt_target; rw [PartialEquiv.left_inv]
  apply mem_extChartAt_source; apply mem_extChartAt_source
  exact MDifferentiableAt.comp _ fd
    (HolomorphicAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt
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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
⊢ ∃ 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
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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
simp only [holomorphicAt_iff, Function.comp, hg] at fa
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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(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:
have dg' := fa.2.differentiableAt.mdifferentiableAt.hasMFDerivAt
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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasMFDerivAt I I g (↑(extChartAt I c) c) (mfderiv I I g (↑(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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasMFDerivAt I I g (↑(extChartAt I c) c) (mfderiv I I g (↑(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:
rw [dg, hasMFDerivAt_iff_hasFDerivAt] at 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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasFDerivAt g 0 (↑(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
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasFDerivAt g 0 (↑(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:
replace dg := dg'.hasDerivAt
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' : 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