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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ 0 ≤ potential d c
Tactic:
induction c using OnePoint.rec
State after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 ≤ potential d ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ potential d ↑x✝

State before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 ≤ potential d ∞
Tactic:
simp only [potential, fill_inf, le_refl]
State after:
no goals

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ potential d ↑x✝
Tactic:
simp only [potential, fill_coe]
State after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ ⋯.potential x✝ ↑x✝

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ ⋯.potential x✝ ↑x✝
Tactic:
exact (superF d).potential_nonneg
State after:
no goals