internlm/Lean-Github huggingface dataset:
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
d0 : ¬mfderiv I I i 0 = 0
⊢ mfderiv I I i 0 ≠ 0

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
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
Tactic:
exact d0
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 : ℂ → ℂ
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
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
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
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i (bottcherNear f d 0)
Tactic:
rw [bottcherNear_zero]
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 : ℂ → ℂ
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
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i 0
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
d0 : mfderiv I I (i ∘ fun x => bottcherNear f d x) 0 ≠ 0
⊢ MDifferentiableAt I I i 0
Tactic:
exact ia.mdifferentiableAt
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ AnalyticAt ℂ (fun z => i (a * bottcherNear f d z)) 0
Tactic:
apply HolomorphicAt.analyticAt I I
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ HolomorphicAt I I (fun z => i (a * bottcherNear f d z)) 0
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ HolomorphicAt I I (fun z => i (a * bottcherNear f d z)) 0
Tactic:
refine ia.comp_of_eq (holomorphicAt_const.mul (ba.holomorphicAt I I)) ?_
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ a * bottcherNear f d 0 = 0
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ a * bottcherNear f d 0 = 0
Tactic:
simp only [bottcherNear_zero, s.f0, MulZeroClass.mul_zero]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ (fun z => i (a * bottcherNear f d z)) 0 = 0
Tactic:
simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, (fun z => i (a * bottcherNear f d z)) z ≠ z ∧ f ((fun z => i (a * bottcherNear f d z)) z) = f z
Tactic:
simp only [eventually_nhdsWithin_iff, mem_compl_singleton_iff]
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
have t0 : ContinuousAt (fun z ↦ a * bottcherNear f d z) 0 :=
  continuousAt_const.mul ba.continuousAt
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
have t1 : ContinuousAt (fun z ↦ f (i (a * bottcherNear f d z))) 0 := by
  refine s.fa0.continuousAt.comp_of_eq (ia.continuousAt.comp_of_eq t0 ?_) ?_
  repeat' simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0]
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
have t2 : ContinuousAt f 0 := s.fa0.continuousAt
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
t2 : ContinuousAt f 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
t2 : ContinuousAt f 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
have m0 : ∀ᶠ z in 𝓝 0, i (a * bottcherNear f d z) ∈ t := by
  refine (ia.continuousAt.comp_of_eq t0 ?_).eventually_mem (s.o.mem_nhds ?_)
  repeat' simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0, s.t0, Function.comp]
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
t2 : ContinuousAt f 0
m0 : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
t2 : ContinuousAt f 0
m0 : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
have m1 : ∀ᶠ z in 𝓝 0, z ∈ t := s.o.eventually_mem s.t0
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
t2 : ContinuousAt f 0
m0 : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1 : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
t1 : ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
t2 : ContinuousAt f 0
m0 : ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
m1 : ∀ᶠ (z : ℂ) in 𝓝 0, z ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
simp only [ContinuousAt, bottcherNear_zero, MulZeroClass.mul_zero, i0, s.f0] at t0 t1 t2
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.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 : ℂ → ℂ
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)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
have tp := t0.prod_mk ba.continuousAt
Proof state after:
case intro.intro.intro.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 : ℂ → ℂ
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 ×ˢ 𝓝 (bottcherNear f d 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x