internlm/Lean-Github huggingface dataset:
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 e1 + 1 ≤ Nat.find e0
Tactic:
rw [Nat.succ_le_iff, Nat.lt_find_iff]
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
⊢ ∀ m ≤ Nat.find e1, (c, (f c)^[m] z) ∉ s.post
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
⊢ ∀ m ≤ Nat.find e1, (c, (f c)^[m] z) ∉ s.post
Tactic:
intro n n1
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
n : ℕ
n1 : n ≤ Nat.find e1
⊢ (c, (f c)^[n] z) ∉ s.post
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
n : ℕ
n1 : n ≤ Nat.find e1
⊢ (c, (f c)^[n] z) ∉ s.post
Tactic:
contrapose n1
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
n : ℕ
n1 : ¬(c, (f c)^[n] z) ∉ s.post
⊢ ¬n ≤ Nat.find e1
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
n : ℕ
n1 : ¬(c, (f c)^[n] z) ∉ s.post
⊢ ¬n ≤ Nat.find e1
Tactic:
simp only [not_not, not_le] at n1 ⊢
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
⊢ Nat.find e1 < n
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
⊢ Nat.find e1 < n
Tactic:
have n0 : n ≠ 0 := by
  contrapose p; simp only [not_not] at p ⊢
  simp only [p, Function.iterate_zero_apply] at n1; exact n1
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 < n
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 < n
Tactic:
rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← Nat.sub_add_cancel (Nat.pos_of_ne_zero n0)]
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 + 1 ≤ n - Nat.succ 0 + Nat.succ 0
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 + 1 ≤ n - Nat.succ 0 + Nat.succ 0
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 ≤ n - Nat.succ 0
Theorem: Super.bottcher_eqn
Proof state before:
case a.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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 ≤ n - Nat.succ 0
Tactic:
apply Nat.find_le
Proof state after:
case a.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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ (c, (f c)^[n - Nat.succ 0] (f c z)) ∈ s.post
Theorem: Super.bottcher_eqn
Proof state before:
case a.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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ (c, (f c)^[n - Nat.succ 0] (f c z)) ∈ s.post
Tactic:
simp only [← Function.iterate_succ_apply, Nat.succ_eq_add_one,
  Nat.sub_add_cancel (Nat.pos_of_ne_zero n0), n1, zero_add]
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
⊢ n ≠ 0
Tactic:
contrapose 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : ¬n ≠ 0
⊢ ¬(c, z) ∉ s.post
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
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : ¬n ≠ 0
⊢ ¬(c, z) ∉ s.post
Tactic:
simp only [not_not] at 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : n = 0
⊢ (c, z) ∈ s.post
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
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
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : n = 0
⊢ (c, z) ∈ s.post
Tactic:
simp only [p, Function.iterate_zero_apply] at n1
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
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
n : ℕ
p : n = 0
n1 : (c, z) ∈ s.post
⊢ (c, z) ∈ s.post
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
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
n : ℕ
p : n = 0
n1 : (c, z) ∈ s.post
⊢ (c, z) ∈ s.post
Tactic:
exact n1
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
⊢ (c, f c z) ∉ s.basin
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
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, f c z) ∉ s.basin
⊢ ¬(c, z) ∉ s.basin
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, f c z) ∉ s.basin
⊢ ¬(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
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, f c z) ∈ s.basin
⊢ (c, z) ∈ s.basin
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, f c z) ∈ s.basin
⊢ (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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ (c, z) ∈ s.basin
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
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ (c, z) ∈ s.basin
Tactic:
use n + 1
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
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ ((c, z).1, (f (c, z).1)^[n + 1] (c, z).2) ∈ s.near
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
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ ((c, z).1, (f (c, z).1)^[n + 1] (c, z).2) ∈ s.near
Tactic:
simp only at 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 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
n : ℕ
m : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
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
n : ℕ
m : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Tactic:
rwa [Function.iterate_succ_apply]
Proof state after:
no goals
Theorem: Super.bottcher_eqn_iter
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
n : ℕ
⊢ s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
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 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)^[0] z) = s.bottcher c z ^ d ^ 0

case succ
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 : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)
Theorem: Super.bottcher_eqn_iter
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 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)^[0] z) = s.bottcher c z ^ d ^ 0

case succ
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 : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_zero_apply, pow_zero, pow_one]
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
n : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)
Theorem: Super.bottcher_eqn_iter
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
n : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_succ_apply', s.bottcher_eqn, h, ← pow_mul, pow_succ]
Proof state after:
no goals
Theorem: Super.abs_bottcher
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
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
have base : ∀ {c z}, (c, z) ∈ s.post → abs (s.bottcher c z) = s.potential c z := by
  intro c z m; rcases s.ray_surj m with ⟨x, m, e⟩; rw [← e, s.bottcher_ray m, s.ray_potential 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
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
⊢ Complex.abs (s.bottcher c z) = s.potential c z