Theorem: Super.np_mono (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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
⊢ s.np c p0 ≤ s.np c p1
Tactic:
have p01 : p0 < 1 := lt_of_le_of_lt le p11
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
⊢ s.np c p0 ≤ s.np c p1

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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
⊢ s.np c p0 ≤ s.np c p1
Tactic:
have e : s.np c p0 = Nat.find (s.has_nice_n c p01) := by
  simp only [Super.np, p01, op, 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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.np c p0 ≤ s.np c p1

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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.np c p0 ≤ s.np c p1
Tactic:
rw [e]
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ Nat.find ⋯ ≤ s.np c p1

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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ Nat.find ⋯ ≤ s.np c p1
Tactic:
apply Nat.find_min'
State after:
case h
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.IsNiceN c p0 (s.np c p1)

State before:
case h
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.IsNiceN c p0 (s.np c p1)
Tactic:
exact fun z zp ↦ s.nice_np c p11 _ (_root_.trans zp le)
State after:
no goals

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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
⊢ s.np c p0 = Nat.find ⋯
Tactic:
simp only [Super.np, p01, op, true_and_iff, dif_pos]
State after:
no goals