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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (multibrot d)
Tactic:
refine IsCompact.of_isClosed_subset (isCompact_closedBall _ _) ?_ multibrot_subset_closedBall
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (multibrot d)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (multibrot d)
Tactic:
rw [multibrot_eq_le_two]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)
Tactic:
apply isClosed_iInter
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (i : ℕ), IsClosed ((fun c => (f' d c)^[i] c) ⁻¹' closedBall 0 2)

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (i : ℕ), IsClosed ((fun c => (f' d c)^[i] c) ⁻¹' closedBall 0 2)
Tactic:
intro n
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ IsClosed ((fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ IsClosed ((fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)
Tactic:
refine IsClosed.preimage ?_ Metric.isClosed_ball
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ Continuous fun c => (f' d c)^[n] c

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ Continuous fun c => (f' d c)^[n] c
Tactic:
induction' n with n h
State after:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => (f' d c)^[0] c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c

State before:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => (f' d c)^[0] c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Tactic:
simp only [Function.iterate_zero_apply]
State after:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c

State before:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Tactic:
exact continuous_id
State after:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c

State before:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Tactic:
simp only [Function.iterate_succ_apply']
State after:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => f' d c ((f' d c)^[n] c)

State before:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => f' d c ((f' d c)^[n] c)
Tactic:
rw [continuous_iff_continuousAt]
State after:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ ∀ (x : ℂ), ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) x

State before:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ ∀ (x : ℂ), ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) x
Tactic:
intro c
State after:
case h.succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
c : ℂ
⊢ ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) c

State before:
case h.succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
c : ℂ
⊢ ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) c
Tactic:
exact (analytic_f' _ (mem_univ _)).continuousAt.comp₂ continuousAt_id h.continuousAt
State after:
no goals