internlm/Lean-Github huggingface dataset:
Theorem: Super.post_slice_connected
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 : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected {z | (c, z) ∈ s.post}
Tactic:
rw [e]
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 : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected (↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext})
Theorem: Super.post_slice_connected
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 : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected (↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext})
Tactic:
exact (s.ext_slice_connected c).image _ (s.homeomorphSlice c).continuousOn
Proof state after:
no goals
Theorem: Super.bottcher_not_basin
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
m : (c, z) ∉ s.basin
⊢ s.bottcher c z = 1
Tactic:
have p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post := by
  contrapose m; simp only [not_not] at m ⊢; rcases m with ⟨n, m⟩
  rcases s.post_basin m with ⟨k, m⟩
  simp only [← Function.iterate_add_apply] at m; exact ⟨k + n, 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
m : (c, z) ∉ s.basin
p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c z = 1
Theorem: Super.bottcher_not_basin
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
m : (c, z) ∉ s.basin
p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c z = 1
Tactic:
simp only [Super.bottcher, p]
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
m : (c, z) ∉ s.basin
p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ (if h : False then (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] z)) else 1) = 1
Theorem: Super.bottcher_not_basin
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
m : (c, z) ∉ s.basin
p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ (if h : False then (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] z)) else 1) = 1
Tactic:
rw [dif_neg]
Proof state after:
case hnc
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
m : (c, z) ∉ s.basin
p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ ¬False
Theorem: Super.bottcher_not_basin
Proof state before:
case hnc
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
m : (c, z) ∉ s.basin
p : ¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ ¬False
Tactic:
exact not_false
Proof state after:
no goals
Theorem: Super.bottcher_not_basin
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
m : (c, z) ∉ s.basin
⊢ ¬∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
contrapose 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
m : ¬¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ ¬(c, z) ∉ s.basin
Theorem: Super.bottcher_not_basin
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
m : ¬¬∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ ¬(c, z) ∉ s.basin
Tactic:
simp only [not_not] at 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
m : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ (c, z) ∈ s.basin
Theorem: Super.bottcher_not_basin
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
m : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ (c, z) ∈ s.basin
Tactic:
rcases m with ⟨n, m⟩
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.post
⊢ (c, z) ∈ s.basin
Theorem: Super.bottcher_not_basin
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.post
⊢ (c, z) ∈ s.basin
Tactic:
rcases s.post_basin m with ⟨k, 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.post
k : ℕ
m : ((c, (f c)^[n] z).1, (f (c, (f c)^[n] z).1)^[k] (c, (f c)^[n] z).2) ∈ s.near
⊢ (c, z) ∈ s.basin
Theorem: Super.bottcher_not_basin
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.post
k : ℕ
m : ((c, (f c)^[n] z).1, (f (c, (f c)^[n] z).1)^[k] (c, (f c)^[n] z).2) ∈ s.near
⊢ (c, z) ∈ s.basin
Tactic:
simp only [← Function.iterate_add_apply] 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.post
k : ℕ
m : (c, (f c)^[k + n] z) ∈ s.near
⊢ (c, z) ∈ s.basin
Theorem: Super.bottcher_not_basin
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.post
k : ℕ
m : (c, (f c)^[k + n] z) ∈ s.near
⊢ (c, z) ∈ s.basin
Tactic:
exact ⟨k + n, 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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have h0 : ∀ {c z}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d := by
  intro c z m
  suffices e : ∀ᶠ w in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d by
    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
    intro z m
    exact (s.bottcher_holomorphicOn _ (s.stays_post m)).along_snd.comp (s.fa _).along_snd
  have e := s.bottcher_eq_bottcherNear c
  have fc := (s.fa (c, a)).along_snd.continuousAt; simp only [ContinuousAt, s.f0] at fc
  apply e.mp; apply (fc.eventually e).mp
  apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).mp
  refine eventually_of_forall fun w m e0 e1 ↦ ?_; simp only at m e0 e1
  simp only [e0, e1]; exact s.bottcherNear_eqn 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
⊢ s.bottcher c (f c z) = s.bottcher c z ^ 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
by_cases p : (c, z) ∈ s.post
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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

case neg
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
⊢ 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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

case neg
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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
simp only [h0 p]
Proof state after:
case neg
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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case neg
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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
by_cases m : (c, z) ∈ s.basin
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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

case neg
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
Theorem: Super.bottcher_eqn
Proof state before:
case neg
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 m1 : (c, f c z) ∉ s.basin := by
  contrapose m; simp only [not_not] at m ⊢
  rcases m with ⟨n, m⟩; use n + 1; simp only at m ⊢; rwa [Function.iterate_succ_apply]
Proof state after:
case neg
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
m1 : (c, f c z) ∉ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Theorem: Super.bottcher_eqn
Proof state before:
case neg
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
m1 : (c, f c z) ∉ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
simp only [s.bottcher_not_basin m, s.bottcher_not_basin m1, one_pow]
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}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
intro c 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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ 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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
suffices e : ∀ᶠ w in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d by
  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
  intro z m
  exact (s.bottcher_holomorphicOn _ (s.stays_post m)).along_snd.comp (s.fa _).along_snd
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
⊢ ∀ᶠ (w : S) in 𝓝 a, 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
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
have e := s.bottcher_eq_bottcherNear c
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
⊢ ∀ᶠ (w : S) in 𝓝 a, 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
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
have fc := (s.fa (c, a)).along_snd.continuousAt
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 : ContinuousAt (fun y => f c y) a
⊢ ∀ᶠ (w : S) in 𝓝 a, 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 : ContinuousAt (fun y => f c y) a
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
simp only [ContinuousAt, s.f0] at fc
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) in 𝓝 a, 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) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
apply e.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✝ 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, s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ 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)
⊢ ∀ᶠ (x : S) in 𝓝 a, s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d
Tactic:
apply (fc.eventually e).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✝ 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,
    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
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,
    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:
apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near 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✝ 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