internlm/Lean-Github huggingface dataset:
Theorem: multibrot_basin
Proof 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
Proof 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
Theorem: multibrot_basin
Proof 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]
Proof state after:
no goals
Theorem: multibrot_basin
Proof 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]
Proof state after:
no goals
Theorem: multibrot_basin
Proof 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⟩
Proof 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
Theorem: multibrot_basin
Proof 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⟩
Proof state after:
no goals
Theorem: multibrot_basin
Proof 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⟩
Proof 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
Theorem: multibrot_basin
Proof 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
Proof 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
Theorem: multibrot_basin
Proof 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']
Proof 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
Theorem: multibrot_basin
Proof 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
Proof state after:
no goals
Theorem: multibrot_p
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ⋯.p c = ⋯.potential c 0
Tactic:
set s := superF d
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ s.p c = s.potential c 0
Theorem: multibrot_p
Proof 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]
Proof 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
Theorem: multibrot_p
Proof 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
Proof state after:
no goals
Theorem: multibrot_p
Proof 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
Proof 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}
Theorem: multibrot_p
Proof 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
Proof 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}
Theorem: multibrot_p
Proof 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]
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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⟩
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof 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
Theorem: multibrot_p
Proof 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
Proof state after:
no goals
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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
Proof 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 = ∞)
Theorem: multibrot_p
Proof 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]
Proof 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 ≠ ∞
Theorem: multibrot_p
Proof 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
Proof state after:
no goals
Theorem: multibrot_p
Proof 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
Proof state after:
no goals
Theorem: multibrotPost
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
⊢ Postcritical ⋯ c ↑c
Tactic:
set s := superF d
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ Postcritical s c ↑c
Theorem: multibrotPost
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ Postcritical s c ↑c
Tactic:
simp only [Postcritical, multibrot_p, ← f_0 d, s.potential_eqn]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ s.potential c 0 ^ d < ⋯.potential c 0
Theorem: multibrotPost
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ s.potential c 0 ^ d < ⋯.potential c 0
Tactic:
simp only [multibrot_basin, not_not] at m
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : (c, 0) ∈ ⋯.basin
⊢ s.potential c 0 ^ d < ⋯.potential c 0
Theorem: multibrotPost
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : (c, 0) ∈ ⋯.basin
⊢ s.potential c 0 ^ d < ⋯.potential c 0
Tactic:
exact pow_lt_self_of_lt_one ((s.potential_pos c).mpr inf_ne_zero.symm)
  (s.potential_lt_one m) (d_gt_one d)
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
induction' n with n h
Proof state after:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (b - 1) ^ 0 * Complex.abs z ≤ Complex.abs ((f' d c)^[0] z)

case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs ((f' d c)^[n + 1] z)
Theorem: iter_large
Proof state before:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (b - 1) ^ 0 * Complex.abs z ≤ Complex.abs ((f' d c)^[0] z)
Tactic:
simp only [Nat.zero_eq, pow_zero, one_mul, Function.iterate_zero_apply, le_refl]
Proof state after:
no goals
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs ((f' d c)^[n + 1] z)
Tactic:
simp only [Function.iterate_succ_apply']
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c ((f' d c)^[n] z))
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c ((f' d c)^[n] z))
Tactic:
generalize hw : (f' d c)^[n] z = w
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
w : ℂ
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
w : ℂ
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
rw [hw] at h
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
clear hw
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have z1 : 1 ≤ abs z := le_trans (by norm_num) (le_trans b2 bz)
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have b1 : 1 ≤ b - 1 := by linarith
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have b0 : 0 ≤ b - 1 := by linarith
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)