Theorem: Barrier.fast_reaches (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 t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
q : (e, z) ∈ b.fast m
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Tactic:
rw [b.mem_fast] at q
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 t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
q : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
q : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Tactic:
rcases q with ⟨n, _, q⟩
State after:
case intro.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✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m : ℕ
e : ℂ
z : S
n : ℕ
left✝ : n < m
q : (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near

State before:
case intro.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✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m : ℕ
e : ℂ
z : S
n : ℕ
left✝ : n < m
q : (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Tactic:
exact ⟨n, b.near q⟩
State after:
no goals