internlm/Lean-Github huggingface dataset:
Theorem: Super.attracts
Proof state before:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      (s.fl c ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) + ↑(extChartAt I a) a) =
    f c ((f c)^[k] ((f c)^[n] z))
Tactic:
generalize hx : (s.fl c)^[k] (extChartAt I a ((f c)^[n] z) - extChartAt I a a) = x
Proof state after:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
x : ℂ
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))
Theorem: Super.attracts
Proof state before:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
x : ℂ
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))
Tactic:
rw [hx] at h
Proof state after:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))
Theorem: Super.attracts
Proof state before:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))
Tactic:
simp only [Super.fl, _root_.fl, Function.comp, sub_add_cancel, h,
  ←Function.iterate_succ_apply' (f c)]
Proof state after:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[k.succ] ((f c)^[n] z))) = (f c)^[k.succ] ((f c)^[n] z)
Theorem: Super.attracts
Proof state before:
case succ
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[k.succ] ((f c)^[n] z))) = (f c)^[k.succ] ((f c)^[n] z)
Tactic:
apply PartialEquiv.left_inv _ (s.near_subset_chart (s.iter_stays_near r _))
Proof state after:
no goals
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ContinuousAt g 0
Tactic:
rw [← hg]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
Tactic:
refine (continuousAt_extChartAt_symm'' I ?_).comp
  (continuous_id.add continuous_const).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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
simp only [zero_add]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
exact mem_extChartAt_target I a
Proof state after:
no goals
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ g 0 = a
Tactic:
simp only [← hg]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a) = a
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a) = a
Tactic:
simp only [zero_add]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
Theorem: Super.attracts
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
Tactic:
exact PartialEquiv.left_inv _ (mem_extChartAt_source _ _)
Proof state after:
no goals
Theorem: Super.isOpen_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 : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ IsOpen s.basin
Tactic:
simp only [Super.basin, setOf_exists]
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
⊢ IsOpen (⋃ i, {x | (x.1, (f x.1)^[i] x.2) ∈ s.near})
Theorem: Super.isOpen_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 : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ IsOpen (⋃ i, {x | (x.1, (f x.1)^[i] x.2) ∈ s.near})
Tactic:
exact isOpen_iUnion fun n ↦ s.isOpen_preimage n
Proof state after:
no goals
Theorem: Super.basin_stays
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
m : (c, z) ∈ s.basin
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
simp only [Super.basin, Set.mem_setOf] 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Theorem: Super.basin_stays
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
m : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Theorem: Super.basin_stays
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
rw [Filter.eventually_atTop]
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ a_1, ∀ b ≥ a_1, (c, (f c)^[b] z) ∈ s.near
Theorem: Super.basin_stays
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ a_1, ∀ b ≥ a_1, (c, (f c)^[b] z) ∈ s.near
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ b ≥ n, (c, (f c)^[b] z) ∈ s.near
Theorem: Super.basin_stays
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
⊢ ∀ b ≥ n, (c, (f c)^[b] z) ∈ s.near
Tactic:
intro k kn
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k] z) ∈ s.near
Theorem: Super.basin_stays
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k] z) ∈ s.near
Tactic:
rw [← Nat.sub_add_cancel kn, Function.iterate_add_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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k - n] ((f c)^[n] z)) ∈ s.near
Theorem: Super.basin_stays
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
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
k : ℕ
kn : k ≥ n
⊢ (c, (f c)^[k - n] ((f c)^[n] z)) ∈ s.near
Tactic:
exact s.iter_stays_near m _
Proof state after:
no goals
Theorem: Super.basin_attracts
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
m : (c, z) ∈ s.basin
⊢ Attracts (f c) z a
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
m : ((c, z).1, (f (c, z).1)^[n] (c, z).2) ∈ s.near
⊢ Attracts (f c) z a
Theorem: Super.basin_attracts
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
n : ℕ
m : ((c, z).1, (f (c, z).1)^[n] (c, z).2) ∈ s.near
⊢ Attracts (f c) z a
Tactic:
exact s.attracts m
Proof state after:
no goals
Theorem: Super.basin_iff_attracts
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, z) ∈ s.basin ↔ Attracts (f c) z a
Tactic:
constructor
Proof state after:
case mp
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, z) ∈ s.basin → Attracts (f c) z a

case mpr
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
⊢ Attracts (f c) z a → (c, z) ∈ s.basin
Theorem: Super.basin_iff_attracts
Proof state before:
case mp
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, z) ∈ s.basin → Attracts (f c) z a

case mpr
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
⊢ Attracts (f c) z a → (c, z) ∈ s.basin
Tactic:
exact s.basin_attracts
Proof state after:
case mpr
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
⊢ Attracts (f c) z a → (c, z) ∈ s.basin
Theorem: Super.basin_iff_attracts
Proof state before:
case mpr
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
⊢ Attracts (f c) z a → (c, z) ∈ s.basin
Tactic:
intro h
Proof state after:
case mpr
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
h : Attracts (f c) z a
⊢ (c, z) ∈ s.basin
Theorem: Super.basin_iff_attracts
Proof state before:
case mpr
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
h : Attracts (f c) z a
⊢ (c, z) ∈ s.basin
Tactic:
rcases tendsto_atTop_nhds.mp h {z | (c, z) ∈ s.near} (s.mem_near c)
  (s.isOpen_near.snd_preimage c) with ⟨n, h⟩
Proof state after:
case mpr.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
h✝ : Attracts (f c) z a
n : ℕ
h : ∀ (n_1 : ℕ), n ≤ n_1 → (f c)^[n_1] z ∈ {z | (c, z) ∈ s.near}
⊢ (c, z) ∈ s.basin
Theorem: Super.basin_iff_attracts
Proof state before:
case mpr.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
h✝ : Attracts (f c) z a
n : ℕ
h : ∀ (n_1 : ℕ), n ≤ n_1 → (f c)^[n_1] z ∈ {z | (c, z) ∈ s.near}
⊢ (c, z) ∈ s.basin
Tactic:
exact ⟨n, h _ (le_refl _)⟩
Proof state after:
no goals
Theorem: Super.fp1
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
n : ℕ
p : ℂ × S
⊢ (s.fp^[n] p).1 = p.1
Tactic:
induction' n with n h
Proof state after:
case zero
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
p : ℂ × S
⊢ (s.fp^[0] p).1 = p.1

case succ
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
p : ℂ × S
n : ℕ
h : (s.fp^[n] p).1 = p.1
⊢ (s.fp^[n + 1] p).1 = p.1
Theorem: Super.fp1
Proof state before:
case zero
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
p : ℂ × S
⊢ (s.fp^[0] p).1 = p.1
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
no goals
Theorem: Super.fp1
Proof state before:
case succ
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
p : ℂ × S
n : ℕ
h : (s.fp^[n] p).1 = p.1
⊢ (s.fp^[n + 1] p).1 = p.1
Tactic:
simp only [Function.iterate_succ_apply', h, fp]
Proof state after:
no goals