no goals
ι : Sort ?u.12394
𝕜 : Type u_2
E : Type u_1
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s✝ t✝ s₁ s₂ t₁ t₂ u : Set E
x y : E
s t : Set E
⊢ (⋃ (i₂ : E) (_ : i₂ ∈ t) (i₁ : E) (_ : i₁ ∈ s), segment 𝕜 i₁ i₂) = convexJoin 𝕜 t s
simp_rw [convexJoin, segment_symm]