simp_rw [Set.mem_iUnion]
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊂ s), (convexHull ℝ) ↑t → x ∈ frontier ((convexHull ℝ) ↑s)
case h.mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
x : E
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull ℝ) ↑i) → x ∈ frontier ((convexHull ℝ) ↑s)