Theorem: Super.potential_eq_zero_of_onePreimage (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
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z = 0 ↔ z = a
Tactic:
constructor
State after:
case mp
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
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z = 0 → z = a

case mpr
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
inst✝ : OnePreimage s
c : ℂ
⊢ z = a → s.potential c z = 0

State before:
case mp
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
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z = 0 → z = a
Tactic:
intro h
State after:
case mp
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
inst✝ : OnePreimage s
c : ℂ
h : s.potential c z = 0
⊢ z = a

State before:
case mp
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
inst✝ : OnePreimage s
c : ℂ
h : s.potential c z = 0
⊢ z = a
Tactic:
rw [s.potential_eq_zero] at h
State after:
case mp
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
inst✝ : OnePreimage s
c : ℂ
h : ∃ n, (f c)^[n] z = a
⊢ z = a

State before:
case mp
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
inst✝ : OnePreimage s
c : ℂ
h : ∃ n, (f c)^[n] z = a
⊢ z = a
Tactic:
rcases h with ⟨n, h⟩
State after:
case mp.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
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : (f c)^[n] z = a
⊢ z = a

State before:
case mp.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
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : (f c)^[n] z = a
⊢ z = a
Tactic:
rw [s.preimage_eq] at h
State after:
case mp.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
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : z = a
⊢ z = a

State before:
case mp.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
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : z = a
⊢ z = a
Tactic:
exact h
State after:
no goals

State before:
case mpr
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
inst✝ : OnePreimage s
c : ℂ
⊢ z = a → s.potential c z = 0
Tactic:
intro h
State after:
case mpr
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
inst✝ : OnePreimage s
c : ℂ
h : z = a
⊢ s.potential c z = 0

State before:
case mpr
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
inst✝ : OnePreimage s
c : ℂ
h : z = a
⊢ s.potential c z = 0
Tactic:
simp only [h, s.potential_a]
State after:
no goals