internlm/Lean-Github huggingface dataset:
Theorem: Super.bottcher_eqn
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      s.bottcher c (f c x) = s.bottcherNear c (f c x) →
        s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d
Tactic:
refine eventually_of_forall fun w m e0 e1 ↦ ?_
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcher c (f c w) = s.bottcher c w ^ d
Theorem: Super.bottcher_eqn
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
simp only [e0, e1]
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcherNear c (f c w) = s.bottcherNear c w ^ d
Theorem: Super.bottcher_eqn
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcherNear c (f c w) = s.bottcherNear c w ^ d
Tactic:
exact s.bottcherNear_eqn m
Proof state after:
no goals
Theorem: Super.bottcher_eqn
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
refine (HolomorphicOn.eq_of_locally_eq ?_ (fun z m ↦
  (s.bottcher_holomorphicOn (c, z) m).along_snd.pow) (s.post_slice_connected c).isPreconnected
  ⟨a, s.post_a c, e⟩).self_of_nhdsSet m
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
⊢ HolomorphicOn I I (fun x => s.bottcher c (f c x)) fun z => s.post (c, z)
Theorem: Super.bottcher_eqn
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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
⊢ HolomorphicOn I I (fun x => s.bottcher c (f c x)) fun z => s.post (c, z)
Tactic:
intro z m
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✝ x : ℂ
a z✝¹ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
m✝ : (c, z✝) ∈ s.post
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
z : S
m : z ∈ fun z => s.post (c, z)
⊢ HolomorphicAt I I (fun x => s.bottcher c (f c x)) z
Theorem: Super.bottcher_eqn
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✝ x : ℂ
a z✝¹ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z✝ : S
m✝ : (c, z✝) ∈ s.post
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
z : S
m : z ∈ fun z => s.post (c, z)
⊢ HolomorphicAt I I (fun x => s.bottcher c (f c x)) z
Tactic:
exact (s.bottcher_holomorphicOn _ (s.stays_post m)).along_snd.comp (s.fa _).along_snd
Proof state after:
no goals
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post := s.basin_post m
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post := by
  rcases e0 with ⟨n, e0⟩; use n
  simp only [← Function.iterate_succ_apply, Function.iterate_succ_apply']
  exact s.stays_post e0
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
simp only [Super.bottcher, e0, e1, dif_pos]
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] z)) ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] z)) ^ d
Tactic:
generalize hk0 : Nat.find e0 = k0
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d
Tactic:
generalize hk1 : Nat.find e1 = k1
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c ((f c)^[k1] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
kk : k0 = k1 + 1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c ((f c)^[k1] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d
Tactic:
simp only [kk, ← Function.iterate_succ_apply, Function.iterate_succ_apply']
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
kk : k0 = k1 + 1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) =
    ((fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) ^ (↑d)⁻¹) ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
kk : k0 = k1 + 1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) =
    ((fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) ^ (↑d)⁻¹) ^ d
Tactic:
rw [Complex.cpow_nat_inv_pow _ s.d0]
Proof state after:
no goals
Theorem: Super.bottcher_eqn
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
Tactic:
rcases e0 with ⟨n, e0⟩
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
Theorem: Super.bottcher_eqn
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, (f c)^[n] (f c z)) ∈ s.post
Theorem: Super.bottcher_eqn
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, (f c)^[n] (f c z)) ∈ s.post
Tactic:
simp only [← Function.iterate_succ_apply, Function.iterate_succ_apply']
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, f c ((f c)^[n] z)) ∈ s.post
Theorem: Super.bottcher_eqn
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, f c ((f c)^[n] z)) ∈ s.post
Tactic:
exact s.stays_post e0
Proof state after:
no goals
Theorem: Super.bottcher_eqn
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ k0 = k1 + 1
Tactic:
rw [← hk0, ← hk1]
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 = Nat.find e1 + 1
Theorem: Super.bottcher_eqn
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 = Nat.find e1 + 1
Tactic:
apply le_antisymm
Proof state after:
case a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 ≤ Nat.find e1 + 1

case a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e1 + 1 ≤ Nat.find e0
Theorem: Super.bottcher_eqn
Proof state before:
case a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 ≤ Nat.find e1 + 1
Tactic:
apply Nat.find_le
Proof state after:
case a.hn
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1 + 1] z) ∈ s.post
Theorem: Super.bottcher_eqn
Proof state before:
case a.hn
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1 + 1] z) ∈ s.post
Tactic:
simp only [Function.iterate_succ_apply]
Proof state after:
case a.hn
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1] (f c z)) ∈ s.post
Theorem: Super.bottcher_eqn
Proof state before:
case a.hn
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1] (f c z)) ∈ s.post
Tactic:
exact Nat.find_spec e1
Proof state after:
no goals