internlm/Lean-Github huggingface dataset:
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case neg
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
set a := leadingCoeff f 0
Proof state after:
case neg
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case neg
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have a0 : a ≠ 0 := leadingCoeff_ne_zero fa o0
Proof state after:
case neg
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, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case neg
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, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
set g := fun z ↦ a⁻¹ • f z
Proof state after:
case neg
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case neg
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have s : SuperAt g (orderAt f 0) :=
  { d2
    fa0 := analyticAt_const.mul fa
    fd := by rw [orderAt_const_smul (inv_ne_zero a0)]
    fc := by rw [leadingCoeff_const_smul]; simp only [smul_eq_mul, inv_mul_cancel a0] }
Proof state after:
case neg
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
s : SuperAt g (orderAt f 0)
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case neg
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
s : SuperAt g (orderAt f 0)
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases s.not_local_inj with ⟨h, ha, h0, e⟩
Proof state after:
case neg.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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0 : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case neg.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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0 : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
use h, ha, h0
Proof state after:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0 : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ f (h z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0 : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ f (h z) = f z
Tactic:
refine e.mp (eventually_of_forall ?_)
Proof state after:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0 : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
⊢ ∀ (x : ℂ), h x ≠ x ∧ g (h x) = g x → h x ≠ x ∧ f (h x) = f x
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0 : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
⊢ ∀ (x : ℂ), h x ≠ x ∧ g (h x) = g x → h x ≠ x ∧ f (h x) = f x
Tactic:
intro z ⟨h0, hz⟩
Proof state after:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0✝ : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
z : ℂ
h0 : h z ≠ z
hz : g (h z) = g z
⊢ h z ≠ z ∧ f (h z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0✝ : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
z : ℂ
h0 : h z ≠ z
hz : g (h z) = g z
⊢ h z ≠ z ∧ f (h z) = f z
Tactic:
use h0
Proof state after:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0✝ : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
z : ℂ
h0 : h z ≠ z
hz : g (h z) = g z
⊢ f (h z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
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
s : SuperAt g (orderAt f 0)
h : ℂ → ℂ
ha : AnalyticAt ℂ h 0
h0✝ : h 0 = 0
e : ∀ᶠ (z : ℂ) in 𝓝[≠] 0, h z ≠ z ∧ g (h z) = g z
z : ℂ
h0 : h z ≠ z
hz : g (h z) = g z
⊢ f (h z) = f z
Tactic:
exact (IsUnit.smul_left_cancel (Ne.isUnit (inv_ne_zero a0))).mp hz
Proof state after:
no goals
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case pos
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : orderAt f 0 = 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
simp only [orderAt_eq_zero_iff fa, f0, Ne, eq_self_iff_true, not_true, or_false_iff] at o0
Proof state after:
case pos
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case pos
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
use fun z ↦ -z, (analyticAt_id _ _).neg, neg_zero
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, -z ≠ z ∧ f (-z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, -z ≠ z ∧ f (-z) = f z
Tactic:
rw [eventually_nhdsWithin_iff]
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → -x ≠ x ∧ f (-x) = f x
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → -x ≠ x ∧ f (-x) = f x
Tactic:
have e0 : ∀ᶠ z in 𝓝 0, f (-z) = 0 := by
  nth_rw 1 [← neg_zero] at o0; exact continuousAt_neg.eventually o0
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → -x ≠ x ∧ f (-x) = f x
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → -x ≠ x ∧ f (-x) = f x
Tactic:
refine o0.mp (e0.mp (eventually_of_forall fun z f0' f0 z0 ↦ ?_))
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0 z
z0 : z ∈ {0}ᶜ
⊢ -z ≠ z ∧ f (-z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0 z
z0 : z ∈ {0}ᶜ
⊢ -z ≠ z ∧ f (-z) = f z
Tactic:
simp only [mem_compl_singleton_iff] at z0
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0 z
z0 : z ≠ 0
⊢ -z ≠ z ∧ f (-z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0 z
z0 : z ≠ 0
⊢ -z ≠ z ∧ f (-z) = f z
Tactic:
rw [Pi.zero_apply] at f0
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0
z0 : z ≠ 0
⊢ -z ≠ z ∧ f (-z) = f z
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0
z0 : z ≠ 0
⊢ -z ≠ z ∧ f (-z) = f z
Tactic:
rw [f0, f0', eq_self_iff_true, and_true_iff, Ne, neg_eq_self_iff]
Proof state after:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0
z0 : z ≠ 0
⊢ ¬z = 0
Theorem: not_local_inj_of_deriv_zero'
Proof state before:
case 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0✝ : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
e0 : ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
z : ℂ
f0' : f (-z) = 0
f0 : f z = 0
z0 : z ≠ 0
⊢ ¬z = 0
Tactic:
exact z0
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 0).EventuallyEq f 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
Tactic:
nth_rw 1 [← neg_zero] at o0
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 (-0)).EventuallyEq f 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : (𝓝 (-0)).EventuallyEq f 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 0, f (-z) = 0
Tactic:
exact continuousAt_neg.eventually o0
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
⊢ orderAt f 0 ≠ 1
Tactic:
have d := df.deriv
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
d : deriv f 0 = 0
⊢ orderAt f 0 ≠ 1
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
d : deriv f 0 = 0
⊢ orderAt f 0 ≠ 1
Tactic:
contrapose d
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
d : ¬orderAt f 0 ≠ 1
⊢ ¬deriv f 0 = 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
d : ¬orderAt f 0 ≠ 1
⊢ ¬deriv f 0 = 0
Tactic:
simp only [not_not] at d
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
d : orderAt f 0 = 1
⊢ ¬deriv f 0 = 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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
d : orderAt f 0 = 1
⊢ ¬deriv f 0 = 0
Tactic:
exact deriv_ne_zero_of_orderAt_eq_one d
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
⊢ 2 ≤ orderAt f 0
Tactic:
rw [Nat.two_le_iff]
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 : ℂ → ℂ
fa : AnalyticAt ℂ f 0
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
⊢ orderAt f 0 ≠ 0 ∧ orderAt f 0 ≠ 1
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
⊢ orderAt f 0 ≠ 0 ∧ orderAt f 0 ≠ 1
Tactic:
use o0, o1
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 : ℂ → ℂ
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
⊢ orderAt g 0 = orderAt f 0
Tactic:
rw [orderAt_const_smul (inv_ne_zero 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 : ℂ → ℂ
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
⊢ leadingCoeff g 0 = 1
Tactic:
rw [leadingCoeff_const_smul]
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 : ℂ → ℂ
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