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

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

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

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

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

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