Theorem: Super.potential_minima_only_a (Ray/Dynamics/Postcritical.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
⊢ z = a
Tactic:
contrapose m
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
⊢ ¬∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
⊢ ¬∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
Tactic:
simp only [Filter.not_eventually, not_le]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
rcases s.nice_nz p.basin z (le_refl _) with ⟨near, nc⟩
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
set f : S → ℂ := s.bottcherNearIter (s.nz c z) c
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
have o : 𝓝 (f z) = Filter.map f (𝓝 z) :=
  (nontrivialHolomorphicAt_of_mfderiv_ne_zero (s.bottcherNearIter_holomorphic near).along_snd
      (s.bottcherNearIter_mfderiv_ne_zero (nc _ (le_refl _))
        (p.not_precritical ((s.potential_ne_zero _).mpr m)))).nhds_eq_map_nhds
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
have e : ∃ᶠ x : ℂ in 𝓝 (f z), abs x < abs (f z) := by
  apply frequently_smaller; contrapose m; simp only [not_not] at m ⊢
  replace m := (s.bottcherNear_eq_zero near).mp m
  rw [s.preimage_eq] at m; exact m
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (x : ℂ) in 𝓝 (f z), Complex.abs x < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (x : ℂ) in 𝓝 (f z), Complex.abs x < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
rw [o, Filter.frequently_map] at e
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
apply e.mp
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z, Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z, Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z
Tactic:
apply (((s.isOpen_preimage _).snd_preimage c).eventually_mem near).mp
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}} →
      Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}} →
      Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z
Tactic:
refine eventually_of_forall fun w m lt ↦ ?_
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : w ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}}
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : w ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}}
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Tactic:
rw [mem_setOf, mem_setOf] at m
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : ((c, w).1, (f✝ (c, w).1)^[s.nz c z] (c, w).2) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : ((c, w).1, (f✝ (c, w).1)^[s.nz c z] (c, w).2) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Tactic:
simp only at m
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Tactic:
simp only [s.potential_eq m, s.potential_eq near, Super.potential']
State after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] w)) ^ (↑d ^ s.nz c z)⁻¹ <
    Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] z)) ^ (↑d ^ s.nz c z)⁻¹

State before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] w)) ^ (↑d ^ s.nz c z)⁻¹ <
    Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] z)) ^ (↑d ^ s.nz c z)⁻¹
Tactic:
exact Real.rpow_lt_rpow (Complex.abs.nonneg _) lt
  (inv_pos.mpr (pow_pos (Nat.cast_pos.mpr s.dp) _))
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ ∃ᶠ (x : ℂ) in 𝓝 (f z), Complex.abs x < Complex.abs (f z)
Tactic:
apply frequently_smaller
State after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ f z ≠ 0

State before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ f z ≠ 0
Tactic:
contrapose m
State after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : ¬f z ≠ 0
⊢ ¬¬z = a

State before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : ¬f z ≠ 0
⊢ ¬¬z = a
Tactic:
simp only [not_not] at m ⊢
State after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : f z = 0
⊢ z = a

State before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : f z = 0
⊢ z = a
Tactic:
replace m := (s.bottcherNear_eq_zero near).mp m
State after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : (f✝ c)^[s.nz c z] z = a
⊢ z = a

State before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : (f✝ c)^[s.nz c z] z = a
⊢ z = a
Tactic:
rw [s.preimage_eq] at m
State after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : z = a
⊢ z = a

State before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : z = a
⊢ z = a
Tactic:
exact m
State after:
no goals