Theorem: SuperAt.not_local_inj (Ray/Dynamics/Multiple.lean)

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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases s.superNear with ⟨t, s⟩
State after:
case 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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case 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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have ba : AnalyticAt ℂ (bottcherNear f d) 0 := bottcherNear_analytic_z s _ s.t0
State after:
case 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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case 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 : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have nc : mfderiv I I (bottcherNear f d) 0 ≠ 0 := by
  rw [mfderiv_eq_fderiv, ← deriv_fderiv, (bottcherNear_monic s).deriv]
  exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
State after:
case 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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case 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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases complex_inverse_fun' (ba.holomorphicAt I I) nc with ⟨i, ia, ib, bi⟩
State after:
case intro.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 : ℂ → ℂ
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 (bottcherNear f d 0)
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 (bottcherNear f d 0), bottcherNear f d (i x) = x
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case intro.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 : ℂ → ℂ
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 (bottcherNear f d 0)
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 (bottcherNear f d 0), bottcherNear f d (i x) = x
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rw [bottcherNear_zero] at bi ia
State after:
case intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have i0 : i 0 = 0 := by nth_rw 1 [← bottcherNear_zero]; rw [ib.self_of_nhds]
State after:
case intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have inj : ∀ᶠ p : ℂ × ℂ in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2 := by
  refine ia.local_inj ?_
  have d0 : mfderiv I I (fun z : ℂ ↦ z) 0 ≠ 0 := id_mderiv_ne_zero
  rw [(Filter.EventuallyEq.symm ib).mfderiv_eq] at d0
  rw [←Function.comp_def, mfderiv_comp 0 _ ba.differentiableAt.mdifferentiableAt] at d0
  simp only [Ne, mderiv_comp_eq_zero_iff, nc, or_false_iff] at d0
  rw [bottcherNear_zero] at d0; exact d0
  rw [bottcherNear_zero]; exact ia.mdifferentiableAt
State after:
case intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases exist_root_of_unity s.d2 with ⟨a, a1, ad⟩
State after:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z

State before:
case intro.intro.intro.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 : ℂ → ℂ
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
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
refine ⟨fun z ↦ i (a * bottcherNear f d z), ?_, ?_, ?_⟩
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
⊢ AnalyticAt ℂ (fun z => i (a * bottcherNear f d z)) 0

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

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

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
⊢ mfderiv I I (bottcherNear f d) 0 ≠ 0
Tactic:
rw [mfderiv_eq_fderiv, ← deriv_fderiv, (bottcherNear_monic s).deriv]
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
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0

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
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Tactic:
exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
State after:
no goals

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
⊢ 1 ≠ 0
Tactic:
norm_num
State after:
no goals

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
⊢ i 0 = 0
Tactic:
nth_rw 1 [← bottcherNear_zero]
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
⊢ i (bottcherNear ?m.13266 ?m.13267 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
⊢ ℂ → ℂ

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
⊢ ℕ

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
⊢ i (bottcherNear ?m.13266 ?m.13267 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
⊢ ℂ → ℂ

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
⊢ ℕ
Tactic:
rw [ib.self_of_nhds]
State after:
no goals

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
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (0, 0), i p.1 = i p.2 → p.1 = p.2
Tactic:
refine ia.local_inj ?_
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
⊢ mfderiv I I i 0 ≠ 0

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
⊢ mfderiv I I i 0 ≠ 0
Tactic:
have d0 : mfderiv I I (fun z : ℂ ↦ z) 0 ≠ 0 := id_mderiv_ne_zero
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 (fun z => z) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0

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 (fun z => z) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0
Tactic:
rw [(Filter.EventuallyEq.symm ib).mfderiv_eq] at d0
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 (fun x => i (bottcherNear f d x)) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0

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 (fun x => i (bottcherNear f d x)) 0 ≠ 0
⊢ mfderiv I I i 0 ≠ 0
Tactic:
rw [←Function.comp_def, mfderiv_comp 0 _ ba.differentiableAt.mdifferentiableAt] at d0
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 (bottcherNear f d 0)).comp (mfderiv I I (bottcherNear f d) 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)

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 (bottcherNear f d 0)).comp (mfderiv I I (bottcherNear f d) 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:
simp only [Ne, mderiv_comp_eq_zero_iff, nc, or_false_iff] at d0
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 (bottcherNear f d 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)

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 (bottcherNear f d 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:
rw [bottcherNear_zero] at d0
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 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)

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
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)

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]
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

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
State after:
no goals

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
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

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)) ?_
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

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]
State after:
no goals

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]
State after:
no goals

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]
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

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
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

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]
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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 ?_))))))
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

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 ↦ ⟨?_, ?_⟩
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

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 ?_) ?_
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

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]
State after:
no goals

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]
State after:
no goals

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 ?_)
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

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]
State after:
no goals

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]
State after:
no goals

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
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)

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 ⊢
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

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]
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

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
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

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
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

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 ⊢
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

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
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

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals