no goals
ι : Type u_2
ι' : Type ?u.4165
E : Type u_1
F : Type ?u.4171
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
x : E
⊢ x ∈ parallelepiped v ↔ ∃ t _ht, x = ∑ i : ι, t i • v i
simp [parallelepiped, eq_comm]