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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ⋯.p c = ⋯.potential c 0
Tactic:
set s := superF d
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ s.p c = s.potential c 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : s.ps c = {1, s.potential c 0}
⊢ s.p c = s.potential c 0
Tactic:
simp only [Super.p, e, csInf_pair]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : s.ps c = {1, s.potential c 0}
⊢ 1 ⊓ s.potential c 0 = s.potential c 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : s.ps c = {1, s.potential c 0}
⊢ 1 ⊓ s.potential c 0 = s.potential c 0
Tactic:
exact inf_of_le_right s.potential_le_one
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ s.ps c = {1, s.potential c 0}
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (x : ℝ), x ∈ s.ps c ↔ x ∈ {1, s.potential c 0}

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (x : ℝ), x ∈ s.ps c ↔ x ∈ {1, s.potential c 0}
Tactic:
intro p
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ p ∈ s.ps c ↔ p ∈ {1, s.potential c 0}

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ p ∈ s.ps c ↔ p ∈ {1, s.potential c 0}
Tactic:
simp only [Super.ps, mem_singleton_iff, mem_setOf, critical_f, Ne, mem_insert_iff,
  mem_singleton_iff]
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)) ↔ p = 1 ∨ p = s.potential c 0

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)) ↔ p = 1 ∨ p = s.potential c 0
Tactic:
constructor
State after:
case h.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)) → p = 1 ∨ p = s.potential c 0

case h.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ p = 1 ∨ p = s.potential c 0 → p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)) → p = 1 ∨ p = s.potential c 0
Tactic:
intro h
State after:
case h.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0

State before:
case h.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0
Tactic:
cases' h with h h
State after:
case h.mp.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1 ∨ p = s.potential c 0

case h.mp.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0

State before:
case h.mp.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1 ∨ p = s.potential c 0

case h.mp.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0
Tactic:
left
State after:
case h.mp.inl.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1

case h.mp.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0

State before:
case h.mp.inl.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1

case h.mp.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0
Tactic:
exact h
State after:
case h.mp.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0

State before:
case h.mp.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = 1 ∨ p = s.potential c 0
Tactic:
right
State after:
case h.mp.inr.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = s.potential c 0

State before:
case h.mp.inr.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
⊢ p = s.potential c 0
Tactic:
rcases h with ⟨p0, z, e, h⟩
State after:
case h.mp.inr.h.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = 0 ∨ z = ∞
⊢ p = s.potential c 0

State before:
case h.mp.inr.h.intro.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = 0 ∨ z = ∞
⊢ p = s.potential c 0
Tactic:
cases' h with h h
State after:
case h.mp.inr.h.intro.intro.intro.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = 0
⊢ p = s.potential c 0

case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = ∞
⊢ p = s.potential c 0

State before:
case h.mp.inr.h.intro.intro.intro.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = 0
⊢ p = s.potential c 0

case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = ∞
⊢ p = s.potential c 0
Tactic:
rw [h] at e
State after:
case h.mp.inr.h.intro.intro.intro.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c 0 = p
h : z = 0
⊢ p = s.potential c 0

case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = ∞
⊢ p = s.potential c 0

State before:
case h.mp.inr.h.intro.intro.intro.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c 0 = p
h : z = 0
⊢ p = s.potential c 0

case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = ∞
⊢ p = s.potential c 0
Tactic:
exact e.symm
State after:
case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = ∞
⊢ p = s.potential c 0

State before:
case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : s.potential c z = p
h : z = ∞
⊢ p = s.potential c 0
Tactic:
rw [h, s.potential_a] at e
State after:
case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : 0 = p
h : z = ∞
⊢ p = s.potential c 0

State before:
case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : 0 = p
h : z = ∞
⊢ p = s.potential c 0
Tactic:
exfalso
State after:
case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : 0 = p
h : z = ∞
⊢ False

State before:
case h.mp.inr.h.intro.intro.intro.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
p0 : ¬p = 0
z : 𝕊
e : 0 = p
h : z = ∞
⊢ False
Tactic:
exact p0 e.symm
State after:
no goals

State before:
case h.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
⊢ p = 1 ∨ p = s.potential c 0 → p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
intro h
State after:
case h.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1 ∨ p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1 ∨ p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
cases' h with h h
State after:
case h.mpr.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

case h.mpr.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mpr.inl
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

case h.mpr.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
left
State after:
case h.mpr.inl.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1

case h.mpr.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mpr.inl.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = 1
⊢ p = 1

case h.mpr.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
exact h
State after:
case h.mpr.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mpr.inr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
right
State after:
case h.mpr.inr.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mpr.inr.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
constructor
State after:
case h.mpr.inr.h.left
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ ¬p = 0

case h.mpr.inr.h.right
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)

State before:
case h.mpr.inr.h.left
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ ¬p = 0
Tactic:
simp only [h, ← ne_eq, s.potential_ne_zero]
State after:
case h.mpr.inr.h.left
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ 0 ≠ ∞

State before:
case h.mpr.inr.h.left
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ 0 ≠ ∞
Tactic:
exact inf_ne_zero.symm
State after:
no goals

State before:
case h.mpr.inr.h.right
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
p : ℝ
h : p = s.potential c 0
⊢ ∃ z, s.potential c z = p ∧ (z = 0 ∨ z = ∞)
Tactic:
use 0, h.symm, Or.inl rfl
State after:
no goals