internlm/Lean-Github huggingface dataset:
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
o0 : ¬orderAt f 0 = 0
d2 : 2 ≤ orderAt f 0
a : ℂ := leadingCoeff f 0
a0 : a ≠ 0
g : ℂ → ℂ := fun z => a⁻¹ • f z
⊢ a⁻¹ • leadingCoeff (fun z => f z) 0 = 1
Tactic:
simp only [smul_eq_mul, inv_mul_cancel a0]
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
set f' := fun z ↦ f (z + c) - f 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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have fa' : AnalyticAt ℂ f' 0 :=
  AnalyticAt.sub
    (AnalyticAt.comp (by simp only [zero_add, fa]) ((analyticAt_id _ _).add analyticAt_const))
    analyticAt_const
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have df' : HasDerivAt f' (0 * 1) 0 := by
  refine HasDerivAt.sub_const ?_ _
  have e : (fun z ↦ f (z + c)) = f ∘ fun z ↦ z + c := rfl
  rw [e]; apply HasDerivAt.comp; simp only [zero_add, df]
  exact HasDerivAt.add_const (hasDerivAt_id _) _
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' (0 * 1) 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' (0 * 1) 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
simp only [MulZeroClass.zero_mul] at df'
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have f0' : (fun z ↦ f (z + c) - f c) 0 = 0 := by simp only [zero_add, sub_self]
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases not_local_inj_of_deriv_zero' fa' df' f0' with ⟨g, ga, e, h⟩
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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
c : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
f0' : (fun z => f (z + c) - f c) 0 = 0
g : ℂ → ℂ
ga : AnalyticAt ℂ g 0
e : g 0 = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
clear fa df fa' df'
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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∃ g, AnalyticAt ℂ g c ∧ g c = c ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
refine ⟨fun z ↦ g (z - c) + c, ?_, ?_, ?_⟩
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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ AnalyticAt ℂ (fun z => g (z - c) + c) 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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ (fun z => g (z - c) + c) 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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] c, (fun z => g (z - c) + c) z ≠ z ∧ f ((fun z => g (z - c) + c) z) = f z
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
⊢ AnalyticAt ℂ f (0 + c)
Tactic:
simp only [zero_add, fa]
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ HasDerivAt f' (0 * 1) 0
Tactic:
refine HasDerivAt.sub_const ?_ _
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0
Tactic:
have e : (fun z ↦ f (z + c)) = f ∘ fun z ↦ z + c := rfl
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => f (z + c)) (0 * 1) 0
Tactic:
rw [e]
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (f ∘ fun z => z + c) (0 * 1) 0
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (f ∘ fun z => z + c) (0 * 1) 0
Tactic:
apply HasDerivAt.comp
Proof state after:
case hh₂
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt f 0 (0 + c)

case hh
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0
Theorem: not_local_inj_of_deriv_zero
Proof state before:
case hh₂
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt f 0 (0 + c)

case hh
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0
Tactic:
simp only [zero_add, df]
Proof state after:
case hh
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0
Theorem: not_local_inj_of_deriv_zero
Proof state before:
case hh
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
e : (fun z => f (z + c)) = f ∘ fun z => z + c
⊢ HasDerivAt (fun z => z + c) 1 0
Tactic:
exact HasDerivAt.add_const (hasDerivAt_id _) _
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 : ℂ
fa : AnalyticAt ℂ f c
df : HasDerivAt f 0 c
f' : ℂ → ℂ := fun z => f (z + c) - f c
fa' : AnalyticAt ℂ f' 0
df' : HasDerivAt f' 0 0
⊢ (fun z => f (z + c) - f c) 0 = 0
Tactic:
simp only [zero_add, sub_self]
Proof state after:
no goals
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ AnalyticAt ℂ (fun z => g (z - c) + c) c
Tactic:
exact AnalyticAt.add (AnalyticAt.comp (by simp only [sub_self, ga])
  ((analyticAt_id _ _).sub analyticAt_const)) analyticAt_const
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ AnalyticAt ℂ g (c - c)
Tactic:
simp only [sub_self, ga]
Proof state after:
no goals
Theorem: not_local_inj_of_deriv_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 : ℂ → ℂ
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ (fun z => g (z - c) + c) c = c
Tactic:
simp only [sub_self, e, zero_add]
Proof state after:
no goals
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 : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f' (g z) = f' z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] c, (fun z => g (z - c) + c) z ≠ z ∧ f ((fun z => g (z - c) + c) z) = f z
Tactic:
simp only [eventually_nhdsWithin_iff] at h ⊢
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 : ℂ → ℂ
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
have sc : Tendsto (fun z ↦ z - c) (𝓝 c) (𝓝 0) := by
  rw [← sub_self c]; exact continuousAt_id.sub continuousAt_const
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 : ℂ → ℂ
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)
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
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)
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
refine (sc.eventually h).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 : ℂ → ℂ
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)
⊢ ∀ (x : ℂ),
    (x - c ∈ {0}ᶜ → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) →
      x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
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)
⊢ ∀ (x : ℂ),
    (x - c ∈ {0}ᶜ → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) →
      x ∈ {c}ᶜ → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
simp only [mem_compl_singleton_iff, sub_ne_zero]
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 : ℂ → ℂ
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)
⊢ ∀ (x : ℂ),
    (x ≠ c → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) → x ≠ c → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
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)
⊢ ∀ (x : ℂ),
    (x ≠ c → g (x - c) ≠ x - c ∧ f' (g (x - c)) = f' (x - c)) → x ≠ c → g (x - c) + c ≠ x ∧ f (g (x - c) + c) = f x
Tactic:
intro z h 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 : ℂ → ℂ
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