internlm/Lean-Github huggingface dataset:
Theorem: Super.potential_basis'
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : s.potential c z = 0
⊢ z ∉ tᶜ
Tactic:
rw [s.potential_eq_zero_of_onePreimage] at m
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ z ∉ tᶜ
Theorem: Super.potential_basis'
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ z ∉ tᶜ
Tactic:
simp only [m, not_mem_compl_iff]
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ a ∈ t
Theorem: Super.potential_basis'
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
z : S
e : s.potential c z = sInf (s.potential c '' tᶜ)
m : z = a
⊢ a ∈ t
Tactic:
exact mem_of_mem_nhds n
Proof state after:
no goals
Theorem: Super.potential_basis'
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
o : IsOpen t
ne : (s.potential c '' tᶜ).Nonempty
pos : ∀ p ∈ s.potential c '' tᶜ, 0 ≤ p
below : BddBelow (s.potential c '' tᶜ)
q : ℝ
hq : sInf (s.potential c '' tᶜ) = q
qt : ∀ (z : S), s.potential c z < q → z ∈ t
mc : sInf (s.potential c '' tᶜ) ∈ closure (s.potential c '' tᶜ)
⊢ IsClosed (s.potential c '' tᶜ)
Tactic:
exact (o.isClosed_compl.isCompact.image (Continuous.potential s).along_snd).isClosed
Proof state after:
no goals
Theorem: Super.potential_basis
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
rcases mem_nhds_iff.mp n with ⟨t', tt, o, m⟩
Proof state after:
case 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Theorem: Super.potential_basis
Proof state before:
case 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
rcases s.potential_basis' c (o.mem_nhds m) o with ⟨p, pp, sub⟩
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
p : ℝ
pp : 0 < p
sub : {z | s.potential c z < p} ⊆ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Theorem: Super.potential_basis
Proof 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
inst✝ : OnePreimage s
c : ℂ
t : Set S
n : t ∈ 𝓝 a
t' : Set S
tt : t' ⊆ t
o : IsOpen t'
m : a ∈ t'
p : ℝ
pp : 0 < p
sub : {z | s.potential c z < p} ⊆ t'
⊢ ∃ p, 0 < p ∧ {z | s.potential c z < p} ⊆ t
Tactic:
use p, pp, _root_.trans sub tt
Proof state after:
no goals
Theorem: Super.isNice_zero
Proof 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 : ℂ
inst✝ : OnePreimage s
⊢ s.IsNiceN c 0 0
Tactic:
intro z zp
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Theorem: Super.isNice_zero
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
have za := le_antisymm zp s.potential_nonneg
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : s.potential c z = 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Theorem: Super.isNice_zero
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : s.potential c z = 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
simp only [s.potential_eq_zero_of_onePreimage] at za
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Theorem: Super.isNice_zero
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
rw [za, Function.iterate_zero_apply]
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, a) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Theorem: Super.isNice_zero
Proof 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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, a) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Tactic:
use s.mem_near c
Proof state after:
case right
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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Theorem: Super.isNice_zero
Proof state before:
case right
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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Tactic:
intro k _
Proof state after:
case right
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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Theorem: Super.isNice_zero
Proof state before:
case right
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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Tactic:
rw [s.iter_a]
Proof state after:
case right
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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) a ≠ 0
Theorem: Super.isNice_zero
Proof state before:
case right
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 : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) a ≠ 0
Tactic:
exact s.bottcherNear_mfderiv_ne_zero c
Proof state after:
no goals
Theorem: Super.isNiceN_mono
Proof 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 : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
⊢ s.IsNiceN c p n1
Tactic:
intro z zp
Proof 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 : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Theorem: Super.isNiceN_mono
Proof 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 : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
rcases nice z zp with ⟨m, nc⟩
Proof 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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
m : (c, (f c)^[n0] z) ∈ s.near
nc : ∀ (k : ℕ), n0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Theorem: Super.isNiceN_mono
Proof 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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
m : (c, (f c)^[n0] z) ∈ s.near
nc : ∀ (k : ℕ), n0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
use s.iter_stays_near' m n01, fun k n1k ↦ nc k (_root_.trans n01 n1k)
Proof state after:
no goals
Theorem: Super.has_nice_n
Proof 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
Proof 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
Theorem: Super.has_nice_n
Proof 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⟩
Proof 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
Theorem: Super.has_nice_n
Proof 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⟩
Proof 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
Theorem: Super.has_nice_n
Proof 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
Proof 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
Theorem: Super.has_nice_n
Proof 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⟩
Proof 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
Theorem: Super.has_nice_n
Proof 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
Proof 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
Theorem: Super.has_nice_n
Proof 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
Proof 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
Theorem: Super.has_nice_n
Proof 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
Proof 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
Theorem: Super.has_nice_n
Proof 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
Proof state after:
no goals
Theorem: Super.has_nice_n
Proof 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
Proof 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