rw [card_singleton]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ {x}.card ≤ k + 1
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ 1 ≤ k + 1