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

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
⊢ d i / (d i / s i) = s i
Tactic:
have h_di_pos := h_d_pos i
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 i < d i
⊢ d i / (d i / s i) = s i

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 i < d i
⊢ d i / (d i / s i) = s i
Tactic:
simp at h_di_pos
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
⊢ d i / (d i / s i) = s i

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
⊢ d i / (d i / s i) = s i
Tactic:
have h_di_nonzero : d i ≠ 0 := by linarith
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
h_di_nonzero : d i ≠ 0
⊢ d i / (d i / s i) = s i

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
h_di_nonzero : d i ≠ 0
⊢ d i / (d i / s i) = s i
Tactic:
rw [← div_mul, div_self h_di_nonzero, one_mul]
State after:
no goals

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
⊢ d i ≠ 0
Tactic:
linarith
State after:
no goals