refine' (Set.iUnion₂_mono fun _ _ => _).antisymm (Set.iUnion₂_subset fun s hs => _)
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
x✝¹ : Finset E
x✝ : x✝¹ ∈ K
⊢ combiInterior 𝕜 x✝¹ ⊆ (convexHull 𝕜) ↑x✝¹

case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ i ∈ K, combiInterior 𝕜 i