Theorem: Super.potential_eq (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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
⊢ s.potential c z = s.potential' c z k
Tactic:
have h : ∃ k, (c, (f c)^[k] z) ∈ s.near := ⟨k,ks⟩
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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential c z = s.potential' c z k

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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential c z = s.potential' c z k
Tactic:
simp only [Super.potential, h, dif_pos]
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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential' c z (Nat.find ⋯) = s.potential' c z k

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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential' c z (Nat.find ⋯) = s.potential' c z k
Tactic:
exact s.potential_eq' (Nat.find_spec h) ks
State after:
no goals