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

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

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

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

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ potential d ↑x✝ = 0 ↔ ↑x✝ = ∞
Tactic:
simp only [potential, fill_coe, (superF d).potential_eq_zero_of_onePreimage]
State after:
no goals