Theorem: Eqn.potential (Ray/Dynamics/Grow.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
⊢ s.potential x.1 (r x.1 x.2) = Complex.abs x.2
Tactic:
simp only [s.potential_eq e.near, Super.potential', e.eqn, Complex.abs.map_pow, ← Nat.cast_pow,
  Real.pow_rpow_inv_natCast (Complex.abs.nonneg _) (pow_ne_zero _ s.d0)]
State after:
no goals