have hspace : K₁.space = K₂.space := by
  refine' hspace.antisymm fun x hx => _
  rw [← combiInteriors_cover, mem_iUnion₂] at hx ⊢
  obtain ⟨s, hs, hxs⟩ := hx
  obtain ⟨F, hF, hsint⟩ := hpartition _ hs
  rw [hsint, mem_iUnion₂] at hxs
  obtain ⟨t, ht, hxt⟩ := hxs
  exact ⟨t, hF ht, hxt⟩
case mpr.intro.intro
𝕜 : 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
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ K₁.Subdivides K₂
case mpr.intro.intro
𝕜 : 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
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
⊢ K₁.Subdivides K₂