Theorem: bottcher_eq_bottcherNear_z (Ray/Dynamics/Multibrot/Bottcher.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
have c0 : 0 < abs c := lt_trans (by norm_num) c16
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
have z0 : 0 < abs z := lt_of_lt_of_le c0 cz
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
set s := superF d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
set t := closedBall (0 : ℂ) (abs c)⁻¹
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
suffices e : EqOn (fun z : ℂ ↦ s.bottcher c (z : 𝕊)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t by
  have z0' : z ≠ 0 := Complex.abs.ne_zero_iff.mp z0.ne'
  convert @e z⁻¹ _; rw [inv_coe (inv_ne_zero z0'), inv_inv]
  simp only [mem_closedBall, Complex.dist_eq, sub_zero, map_inv₀, inv_le_inv z0 c0, cz, t]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
have a0 : HolomorphicOn I I (fun z : ℂ ↦ s.bottcher c (z : 𝕊)⁻¹) t := by
  intro z m
  refine (s.bottcher_holomorphicOn _ ?_).along_snd.comp (holomorphic_inv.comp holomorphic_coe _)
  simp only [mem_closedBall, Complex.dist_eq, sub_zero, t] at m
  by_cases z0 : z = 0; simp only [z0, coe_zero, inv_zero']; exact s.post_a c
  rw [inv_coe z0]; refine postcritical_large (by linarith) ?_
  rwa [map_inv₀, le_inv c0]; exact Complex.abs.pos z0
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
have a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t := by
  intro z m; apply AnalyticAt.holomorphicAt
  apply bottcherNear_analytic_z (superNearF d c)
  simp only [mem_setOf, mem_closedBall, Complex.dist_eq, sub_zero, t] at m ⊢
  refine lt_of_le_of_lt m ?_
  refine inv_lt_inv_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _)) ?_
  exact max_lt c16 (half_lt_self (lt_trans (by norm_num) c16))
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
refine (a0.eq_of_locally_eq a1 (convex_closedBall _ _).isPreconnected ?_).self_of_nhdsSet
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ ∃ x ∈ t, (𝓝 x).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ ∃ x ∈ t, (𝓝 x).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Tactic:
use 0, mem_closedBall_self (by bound)
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Tactic:
have e : ∀ᶠ z in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (z : 𝕊)⁻¹ := by
  simp only [Super.bottcherNear, extChartAt_inf_apply, inv_inv, toComplex_coe,
    RiemannSphere.inv_inf, toComplex_zero, sub_zero, Super.fl, eq_self_iff_true,
    Filter.eventually_true]
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Tactic:
refine Filter.EventuallyEq.trans ?_ (Filter.EventuallyEq.symm e)
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹
Tactic:
have i : Tendsto (fun z : ℂ ↦ (z : 𝕊)⁻¹) (𝓝 0) (𝓝 ∞) := by
  have h : ContinuousAt (fun z : ℂ ↦ (z : 𝕊)⁻¹) 0 :=
    (RiemannSphere.continuous_inv.comp continuous_coe).continuousAt
  simp only [ContinuousAt, coe_zero, inv_zero'] at h; exact h
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
i : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
i : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹
Tactic:
exact i.eventually (s.bottcher_eq_bottcherNear c)
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
have z0' : z ≠ 0 := Complex.abs.ne_zero_iff.mp z0.ne'
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
convert @e z⁻¹ _
State after:
case h.e'_2.h.e'_13
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ ↑z = (↑z⁻¹)⁻¹

c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t

State before:
case h.e'_2.h.e'_13
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ ↑z = (↑z⁻¹)⁻¹

c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t
Tactic:
rw [inv_coe (inv_ne_zero z0'), inv_inv]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, map_inv₀, inv_le_inv z0 c0, cz, t]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
Tactic:
intro z m
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (fun z => s.bottcher c (↑z)⁻¹) z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (fun z => s.bottcher c (↑z)⁻¹) z
Tactic:
refine (s.bottcher_holomorphicOn _ ?_).along_snd.comp (holomorphic_inv.comp holomorphic_coe _)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ (c, (↑z)⁻¹) ∈ s.post

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, t] at m
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (c, (↑z)⁻¹) ∈ s.post

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
by_cases z0 : z = 0
State after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

State before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
simp only [z0, coe_zero, inv_zero']
State after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, ∞) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

State before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, ∞) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
exact s.post_a c
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
rw [inv_coe z0]
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, ↑z⁻¹) ∈ s.post

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, ↑z⁻¹) ∈ s.post
Tactic:
refine postcritical_large (by linarith) ?_
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ Complex.abs (c, ↑z⁻¹).1 ≤ Complex.abs z⁻¹

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ Complex.abs (c, ↑z⁻¹).1 ≤ Complex.abs z⁻¹
Tactic:
rwa [map_inv₀, le_inv c0]
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ 0 < Complex.abs z

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ 0 < Complex.abs z
Tactic:
exact Complex.abs.pos z0
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ 4 ≤ Complex.abs (c, ↑z⁻¹).1
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
⊢ HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
intro z m
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (bottcherNear (fl (f d) ∞ c) d) z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (bottcherNear (fl (f d) ∞ c) d) z
Tactic:
apply AnalyticAt.holomorphicAt
State after:
case fa
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ (bottcherNear (fl (f d) ∞ c) d) z

State before:
case fa
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ (bottcherNear (fl (f d) ∞ c) d) z
Tactic:
apply bottcherNear_analytic_z (superNearF d c)
State after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}

State before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
simp only [mem_setOf, mem_closedBall, Complex.dist_eq, sub_zero, t] at m ⊢
State after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹

State before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine lt_of_le_of_lt m ?_
State after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹

State before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine inv_lt_inv_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _)) ?_
State after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ max 16 (Complex.abs c / 2) < Complex.abs c

State before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Tactic:
exact max_lt c16 (half_lt_self (lt_trans (by norm_num) c16))
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ 0 ≤ (Complex.abs c)⁻¹
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
Tactic:
simp only [Super.bottcherNear, extChartAt_inf_apply, inv_inv, toComplex_coe,
  RiemannSphere.inv_inf, toComplex_zero, sub_zero, Super.fl, eq_self_iff_true,
  Filter.eventually_true]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Tactic:
have h : ContinuousAt (fun z : ℂ ↦ (z : 𝕊)⁻¹) 0 :=
  (RiemannSphere.continuous_inv.comp continuous_coe).continuousAt
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : ContinuousAt (fun z => (↑z)⁻¹) 0
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : ContinuousAt (fun z => (↑z)⁻¹) 0
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Tactic:
simp only [ContinuousAt, coe_zero, inv_zero'] at h
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Tactic:
exact h
State after:
no goals