exact this.subset fun i h => h.1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T2Space E
s t : Finset E
this : {t | t ⊆ s}.Finite
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t
no goals