Theorem: Super.abs_bottcherNear (Ray/Dynamics/Potential.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✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[n] z)) = s.potential c z ^ d ^ n
Tactic:
simp only [s.potential_eq r, Super.potential']
State after:
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✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[n] z)) = (Complex.abs (s.bottcherNear c ((f c)^[n] z)) ^ (↑d ^ n)⁻¹) ^ d ^ n

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✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[n] z)) = (Complex.abs (s.bottcherNear c ((f c)^[n] z)) ^ (↑d ^ n)⁻¹) ^ d ^ n
Tactic:
rw [← Real.rpow_natCast, ← Real.rpow_mul (Complex.abs.nonneg _), Nat.cast_pow, inv_mul_cancel,
  Real.rpow_one]
State after:
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✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ↑d ^ n ≠ 0

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✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ↑d ^ n ≠ 0
Tactic:
exact pow_ne_zero _ (Nat.cast_ne_zero.mpr s.d0)
State after:
no goals