Theorem: Finset.posDiffs_subset_diffs (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 \₊ t ⊆ s \\ t
Tactic:
simp only [subset_iff, mem_posDiffs, mem_diffs]
State after:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
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) → ∃ a ∈ s, ∃ b ∈ t, a \ b = x

State before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
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) → ∃ a ∈ s, ∃ b ∈ t, a \ b = x
Tactic:
exact fun a ⟨b, hb, c, hc, _, ha⟩ ↦ ⟨b, hb, c, hc, ha⟩
State after:
no goals