internlm/Lean-Github huggingface dataset:
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro.intro.intro.refine_3.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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
⊢ i (a * bottcherNear f d z) = i (bottcherNear f d z) ∧ ¬a * bottcherNear f d z = bottcherNear f d z
Tactic:
rw [ib]
Proof state after:
case intro.intro.intro.intro.intro.intro.refine_3.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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
⊢ i (a * bottcherNear f d z) = z ∧ ¬a * bottcherNear f d z = bottcherNear f d z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro.intro.intro.refine_3.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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
⊢ i (a * bottcherNear f d z) = z ∧ ¬a * bottcherNear f d z = bottcherNear f d z
Tactic:
use tp
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
⊢ ¬a * bottcherNear f d z = bottcherNear f d z
Theorem: SuperAt.not_local_inj
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
⊢ ¬a * bottcherNear f d z = bottcherNear f d z
Tactic:
contrapose a1
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : ¬¬a * bottcherNear f d z = bottcherNear f d z
⊢ ¬a ≠ 1
Theorem: SuperAt.not_local_inj
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : ¬¬a * bottcherNear f d z = bottcherNear f d z
⊢ ¬a ≠ 1
Tactic:
simp only [not_not] at a1 ⊢
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : a * bottcherNear f d z = bottcherNear f d z
⊢ a = 1
Theorem: SuperAt.not_local_inj
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : a * bottcherNear f d z = bottcherNear f d z
⊢ a = 1
Tactic:
have b0 := bottcherNear_ne_zero s m1 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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : a * bottcherNear f d z = bottcherNear f d z
b0 : bottcherNear f d z ≠ 0
⊢ a = 1
Theorem: SuperAt.not_local_inj
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : a * bottcherNear f d z = bottcherNear f d z
b0 : bottcherNear f d z ≠ 0
⊢ a = 1
Tactic:
calc a
  _ = a * bottcherNear f d z / bottcherNear f d z := by field_simp [b0]
  _ = bottcherNear f d z / bottcherNear f d z := by rw [a1]
  _ = 1 := div_self b0
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : a * bottcherNear f d z = bottcherNear f d z
b0 : bottcherNear f d z ≠ 0
⊢ a = a * bottcherNear f d z / bottcherNear f d z
Tactic:
field_simp [b0]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
z0 : z ≠ 0
tp : i (a * bottcherNear f d z) = z
a1 : a * bottcherNear f d z = bottcherNear f d z
b0 : bottcherNear f d z ≠ 0
⊢ a * bottcherNear f d z / bottcherNear f d z = bottcherNear f d z / bottcherNear f d z
Tactic:
rw [a1]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro.intro.intro.refine_3.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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib✝ : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
i0 : i 0 = 0
inj : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
a : ℂ
a1 : a ≠ 1
ad : a ^ d = 1
m0✝ : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1✝ : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
t0✝ : Tendsto (fun z => a * bottcherNear f d z) (𝓝 0) (𝓝 0)
t1✝ : Tendsto (fun z => f (i (a * bottcherNear f d z))) (𝓝 0) (𝓝 0)
t2✝ : Tendsto f (𝓝 0) (𝓝 0)
tp✝ : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
z : ℂ
m1 : z ∈ t
m0 : i (a * bottcherNear f d z) ∈ t
t2 : i (bottcherNear f d (f z)) = f z
t0 : bottcherNear f d (i (a * bottcherNear f d z)) = a * bottcherNear f d z
t1 : i (bottcherNear f d (f (i (a * bottcherNear f d z)))) = f (i (a * bottcherNear f d z))
x✝ : bottcherNear f d (i z) = z
ib : i (bottcherNear f d z) = z
tp :
  i (a * bottcherNear f d z, bottcherNear f d z).1 = i (a * bottcherNear f d z, bottcherNear f d z).2 →
    (a * bottcherNear f d z, bottcherNear f d z).1 = (a * bottcherNear f d z, bottcherNear f d z).2
z0 : z ≠ 0
⊢ f (i (a * bottcherNear f d z)) = f z
Tactic:
rw [← t1, bottcherNear_eqn s m0, t0, mul_pow, ad, one_mul, ← bottcherNear_eqn s m1, t2]
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
by_cases o0 : orderAt f 0 = 0
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 : orderAt f 0 = 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

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
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
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
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:
have o1 : orderAt f 0 ≠ 1 := by
  have d := df.deriv; contrapose d; simp only [not_not] at d
  exact deriv_ne_zero_of_orderAt_eq_one d
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
⊢ ∃ 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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have d2 : 2 ≤ orderAt f 0 := by rw [Nat.two_le_iff]; use o0, o1
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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
d2 : 2 ≤ 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
df : HasDerivAt f 0 0
f0 : f 0 = 0
o0 : ¬orderAt f 0 = 0
o1 : orderAt f 0 ≠ 1
d2 : 2 ≤ orderAt f 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
clear o1 df f0
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z