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 ∈ 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
Tactic:
refine eventually_of_forall fun z m1 m0 t2 t0 t1 _ ib tp z0 ↦ ⟨?_, ?_⟩
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
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

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