Theorem: Finset.empty_posDiffs (LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean)

State before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ ∅ \₊ s = ∅
Tactic:
simp [posDiffs]
State after:
no goals