refine' Set.iUnion₂_mono' fun t hts => _
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
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
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
t : Finset E
hts : t ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'