Theorem: Super.potential_eqn (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
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
by_cases a : ∃ n, (c, (f c)^[n] z) ∈ s.near
State after:
case pos
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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d

case neg
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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d

State before:
case pos
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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
rcases a with ⟨n, a⟩
State after:
case pos.intro
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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d

State before:
case pos.intro
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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
have a' : (c, (f c)^[n] (f c z)) ∈ s.near := by
  simp only [← Function.iterate_succ_apply, Function.iterate_succ', s.stays_near a,
    Function.comp]
State after:
case pos.intro
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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
a' : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d

State before:
case pos.intro
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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
a' : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
simp only [s.potential_eq a, s.potential_eq a', Super.potential', ← Function.iterate_succ_apply,
  Function.iterate_succ', s.bottcherNear_eqn a, Complex.abs.map_pow, ← Real.rpow_natCast, ←
  Real.rpow_mul (Complex.abs.nonneg _), mul_comm, Function.comp]
State after:
no goals

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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n] (f c z)) ∈ s.near
Tactic:
simp only [← Function.iterate_succ_apply, Function.iterate_succ', s.stays_near a,
  Function.comp]
State after:
no goals

State before:
case neg
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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
have a' : ∀ n, (c, (f c)^[n] (f c z)) ∉ s.near := by
  contrapose a; simp only [not_forall, not_not, ← Function.iterate_succ_apply] at a ⊢
  rcases a with ⟨n, a⟩; exact ⟨n + 1, a⟩
State after:
case neg
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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
a' : ∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d

State before:
case neg
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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
a' : ∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
simp only [s.potential_eq_one (not_exists.mp a), s.potential_eq_one a', one_pow]
State after:
no goals

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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
Tactic:
contrapose a
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✝
a : ¬∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ ¬¬∃ n, (c, (f c)^[n] z) ∈ s.near

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✝
a : ¬∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ ¬¬∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
simp only [not_forall, not_not, ← Function.iterate_succ_apply] at a ⊢
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✝
a : ∃ x, (c, (f c)^[x.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near

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✝
a : ∃ x, (c, (f c)^[x.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
rcases a with ⟨n, a⟩
State after:
case intro
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 : ℕ
a : (c, (f c)^[n.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near

State before:
case intro
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 : ℕ
a : (c, (f c)^[n.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
exact ⟨n + 1, a⟩
State after:
no goals