simp_rw [posSub, mem_image, mem_filter, mem_product, Prod.exists, and_assoc, exists_and_left]
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s -₊ t ↔ ∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = a
no goals