Theorem: VehicleSpeedSched.dₚ_pos (CvxLean/Examples/VehicleSpeedScheduling.lean)

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ StrongLT 0 dₚ
Tactic:
intro i
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < dₚ i

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < dₚ i
Tactic:
fin_cases i <;> (dsimp [dₚ]; norm_num)
State after:
no goals

State before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ⟨9, ⋯⟩ < dₚ ⟨9, ⋯⟩
Tactic:
dsimp [dₚ]
State after:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩

State before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩
Tactic:
norm_num
State after:
no goals