α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t
rw [← sep_eq_of_subset h]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
infer_instance