internlm/Lean-Github huggingface dataset:
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)
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
Tactic:
simp only [← nhds_prod_eq, ContinuousAt, bottcherNear_zero] at tp
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, 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)
tp : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
apply (tp.eventually inj).mp
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, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    (i (a * bottcherNear f d x, bottcherNear f d x).1 = i (a * bottcherNear f d x, bottcherNear f d x).2 →
        (a * bottcherNear f d x, bottcherNear f d x).1 = (a * bottcherNear f d x, bottcherNear f d x).2) →
      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)
tp : Tendsto (fun x => (a * bottcherNear f d x, bottcherNear f d x)) (𝓝 0) (𝓝 (0, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    (i (a * bottcherNear f d x, bottcherNear f d x).1 = i (a * bottcherNear f d x, bottcherNear f d x).2 →
        (a * bottcherNear f d x, bottcherNear f d x).1 = (a * bottcherNear f d x, bottcherNear f d x).2) →
      x ≠ 0 → i (a * bottcherNear f d x) ≠ x ∧ f (i (a * bottcherNear f d x)) = f x
Tactic:
refine ib.mp (bi.mp ((t1.eventually ib).mp
  ((t0.eventually bi).mp ((t2.eventually ib).mp (m0.mp (m1.mp ?_))))))
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, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    x ∈ t →
      i (a * bottcherNear f d x) ∈ t →
        i (bottcherNear f d (f x)) = f x →
          bottcherNear f d (i (a * bottcherNear f d x)) = a * bottcherNear f d x →
            i (bottcherNear f d (f (i (a * bottcherNear f d x)))) = f (i (a * bottcherNear f d x)) →
              bottcherNear f d (i x) = x →
                i (bottcherNear f d x) = x →
                  (i (a * bottcherNear f d x, bottcherNear f d x).1 = i (a * bottcherNear f d x, bottcherNear f d x).2 →
                      (a * bottcherNear f d x, bottcherNear f d x).1 = (a * bottcherNear f d x, bottcherNear f d x).2) →
                    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:
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
⊢ ContinuousAt (fun z => f (i (a * bottcherNear f d z))) 0
Tactic:
refine s.fa0.continuousAt.comp_of_eq (ia.continuousAt.comp_of_eq t0 ?_) ?_
Proof state after:
case 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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ a * bottcherNear f d 0 = 0

case 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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ i (a * bottcherNear f d 0) = 0
Theorem: SuperAt.not_local_inj
Proof state before:
case 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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ a * bottcherNear f d 0 = 0

case 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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ i (a * bottcherNear f d 0) = 0
Tactic:
repeat' simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
case 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
t0 : ContinuousAt (fun z => a * bottcherNear f d z) 0
⊢ i (a * bottcherNear f d 0) = 0
Tactic:
simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0]
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 : ℂ
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
⊢ ∀ᶠ (z : ℂ) in 𝓝 0, i (a * bottcherNear f d z) ∈ t
Tactic:
refine (ia.continuousAt.comp_of_eq t0 ?_).eventually_mem (s.o.mem_nhds ?_)
Proof state after:
case 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
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
⊢ a * bottcherNear f d 0 = 0

case 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
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
⊢ (i ∘ fun z => a * bottcherNear f d z) 0 ∈ t
Theorem: SuperAt.not_local_inj
Proof state before:
case 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
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
⊢ a * bottcherNear f d 0 = 0

case 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
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
⊢ (i ∘ fun z => a * bottcherNear f d z) 0 ∈ t
Tactic:
repeat' simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0, s.t0, Function.comp]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof state before:
case 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
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
⊢ (i ∘ fun z => a * bottcherNear f d z) 0 ∈ t
Tactic:
simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0, s.t0, Function.comp]
Proof state after:
no goals
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
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
⊢ i (a * bottcherNear f d z) ≠ z
Tactic:
contrapose tp
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, 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)
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, 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)
Tactic:
simp only [ne_eq, Decidable.not_not, Classical.not_imp] at tp ⊢
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) = i (bottcherNear f d z) ∧ ¬a * bottcherNear f d z = bottcherNear f d z