refine' ⟨{t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, fun t ht => ht.1, _⟩
case mp.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ ∃ F ⊆ K₁.faces, combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
case mp.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
⊢ combiInterior ℝ s = ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁