Theorem: multibrot_of_repeat (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
⊢ c ∈ multibrot d
Tactic:
generalize hg : (fun n ↦ (f' d c)^[n] c) = g
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : (fun n => (f' d c)^[n] c) = g
⊢ c ∈ multibrot d

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : (fun n => (f' d c)^[n] c) = g
⊢ c ∈ multibrot d
Tactic:
replace hg : ∀ n, (f' d c)^[n] c = g n := fun n ↦ by rw [← hg]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
⊢ c ∈ multibrot d

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
⊢ c ∈ multibrot d
Tactic:
simp only [f_f'_iter, ← coe_zero, coe_eq_coe, hg] at h
State after:
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
⊢ c ∈ multibrot d

State before:
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ c ∈ multibrot d
Tactic:
simp only [multibrot_coe, atInf_basis.tendsto_right_iff, true_imp_iff, not_forall,
  Filter.not_eventually, mem_setOf, not_lt, Complex.norm_eq_abs, hg]
State after:
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ x, ∃ᶠ (x_1 : ℕ) in atTop, Complex.abs (g x_1) ≤ x

State before:
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ x, ∃ᶠ (x_1 : ℕ) in atTop, Complex.abs (g x_1) ≤ x
Tactic:
use partialSups (fun k ↦ Complex.abs (g k)) b
State after:
case h
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ᶠ (x : ℕ) in atTop, Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b

State before:
case h
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ᶠ (x : ℕ) in atTop, Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
apply Filter.frequently_of_forall
State after:
case h.h
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∀ (x : ℕ), Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b

State before:
case h.h
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∀ (x : ℕ), Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
intro k
State after:
case h.h
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k : ℕ
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b

State before:
case h.h
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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k : ℕ
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
rcases lo k with ⟨l, lb, kl⟩
State after:
case h.h.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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b

State before:
case h.h.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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
rw [kl]
State after:
case h.h.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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g l) ≤ (partialSups fun k => Complex.abs (g k)) b

State before:
case h.h.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
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g l) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
exact le_partialSups_of_le (fun k ↦ abs (g k)) lb
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : (fun n => (f' d c)^[n] c) = g
n : ℕ
⊢ (f' d c)^[n] c = g n
Tactic:
rw [← hg]
State after:
no goals

State before:
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 ≤ b, g n = g k
Tactic:
intro n
State after:
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 ≤ b, g n = g k

State before:
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 ≤ b, g n = g k
Tactic:
induction' n with n h
State after:
case zero
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
⊢ ∃ k ≤ b, g 0 = g k

case succ
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 : ℕ
h : ∃ k ≤ b, g n = g k
⊢ ∃ k ≤ b, g (n + 1) = g k

State before:
case zero
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
⊢ ∃ k ≤ b, g 0 = g k
Tactic:
use 0, Nat.zero_le _
State after:
no goals

State before:
case succ
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 : ℕ
h : ∃ k ≤ b, g n = g k
⊢ ∃ k ≤ b, g (n + 1) = g k
Tactic:
rcases h with ⟨k, kb, nk⟩
State after:
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

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

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

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

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

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