Theorem: Super.bottcher_not_basin (Ray/Dynamics/Bottcher.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c 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⟩
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

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]
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

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]
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

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
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c 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
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

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 ⊢
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

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⟩
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

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⟩
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

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
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

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⟩
State after:
no goals