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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ Complex.abs (bottcher d c) = potential d c
Tactic:
set s := superF d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d c) = potential d c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d c) = potential d c
Tactic:
induction c using OnePoint.rec
State after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d ∞) = potential d ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher d ↑x✝) = potential d ↑x✝

State before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d ∞) = potential d ∞
Tactic:
simp only [bottcher, potential, fill_inf, Complex.abs.map_zero]
State after:
no goals

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher d ↑x✝) = potential d ↑x✝
Tactic:
simp only [bottcher, potential, fill_coe]
State after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher' d x✝) = ⋯.potential x✝ ↑x✝

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher' d x✝) = ⋯.potential x✝ ↑x✝
Tactic:
exact s.abs_bottcher
State after:
no goals