rw [combiInterior_empty]
case refine'_2.inl
𝕜 : 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
hts : ∅ ⊆ s
⊢ combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 s
case refine'_2.inl
𝕜 : 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
hts : ∅ ⊆ s
⊢ ∅ ⊆ combiInterior 𝕜 s