Theorem: Barrier.mem_fast (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
⊢ (e, z) ∈ b.fast m ↔ ∃ n < m, (e, (f e)^[n] z) ∈ t
Tactic:
simp only [Barrier.fast, Set.mem_iUnion, Set.mem_preimage]
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
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) ↔ ∃ n < m, (e, (f e)^[n] z) ∈ t

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
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) ↔ ∃ n < m, (e, (f e)^[n] z) ∈ t
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) → ∃ n < m, (e, (f e)^[n] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) → ∃ n < m, (e, (f e)^[n] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
h : ∃ i, (e, (f e)^[↑i] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
h : ∃ i, (e, (f e)^[↑i] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m : ℕ
e : ℂ
z : S
n : Fin m
h : (e, (f e)^[↑n] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t

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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m : ℕ
e : ℂ
z : S
n : Fin m
h : (e, (f e)^[↑n] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
use n, Fin.is_lt _, 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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
h : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t

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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
e : ℂ
z : S
h : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
rcases h with ⟨n, nm, h⟩
State after:
case mpr.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 : ℕ
nm : n < m
h : (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t

State before:
case mpr.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 : ℕ
nm : n < m
h : (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
use⟨n, nm⟩, h
State after:
no goals