ι : Type u_2
ι' : Type ?u.96374
E : Type u_1
F : Type ?u.96380
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
A : Set E →+ Set E :=
  { toZeroHom := { toFun := ↑(convexHull ℝ).toOrderHom, map_zero' := (_ : ↑(convexHull ℝ).toOrderHom {0} = {0}) },
    map_add' :=
      (_ :
        ∀ (s t : Set E),
          ↑(convexHull ℝ).toOrderHom (s + t) = ↑(convexHull ℝ).toOrderHom s + ↑(convexHull ℝ).toOrderHom t) }
⊢ parallelepiped v = ↑(convexHull ℝ).toOrderHom (∑ i : ι, {0, v i})
ι : Type u_2
ι' : Type ?u.96374
E : Type u_1
F : Type ?u.96380
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ parallelepiped v = ↑(convexHull ℝ).toOrderHom (∑ i : ι, {0, v i})
let A : Set E →+ Set E :=
  { toFun := convexHull ℝ
    map_zero' := convexHull_singleton _
    map_add' := convexHull_add }
ι : Type u_2
ι' : Type ?u.96374
E : Type u_1
F : Type ?u.96380
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
A : Set E →+ Set E :=
  { toZeroHom := { toFun := ↑(convexHull ℝ).toOrderHom, map_zero' := (_ : ↑(convexHull ℝ).toOrderHom {0} = {0}) },
    map_add' :=
      (_ :
        ∀ (s t : Set E),
          ↑(convexHull ℝ).toOrderHom (s + t) = ↑(convexHull ℝ).toOrderHom s + ↑(convexHull ℝ).toOrderHom t) }
⊢ ∑ x : ι, ↑(convexHull ℝ).toOrderHom {0, v x} = ↑(convexHull ℝ).toOrderHom (∑ i : ι, {0, v i})
ι : Type u_2
ι' : Type ?u.96374
E : Type u_1
F : Type ?u.96380
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
A : Set E →+ Set E :=
  { toZeroHom := { toFun := ↑(convexHull ℝ).toOrderHom, map_zero' := (_ : ↑(convexHull ℝ).toOrderHom {0} = {0}) },
    map_add' :=
      (_ :
        ∀ (s t : Set E),
          ↑(convexHull ℝ).toOrderHom (s + t) = ↑(convexHull ℝ).toOrderHom s + ↑(convexHull ℝ).toOrderHom t) }
⊢ parallelepiped v = ↑(convexHull ℝ).toOrderHom (∑ i : ι, {0, v i})
simp_rw [parallelepiped_eq_sum_segment, ← convexHull_pair]
no goals
ι : Type u_2
ι' : Type ?u.96374
E : Type u_1
F : Type ?u.96380
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
A : Set E →+ Set E :=
  { toZeroHom := { toFun := ↑(convexHull ℝ).toOrderHom, map_zero' := (_ : ↑(convexHull ℝ).toOrderHom {0} = {0}) },
    map_add' :=
      (_ :
        ∀ (s t : Set E),
          ↑(convexHull ℝ).toOrderHom (s + t) = ↑(convexHull ℝ).toOrderHom s + ↑(convexHull ℝ).toOrderHom t) }
⊢ ∑ x : ι, ↑(convexHull ℝ).toOrderHom {0, v x} = ↑(convexHull ℝ).toOrderHom (∑ i : ι, {0, v i})
exact (A.map_sum _ _).symm