Theorem: Super.nice_np (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
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ s.IsNiceN c p (s.np c p)
Tactic:
have q : p < 1 ∧ OnePreimage s := ⟨p1, op⟩
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
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (s.np c p)

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
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (s.np c p)
Tactic:
simp only [Super.np, q, true_and_iff, 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
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (Nat.find ⋯)

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
c : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (Nat.find ⋯)
Tactic:
exact Nat.find_spec (s.has_nice_n c p1)
State after:
no goals