Theorem: VehicleSpeedSched.aₚdₚ2_nonneg (CvxLean/Examples/VehicleSpeedScheduling.lean)

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ aₚ • dₚ ^ 2
Tactic:
intros i
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i ≤ (aₚ • dₚ ^ 2) i

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i ≤ (aₚ • dₚ ^ 2) i
Tactic:
fin_cases i <;> (dsimp [aₚ, 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, ⋯⟩ ≤ (aₚ • dₚ ^ 2) ⟨9, ⋯⟩
Tactic:
dsimp [aₚ, 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 * ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩ ^ 2

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