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

State before:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a x : α
⊢ x ∈ s -₊ t → x ∈ s - t
Tactic:
rw [mem_posSub, mem_sub]
State after:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a x : α
⊢ (∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = x) → ∃ b ∈ s, ∃ c ∈ t, b - c = x

State before:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a x : α
⊢ (∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = x) → ∃ b ∈ s, ∃ c ∈ t, b - c = x
Tactic:
exact fun ⟨b, hb, c, hc, _, h⟩ ↦ ⟨b, hb, c, hc, h⟩
State after:
no goals