Theorem: VehicleSpeedSched.sminₚ_le_smaxₚ (CvxLean/Examples/VehicleSpeedScheduling.lean)

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

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ sminₚ i ≤ smaxₚ i
Tactic:
fin_cases i <;> (dsimp [sminₚ, smaxₚ]; 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 : ℝ → ℝ
⊢ sminₚ ⟨9, ⋯⟩ ≤ smaxₚ ⟨9, ⋯⟩
Tactic:
dsimp [sminₚ, smaxₚ]
State after:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405] ⟨9, ⋯⟩ ≤
    ![1.9624, 1.6036, 1.6439, 1.5641, 1.7194, 1.9090, 1.3193, 1.3366, 1.9470, 2.8803] ⟨9, ⋯⟩

State before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405] ⟨9, ⋯⟩ ≤
    ![1.9624, 1.6036, 1.6439, 1.5641, 1.7194, 1.9090, 1.3193, 1.3366, 1.9470, 2.8803] ⟨9, ⋯⟩
Tactic:
norm_num
State after:
no goals