ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ (t ∪ u) = t ∪ (s ∪ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ t ∪ u = s ∪ u ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∪ ∅ = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>∅ ∪ s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s.Nonempty<GOAL>(s ∪ t).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : t.Nonempty<GOAL>(s ∪ t).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>insert a s = {a} ∪ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>insert a s ∪ t = insert a (s ∪ t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>s ∪ insert a t = insert a (s ∪ t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>insert a (s ∪ t) = insert a s ∪ insert a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t = s ↔ t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s = s ∪ t ↔ t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t = t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s = t ∪ s ↔ t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>ht : t ⊆ s ∪ u<VAR>hu : u ⊆ s ∪ t<GOAL>s ∪ t = s ∪ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>hs : s ⊆ t ∪ u<VAR>ht : t ⊆ s ∪ u<GOAL>s ∪ u = t ∪ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>P : Finset α → Finset α → Prop<VAR>symm : ∀ {a b : Finset α}, P a b → P b a<VAR>empty_right : ∀ {a : Finset α}, P a ∅<VAR>singletons : ∀ {a b : α}, P {a} {b}<VAR>union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c<VAR>a b : Finset α<GOAL>P a b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>(s₁ ∩ s₂).val = s₁.val.ndinter s₂.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>(s₁ ∩ s₂).val = s₁.val ∩ s₂.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finset α<GOAL>a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finset α<VAR>h : a ∈ s₁ ∩ s₂<GOAL>a ∈ s₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finset α<VAR>h : a ∈ s₁ ∩ s₂<GOAL>a ∈ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finset α<GOAL>a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ ∩ s₂ ⊆ s₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ ∩ s₂ ⊆ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ u : Finset α<GOAL>s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>↑(s₁ ∩ s₂) = ↑s₁ ∩ ↑s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t) ∩ s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t) ∩ t = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ ∩ s₂ = s₂ ∩ s₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : Finset α<GOAL>s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : Finset α<GOAL>s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : Finset α<GOAL>s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∩ s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∩ ∅ = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>∅ ∩ s = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∩ (t ∪ s) = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∈ s₂<GOAL>insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∈ s₁<GOAL>s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∉ s₂<GOAL>insert a s₁ ∩ s₂ = s₁ ∩ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∉ s₁<GOAL>s₁ ∩ insert a s₂ = s₁ ∩ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>H : a ∈ s<GOAL>{a} ∩ s = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>H : a ∉ s<GOAL>{a} ∩ s = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∈ s<GOAL>s ∩ {a} = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>s ∩ {a} = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y s t : Finset α<VAR>h : x ⊆ y<VAR>h' : s ⊆ t<GOAL>x ∩ s ⊆ y ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>h : t ⊆ u<GOAL>s ∩ t ⊆ s ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>h : s ⊆ t<GOAL>s ∩ u ⊆ t ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∩ t ⊆ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ (s ∪ t) = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t ∪ t = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∩ (s ∩ t) = s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∩ t ∩ t = s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u v : Finset α<GOAL>s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u v : Finset α<GOAL>s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∩ t = s ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>t ∩ s = s ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>ht : s ∩ u ⊆ t<VAR>hu : s ∩ t ⊆ u<GOAL>s ∩ t = s ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>hs : t ∩ u ⊆ s<VAR>ht : s ∩ u ⊆ t<GOAL>s ∩ u = t ∩ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s s' : Finset α<VAR>P : Prop<VAR>Decidable P<GOAL>(if P then s else s') ⊆ s ∪ s'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s s' : Finset α<VAR>P : Prop<VAR>Decidable P<GOAL>s ∩ s' ⊆ if P then s else s'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>¬Disjoint s t ↔ (s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Disjoint s t ∨ (s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>(s.erase a).val = s.val.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Finset α<GOAL>a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>a ∉ s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>∅.erase a = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>hs : s.Nontrivial<GOAL>(s.erase a).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>(s.erase a).Nonempty ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a}.erase a = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<GOAL>b ∈ s.erase a → b ≠ a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<GOAL>b ∈ s.erase a → b ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<GOAL>a ≠ b → a ∈ s → a ∈ s.erase b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>hs : b ∈ s<VAR>hsa : b ∉ s.erase a<GOAL>b = a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>s.erase a = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a = s ↔ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>(insert a s).erase a = s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(insert a s).erase a = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Finset α<VAR>h : a ≠ b<GOAL>(insert a s).erase b = insert a (s.erase b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hb : a ≠ b<GOAL>(Finset.cons a s ha).erase b = Finset.cons a (s.erase b) ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>insert a (s.erase a) = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ s<VAR>ht : a ∉ t<GOAL>s.erase a = t ↔ s = insert a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Set.InvOn (insert a) (fun s => s.erase a) {s | a ∈ s} {s | a ∉ s}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>s.erase a ⊆ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>s.erase a ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>s ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>↑(s.erase a) = ↑s \ {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∈ s<GOAL>s.erase a ⊂ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a ⊂ insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a ≠ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>(Finset.cons a s h).erase a = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(s.erase a).erase a = s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Finset α<GOAL>(s.erase a).erase b = (s.erase b).erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>s ⊆ insert a t ↔ s.erase a ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).erase a ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>s ⊆ insert a (s.erase a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ⊆ insert a t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∈ t<GOAL>s.erase a ⊆ t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>s : Finset α<VAR>hx : x ∈ s<GOAL>s.erase x = s.erase y ↔ x = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Set.InjOn s.erase ↑s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Set.InjOn (fun s => s.erase a) {s | a ∈ s}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nontrivial<GOAL>∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), Finset.cons a (Finset.cons b t hb) ⋯ = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>(s₁ \ s₂).val = s₁.val - s₂.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s \ t ↔ a ∈ s ∧ a ∉ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ ∩ (s₂ \ s₁) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∈ t<GOAL>a ∉ s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>a ∉ s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>s ∪ t \ s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>h : s₁ ⊆ s₂<GOAL>s₂ \ s₁ ∪ s₁ = s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>(s ∩ t) \ u = s ∩ (t \ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ∩ (t \ u) = (s ∩ t) \ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₂ \ s₁ ∩ s₁ = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ : Finset α<GOAL>s₁ \ s₁ = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s \ (t ∩ u) = s \ t ∪ s \ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ (s ∩ t) = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ (t ∩ s) = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s \ ∅ = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u v : Finset α<VAR>hst : s ⊆ t<VAR>hvu : v ⊆ u<GOAL>s \ u ⊆ t \ v
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>↑(s₁ \ s₂) = ↑s₁ \ ↑s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t \ s = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ t ∪ t = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t) \ s = t \ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t) \ t = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>(s ∪ t) \ s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>(s ∪ t) \ t = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t \ s = t ∪ s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ t ∪ s ∩ t = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t) \ t = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ t = ∅ ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).Nonempty ↔ ¬s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>∅ \ s = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : Finset α<VAR>x : α<VAR>h : x ∉ t<GOAL>insert x s \ t = insert x (s \ t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>t : Finset α<VAR>s : Finset α<VAR>x : α<VAR>h : x ∈ t<GOAL>insert x s \ t = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>insert a s \ s = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>x : α<GOAL>insert x s \ insert x t = s \ insert x t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>hab : a ≠ b<VAR>ha : a ∉ s<GOAL>insert a s \ insert b s = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>hab : a ≠ b<VAR>hb : b ∈ s<GOAL>s.erase a \ s.erase b = {b}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>hab : a ≠ b<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>Finset.cons a s ha \ Finset.cons b s hb = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>x : α<VAR>h : x ∉ s<VAR>t : Finset α<GOAL>s \ insert x t = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : t ⊆ s<VAR>ht : t.Nonempty<GOAL>s \ t ⊂ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t₁ t₂ : Finset α<GOAL>s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>s \ {a} = s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a = s \ {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ t<GOAL>Disjoint (s.erase a) (insert a t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>Disjoint (insert a s) (t.erase a) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ t<VAR>hst : Disjoint (s.erase a) t<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ s<VAR>hst : Disjoint s (t.erase a)<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>s ∩ t.erase a = (s ∩ t).erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>s.erase a ∩ t = (s ∩ t).erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>s.erase a \ t = (s \ t).erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>insert a s ∪ t = s ∪ insert a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>s.erase a ∩ t = s ∩ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>(s ∪ t).erase a = s.erase a ∪ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>insert a (s ∩ t) = insert a s ∩ insert a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>(s \ t).erase a = s.erase a \ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>t : Finset α<VAR>a : α<VAR>ha : a ∈ t<VAR>s : Finset α<GOAL>s.erase a ∪ t = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>t : Finset α<GOAL>s ∪ t.erase a = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>s \ {a} = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>c : α<VAR>s : Finset α<VAR>hS : s.Nontrivial<GOAL>(s \ {c}).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>(s \ t) \ u = s \ t ∩ (s \ u)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>hts : t ⊆ s<VAR>hut : u ⊆ t<GOAL>s \ t ∪ t \ u = s \ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>hts : t ⊆ s<VAR>ha : a ∈ t<GOAL>s \ t ∪ t.erase a = s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>h : u ⊆ s<GOAL>s \ (t \ u) = s \ t ∪ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>x : α<GOAL>s \ insert x t = (s \ t).erase x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxt : x ∉ t<GOAL>insert x (s \ insert x t) = s \ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>s \ t.erase a = insert a (s \ t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>s \ s.erase a = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ (s \ t) = s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : t ⊆ s<GOAL>s \ (s \ t) = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t₁ t₂ : Finset α<GOAL>s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a = ∅ ↔ s = ∅ ∨ s = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Disjoint (t \ s) s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Disjoint s (t \ s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Disjoint (s \ t) (s ∩ t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ t = s ↔ Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>s \ t = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>↑(symmDiff s t) = symmDiff ↑s ↑t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>symmDiff s t = ∅ ↔ s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(symmDiff s t).Nonempty ↔ s ≠ t
<VAR>α : Type u_1<VAR>SizeOf α<VAR>x : α<VAR>s : Finset α<VAR>hx : x ∈ s<GOAL>sizeOf x < sizeOf s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.attach.val = s.val.attach
<VAR>α : Type u_1<VAR>s : Finset α<VAR>x : { x // x ∈ s }<GOAL>x ∈ s.attach
<VAR>α : Type u_1<GOAL>∅.attach = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.attach.Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.attach = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>(Finset.filter p s).val = Multiset.filter p s.val
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.filter p s ⊆ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ Finset.filter p s ↔ a ∈ s ∧ p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>x : α<VAR>h : x ∈ Finset.filter p s<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.filter p s ⊂ s ↔ ∃ x ∈ s, ¬p x
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>s : Finset α<GOAL>Finset.filter q (Finset.filter p s) = Finset.filter (fun a => p a ∧ q a) s
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>s : Finset α<GOAL>Finset.filter q (Finset.filter p s) = Finset.filter p (Finset.filter q s)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p : α → Prop<VAR>h : DecidablePred p<VAR>DecidablePred p<GOAL>Finset.filter p s = Finset.filter p s
<VAR>α : Type u_1<VAR>h : DecidablePred fun x => True<VAR>s : Finset α<GOAL>Finset.filter (fun x => True) s = s
<VAR>α : Type u_1<VAR>h : DecidablePred fun x => False<VAR>s : Finset α<GOAL>Finset.filter (fun x => False) s = ∅
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.filter p s = s ↔ ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>(Finset.filter p s).Nonempty ↔ ∃ a ∈ s, p a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>h : ∀ x ∈ s, p x<GOAL>Finset.filter p s = s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>h : ∀ x ∈ s, ¬p x<GOAL>Finset.filter p s = ∅
<VAR>α : Type u_1<VAR>p : Prop<VAR>Decidable p<VAR>s : Finset α<GOAL>Finset.filter (fun _a => p) s = if p then s else ∅
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>s : Finset α<VAR>H : ∀ x ∈ s, p x ↔ q x<GOAL>Finset.filter p s = Finset.filter q s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finset.filter p ∅ = ∅
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>Finset.filter p s ⊆ Finset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Monotone (Finset.filter p)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>h : p ≤ q<GOAL>Finset.filter p s ⊆ Finset.filter q s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>↑(Finset.filter p s) = {x | x ∈ s ∧ p x}
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<VAR>t : Set α<VAR>h₁ : t ⊆ ↑s<VAR>h₂ : ∀ x ∈ t, p x<GOAL>t ⊆ ↑(Finset.filter p s)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<GOAL>Finset.filter p {a} = if p a then {a} else ∅
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hp : p a<GOAL>Finset.filter p (Finset.cons a s ha) = Finset.cons a (Finset.filter p s) ⋯
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hp : ¬p a<GOAL>Finset.filter p (Finset.cons a s ha) = Finset.filter p s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<GOAL>Disjoint (Finset.filter p s) (Finset.filter q s) ↔ ∀ x ∈ s, p x → ¬q x
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<GOAL>Disjoint s t → Disjoint (Finset.filter p s) (Finset.filter q t)
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>h : Disjoint p q<GOAL>Disjoint (Finset.filter p s) (Finset.filter q t)
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>(x : α) → Decidable ¬p x<GOAL>Disjoint (Finset.filter p s) (Finset.filter (fun a => ¬p a) t)