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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ c ∈ multibrot d ↔ (c, 0) ∉ ⋯.basin
Tactic:
set s := superF d
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ c ∈ multibrot d ↔ (c, 0) ∉ s.basin

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ c ∈ multibrot d ↔ (c, 0) ∉ s.basin
Tactic:
simp only [multibrot_basin', not_iff_not, Super.basin, mem_setOf]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (∃ n, (c, (f d c)^[n] ↑c) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n] ↑c) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Tactic:
simp only [e]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) ↔ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Tactic:
constructor
State after:
case mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) → ∃ n, (c, (f d c)^[n] 0) ∈ s.near

case mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n] 0) ∈ s.near) → ∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
Tactic:
intro n
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
n : ℕ
⊢ (f d c)^[n] ↑c = (f d c)^[n + 1] 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
n : ℕ
⊢ (f d c)^[n] ↑c = (f d c)^[n + 1] 0
Tactic:
induction' n with n h
State after:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (f d c)^[0] ↑c = (f d c)^[0 + 1] 0

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
n : ℕ
h : (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (f d c)^[n + 1] ↑c = (f d c)^[n + 1 + 1] 0

State before:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (f d c)^[0] ↑c = (f d c)^[0 + 1] 0
Tactic:
simp only [Function.iterate_zero_apply, zero_add, Function.iterate_one, f_0, Nat.zero_eq]
State after:
no goals

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
n : ℕ
h : (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (f d c)^[n + 1] ↑c = (f d c)^[n + 1 + 1] 0
Tactic:
simp only [Function.iterate_succ_apply', h]
State after:
no goals

State before:
case mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near) → ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Tactic:
intro ⟨n, h⟩
State after:
case mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n + 1] 0) ∈ ⋯.near
⊢ ∃ n, (c, (f d c)^[n] 0) ∈ s.near

State before:
case mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n + 1] 0) ∈ ⋯.near
⊢ ∃ n, (c, (f d c)^[n] 0) ∈ s.near
Tactic:
exact ⟨n + 1, h⟩
State after:
no goals

State before:
case mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
⊢ (∃ n, (c, (f d c)^[n] 0) ∈ s.near) → ∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near
Tactic:
intro ⟨n, h⟩
State after:
case mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n] 0) ∈ s.near
⊢ ∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near

State before:
case mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n] 0) ∈ s.near
⊢ ∃ n, (c, (f d c)^[n + 1] 0) ∈ ⋯.near
Tactic:
use n
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n] 0) ∈ s.near
⊢ (c, (f d c)^[n + 1] 0) ∈ ⋯.near

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n] 0) ∈ s.near
⊢ (c, (f d c)^[n + 1] 0) ∈ ⋯.near
Tactic:
simp only [Function.iterate_succ_apply']
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n] 0) ∈ s.near
⊢ (c, f d c ((f d c)^[n] 0)) ∈ ⋯.near

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : ∀ (n : ℕ), (f d c)^[n] ↑c = (f d c)^[n + 1] 0
n : ℕ
h : (c, (f d c)^[n] 0) ∈ s.near
⊢ (c, f d c ((f d c)^[n] 0)) ∈ ⋯.near
Tactic:
exact s.stays_near h
State after:
no goals