internlm/Lean-Github huggingface dataset:
Theorem: multibrot_of_repeat
Proof state before:
case succ.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
⊢ ∃ k ≤ b, g (n + 1) = g k
Tactic:
by_cases e : k = b
Proof state after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : k = b
⊢ ∃ k ≤ b, g (n + 1) = g k

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ ∃ k ≤ b, g (n + 1) = g k
Theorem: multibrot_of_repeat
Proof state before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : k = b
⊢ ∃ k ≤ b, g (n + 1) = g k

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ ∃ k ≤ b, g (n + 1) = g k
Tactic:
use a + 1, Nat.succ_le_iff.mpr ab
Proof state after:
case right
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : k = b
⊢ g (n + 1) = g (a + 1)

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ ∃ k ≤ b, g (n + 1) = g k
Theorem: multibrot_of_repeat
Proof state before:
case right
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : k = b
⊢ g (n + 1) = g (a + 1)

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ ∃ k ≤ b, g (n + 1) = g k
Tactic:
rw [← hg, ← hg, Function.iterate_succ_apply', Function.iterate_succ_apply', hg, hg, nk, e, h]
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ ∃ k ≤ b, g (n + 1) = g k
Theorem: multibrot_of_repeat
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ ∃ k ≤ b, g (n + 1) = g k
Tactic:
use k + 1, Nat.succ_le_iff.mpr (Ne.lt_of_le e kb)
Proof state after:
case right
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ g (n + 1) = g (k + 1)
Theorem: multibrot_of_repeat
Proof state before:
case right
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
e : ¬k = b
⊢ g (n + 1) = g (k + 1)
Tactic:
rw [← hg, ← hg, Function.iterate_succ_apply', Function.iterate_succ_apply', hg, hg, nk]
Proof state after:
no goals
Theorem: multibrot_of_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
⊢ c ∈ multibrot d
Tactic:
have i0 : (f d c)^[0] c = c := by rw [Function.iterate_zero_apply]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
i0 : (f d c)^[0] ↑c = ↑c
⊢ c ∈ multibrot d
Theorem: multibrot_of_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
i0 : (f d c)^[0] ↑c = ↑c
⊢ c ∈ multibrot d
Tactic:
have i1 : (f d c)^[n + 1] c = c := by simp only [Function.iterate_succ_apply', h, f_0]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
i0 : (f d c)^[0] ↑c = ↑c
i1 : (f d c)^[n + 1] ↑c = ↑c
⊢ c ∈ multibrot d
Theorem: multibrot_of_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
i0 : (f d c)^[0] ↑c = ↑c
i1 : (f d c)^[n + 1] ↑c = ↑c
⊢ c ∈ multibrot d
Tactic:
exact multibrot_of_repeat (Nat.zero_lt_succ _) (_root_.trans i0 i1.symm)
Proof state after:
no goals
Theorem: multibrot_of_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
⊢ (f d c)^[0] ↑c = ↑c
Tactic:
rw [Function.iterate_zero_apply]
Proof state after:
no goals
Theorem: multibrot_of_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : (f d c)^[n] ↑c = 0
i0 : (f d c)^[0] ↑c = ↑c
⊢ (f d c)^[n + 1] ↑c = ↑c
Tactic:
simp only [Function.iterate_succ_apply', h, f_0]
Proof state after:
no goals
Theorem: multibrot_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 ∈ multibrot d
Tactic:
apply multibrot_of_zero
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (f d 0)^[?n] ↑0 = 0

case n
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ℕ
Theorem: multibrot_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (f d 0)^[?n] ↑0 = 0

case n
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ℕ
Tactic:
rw [Function.iterate_zero_apply, coe_zero]
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
⊢ c ∉ multibrot d
Tactic:
by_cases c2 : 2 < abs c
Proof state after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : 2 < Complex.abs c
⊢ c ∉ multibrot d

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d
Theorem: not_multibrot_of_two_lt
Proof state before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : 2 < Complex.abs c
⊢ c ∉ multibrot d

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d
Tactic:
exact multibrot_two_lt c2
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ c ∉ multibrot d
Tactic:
simp only [multibrot_coe, not_not]
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : ¬2 < Complex.abs c
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
simp only [not_lt] at c2
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
generalize hs : abs ((f' d c)^[n] c) = s
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
s : ℝ
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : 2 < Complex.abs ((f' d c)^[n] c)
c2 : Complex.abs c ≤ 2
s : ℝ
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
rw [hs] at h
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
have s1 : 1 ≤ s := by linarith
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
have s1' : 1 ≤ s - 1 := by linarith
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
have s0 : 0 ≤ s := by linarith
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
simp only [tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs]
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] c)) atTop atTop
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] c)) atTop atTop
Tactic:
rw [← Filter.tendsto_add_atTop_iff_nat n]
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n_1 => Complex.abs ((f' d c)^[n_1 + n] c)) atTop atTop
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n_1 => Complex.abs ((f' d c)^[n_1 + n] c)) atTop atTop
Tactic:
apply Filter.tendsto_atTop_mono b
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => s * (s - 1) ^ n) atTop atTop
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => s * (s - 1) ^ n) atTop atTop
Tactic:
refine Filter.Tendsto.mul_atTop (by linarith) tendsto_const_nhds ?_
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => (s - 1) ^ n) atTop atTop
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ Tendsto (fun n => (s - 1) ^ n) atTop atTop
Tactic:
apply tendsto_pow_atTop_atTop_of_one_lt
Proof state after:
case neg.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ 1 < s - 1
Theorem: not_multibrot_of_two_lt
Proof state before:
case neg.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ 1 < s - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
⊢ 1 ≤ s
Tactic:
linarith
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
⊢ 1 ≤ s - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
⊢ 0 ≤ s
Tactic:
linarith
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
Tactic:
intro k
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
⊢ s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
⊢ s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
Tactic:
induction' k with k p
Proof state after:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ s * (s - 1) ^ 0 ≤ Complex.abs ((f' d c)^[0 + n] c)

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs ((f' d c)^[k + 1 + n] c)
Theorem: not_multibrot_of_two_lt
Proof state before:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
⊢ s * (s - 1) ^ 0 ≤ Complex.abs ((f' d c)^[0 + n] c)
Tactic:
simp only [pow_zero, mul_one, zero_add, Nat.zero_eq, hs, le_refl]
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs ((f' d c)^[k + 1 + n] c)
Tactic:
simp only [Nat.succ_add, Function.iterate_succ_apply']
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c ((f' d c)^[k + n] c))
Theorem: not_multibrot_of_two_lt
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c ((f' d c)^[k + n] c))
Tactic:
generalize hz : (f' d c)^[k + n] c = z
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
z : ℂ
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Theorem: not_multibrot_of_two_lt
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
p : s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
z : ℂ
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
rw [hz] at p
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Theorem: not_multibrot_of_two_lt
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
have ss1 : 1 ≤ s * (s - 1) ^ k := by bound
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Theorem: not_multibrot_of_two_lt
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
have k2 : k ≤ k * 2 := by linarith
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Theorem: not_multibrot_of_two_lt
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s * (s - 1) ^ (k + 1) ≤ Complex.abs (f' d c z)
Tactic:
calc abs (f' d c z)
  _ = abs (z ^ d + c) := rfl
  _ ≥ abs (z ^ d) - abs c := by bound
  _ = abs z ^ d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ (s * (s - 1) ^ k) ^ d - 2 := by bound
  _ ≥ (s * (s - 1) ^ k) ^ 2 - 2 := by bound
  _ = s ^ 2 * (s - 1) ^ (k * 2) - 2 * 1 := by rw [mul_pow, pow_mul, mul_one]
  _ ≥ s ^ 2 * (s - 1) ^ k - s * (s - 1) ^ k := by bound
  _ = s * ((s - 1) ^ k * (s - 1)) := by ring
  _ = s * (s - 1) ^ (k + 1) := by rw [pow_succ]
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
⊢ 1 ≤ s * (s - 1) ^ k
Tactic:
bound
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
⊢ k ≤ k * 2
Tactic:
linarith
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ Complex.abs (z ^ d + c) ≥ Complex.abs (z ^ d) - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ Complex.abs (z ^ d) - Complex.abs c = Complex.abs z ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ Complex.abs z ^ d - Complex.abs c ≥ (s * (s - 1) ^ k) ^ d - 2
Tactic:
bound
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ (s * (s - 1) ^ k) ^ d - 2 ≥ (s * (s - 1) ^ k) ^ 2 - 2
Tactic:
bound
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ (s * (s - 1) ^ k) ^ 2 - 2 = s ^ 2 * (s - 1) ^ (k * 2) - 2 * 1
Tactic:
rw [mul_pow, pow_mul, mul_one]
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s ^ 2 * (s - 1) ^ (k * 2) - 2 * 1 ≥ s ^ 2 * (s - 1) ^ k - s * (s - 1) ^ k
Tactic:
bound
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s ^ 2 * (s - 1) ^ k - s * (s - 1) ^ k = s * ((s - 1) ^ k * (s - 1))
Tactic:
ring
Proof state after:
no goals
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
k : ℕ
z : ℂ
p : s * (s - 1) ^ k ≤ Complex.abs z
hz : (f' d c)^[k + n] c = z
ss1 : 1 ≤ s * (s - 1) ^ k
k2 : k ≤ k * 2
⊢ s * ((s - 1) ^ k * (s - 1)) = s * (s - 1) ^ (k + 1)
Tactic:
rw [pow_succ]
Proof state after:
no goals