Theorem: Super.has_nice_n (Ray/Dynamics/Potential.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∃ n, s.IsNiceN c p n
Tactic:
have et : ∀ᶠ z in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0 := by
  apply
    (mfderiv_ne_zero_eventually (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd
        (s.bottcherNear_mfderiv_ne_zero c)).mp
  apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).mp
  refine eventually_of_forall fun z m nc ↦ ?_; use m, nc
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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
et : ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
⊢ ∃ n, s.IsNiceN c p n

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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
et : ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
⊢ ∃ n, s.IsNiceN c p n
Tactic:
rcases et.exists_mem with ⟨t, m, h⟩
State after:
case intro.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
et : ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
t : Set S
m : t ∈ 𝓝 a
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
⊢ ∃ n, s.IsNiceN c p n

State before:
case intro.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
et : ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
t : Set S
m : t ∈ 𝓝 a
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
⊢ ∃ n, s.IsNiceN c p n
Tactic:
rcases s.potential_basis c m with ⟨q, qp, qt⟩
State after:
case intro.intro.intro.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
et : ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
t : Set S
m : t ∈ 𝓝 a
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
⊢ ∃ n, s.IsNiceN c p n

State before:
case intro.intro.intro.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
et : ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
t : Set S
m : t ∈ 𝓝 a
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
⊢ ∃ n, s.IsNiceN c p n
Tactic:
clear et m
State after:
case intro.intro.intro.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
⊢ ∃ n, s.IsNiceN c p n

State before:
case intro.intro.intro.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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
⊢ ∃ n, s.IsNiceN c p n
Tactic:
rcases exists_pow_lt_of_lt_one qp p1 with ⟨n, pq⟩
State after:
case intro.intro.intro.intro.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 : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
⊢ ∃ n, s.IsNiceN c p n

State before:
case intro.intro.intro.intro.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 : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
⊢ ∃ n, s.IsNiceN c p n
Tactic:
use n
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
⊢ s.IsNiceN c p n

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
⊢ s.IsNiceN c p n
Tactic:
intro z m
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
⊢ (c, (f c)^[n] z) ∈ s.near ∧ ∀ (k : ℕ), n ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
⊢ (c, (f c)^[n] z) ∈ s.near ∧ ∀ (k : ℕ), n ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
replace m : ∀ k, n ≤ k → s.potential c ((f c)^[k] z) < q := by
  intro k nk; refine lt_of_le_of_lt ?_ pq; simp only [s.potential_eqn_iter]
  have dn := (Nat.lt_pow_self s.d1 k).le
  apply _root_.trans (pow_le_pow_of_le_one s.potential_nonneg s.potential_le_one dn)
  refine _root_.trans (pow_le_pow_left s.potential_nonneg m _) ?_
  exact pow_le_pow_of_le_one (_root_.trans s.potential_nonneg m) p1.le nk
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : ∀ (k : ℕ), n ≤ k → s.potential c ((f c)^[k] z) < q
⊢ (c, (f c)^[n] z) ∈ s.near ∧ ∀ (k : ℕ), n ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : ∀ (k : ℕ), n ≤ k → s.potential c ((f c)^[k] z) < q
⊢ (c, (f c)^[n] z) ∈ s.near ∧ ∀ (k : ℕ), n ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
use(h _ (qt (m n (le_refl _)))).1, fun k nk ↦ (h _ (qt (m k nk))).2
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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (z : S) in 𝓝 a, (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
Tactic:
apply
  (mfderiv_ne_zero_eventually (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd
      (s.bottcherNear_mfderiv_ne_zero c)).mp
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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0

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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0
Tactic:
apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).mp
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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0

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 : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0
Tactic:
refine eventually_of_forall fun z m nc ↦ ?_
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
z : S
m : z ∈ {b | (c, b) ∈ s.near}
nc : mfderiv I I (fun y => s.bottcherNear c y) z ≠ 0
⊢ (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0

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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
z : S
m : z ∈ {b | (c, b) ∈ s.near}
nc : mfderiv I I (fun y => s.bottcherNear c y) z ≠ 0
⊢ (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
Tactic:
use m, nc
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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
⊢ ∀ (k : ℕ), n ≤ k → s.potential c ((f c)^[k] z) < q
Tactic:
intro k nk
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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) < q

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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) < q
Tactic:
refine lt_of_le_of_lt ?_ pq
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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) ≤ p ^ n

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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) ≤ p ^ n
Tactic:
simp only [s.potential_eqn_iter]
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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n

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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n
Tactic:
have dn := (Nat.lt_pow_self s.d1 k).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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n

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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n
Tactic:
apply _root_.trans (pow_le_pow_of_le_one s.potential_nonneg s.potential_le_one dn)
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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ k ≤ p ^ n

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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ k ≤ p ^ n
Tactic:
refine _root_.trans (pow_le_pow_left s.potential_nonneg 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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ p ^ k ≤ p ^ n

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✝ : S
d n✝ : ℕ
s : Super f d a
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ p ^ k ≤ p ^ n
Tactic:
exact pow_le_pow_of_le_one (_root_.trans s.potential_nonneg m) p1.le nk
State after:
no goals