obtain ⟨u, hu, htu⟩ := (not_facet_iff_subface ht).mp htfacet
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1