Theorem: VehicleSpeedSched.fold_partial_sum (CvxLean/Examples/VehicleSpeedScheduling.lean)

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
⊢ ∑ j ∈ [[0, i]], t j = Vec.cumsum t i
Tactic:
simp [Vec.cumsum]
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
⊢ ∑ j ∈ [[0, i]], t j = if h : 0 < n then ∑ j ∈ [[⟨0, h⟩, i]], t j else 0

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
⊢ ∑ j ∈ [[0, i]], t j = if h : 0 < n then ∑ j ∈ [[⟨0, h⟩, i]], t j else 0
Tactic:
split_ifs
State after:
case pos
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : 0 < n
⊢ ∑ j ∈ [[0, i]], t j = ∑ j ∈ [[⟨0, h✝⟩, i]], t j

case neg
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : ¬0 < n
⊢ ∑ j ∈ [[0, i]], t j = 0

State before:
case pos
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : 0 < n
⊢ ∑ j ∈ [[0, i]], t j = ∑ j ∈ [[⟨0, h✝⟩, i]], t j
Tactic:
rfl
State after:
no goals

State before:
case neg
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : ¬0 < n
⊢ ∑ j ∈ [[0, i]], t j = 0
Tactic:
linarith [hn.out]
State after:
no goals