awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a \ t = (s \ t).erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a ∩ t = s ∩ t.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ (s \ t).erase a = s.erase a \ t.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
t : Finset α
a : α
ha : a ∈ t
s : Finset α
⊢ s.erase a ∪ t = s ∪ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
t : Finset α
⊢ s ∪ t.erase a = s ∪ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
hts : t ⊆ s
ha : a ∈ t
⊢ s \ t ∪ t.erase a = s.erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
x : α
⊢ s \ insert x t = (s \ t).erase x

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
x : α
hxs : x ∈ s
hxt : x ∉ t
⊢ insert x (s \ insert x t) = s \ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∈ s
⊢ s \ t.erase a = insert a (s \ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ s \ s.erase a = {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
rw : s \ {a} = ∅ ↔ s = ∅ ∨ s = {a}
rw₁ : s ⊆ {a} ↔ s = ∅ ∨ s = {a}
rw₂ rw₃ : s = ∅ ∨ s = {a} ↔ s = ∅ ∨ s = {a}
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

Tactic:
rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]

Premises used: Finset.sdiff_singleton_eq_erase, Finset.sdiff_eq_empty_iff_subset, Finset.subset_singleton_iff
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint (t \ s) s

Tactic:
disjoint_left.2 fun _a ha => (mem_sdiff.1 ha).2

Premises used: Iff.mpr, Finset.mem_sdiff, And.right, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint s (t \ s)

Tactic:
sdiff_disjoint.symm

Premises used: Disjoint.symm, Finset.sdiff_disjoint
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Disjoint (s \ t) (s ∩ t)

Tactic:
disjoint_of_subset_right inter_subset_right sdiff_disjoint

Premises used: Finset.inter_subset_right, Finset.disjoint_of_subset_right, Finset.sdiff_disjoint
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset ↥∅) (attach ∅) ∅

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiset.zero, Finset.empty, Multiset.Mem, List.pmap, Multiset.ofList, Multiset.pmap, Finset.attach, Multiset.attach, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
⊢ s.attach.Nonempty ↔ s.Nonempty

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
⊢ s.attach = ∅ ↔ s = ∅

Tactic:
simp [eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
hp : p a
⊢ filter p (cons a s ha) = cons a (filter p s) ⋯

Tactic:
eq_of_veq <| s.val.filter_cons_of_pos hp

Premises used: Finset.eq_of_veq, Finset.val, Multiset.filter_cons_of_pos
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
hp : ¬p a
⊢ filter p (cons a s ha) = filter p s

Tactic:
eq_of_veq <| s.val.filter_cons_of_neg hp

Premises used: Finset.eq_of_veq, Finset.val, Multiset.filter_cons_of_neg
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
mp : Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x
mpr : (∀ x ∈ s, p x → ¬q x) → Disjoint (filter p s) (filter q s)
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x

Tactic:
simp +contextual [disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ (∀ x ∈ s, p x → ¬q x) → Disjoint (filter p s) (filter q s)

Tactic:
simp +contextual [disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : Disjoint p q
simp_rw : ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
⊢ Disjoint (filter p s) (filter q t)

Tactic:
simp_rw [disjoint_left, mem_filter]

Premises used: Finset.mem_filter, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : Disjoint p q
a : α
left : a ∈ s
hp : p a
left_1 : a ∈ t
hq : q a
rw : ∀ (h : ∀ (i : α), Disjoint (p i) (q i)) ⦃a : α⦄, a ∈ s → ∀ (hp : p a), a ∈ t → ∀ (hq : q a), False
⊢ False

Tactic:
rw [Pi.disjoint_iff] at h

Premises used: Pi.disjoint_iff
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t : Finset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left : a ∈ s
hp : p a
left_1 : a ∈ t
hq : q a
⊢ False

Tactic:
simpa [hp, hq] using h a
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
⊢ Disjoint (filter p s) (filter (fun (a : α) ↦ ¬p a) t)

Tactic:
s.disjoint_filter_filter' t disjoint_compl_right

Premises used: Finset.disjoint_filter_filter', disjoint_compl_right
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Finset α
h : Disjoint s t
⊢ filter p (s.disjUnion t h) = (filter p s).disjUnion (filter p t) ⋯

Tactic:
eq_of_veq <| Multiset.filter_add _ _ _

Premises used: Finset.eq_of_veq, Multiset.filter_add
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
⊢ filter p (cons a s ha) = if p a then cons a (filter p s) ⋯ else filter p s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t u : Finset α
h : Disjoint s t
⊢ Disjoint (s.disjUnion t h) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
simp only [disjoint_left, mem_disjUnion, or_imp, forall_and]

Premises used: or_imp, Finset.mem_disjUnion, Finset.disjoint_left, forall_and
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s t u : Finset α
h : Disjoint t u
⊢ Disjoint s (t.disjUnion u h) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
simp only [disjoint_right, mem_disjUnion, or_imp, forall_and]

Premises used: or_imp, Finset.mem_disjUnion, Finset.disjoint_right, forall_and
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
s₁ s₂ : Finset α
⊢ filter p (s₁ ∪ s₂) = filter p s₁ ∪ filter p s₂

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : DecidableEq α
s : Finset α
⊢ filter p s ∪ filter q s = filter (fun (x : α) ↦ p x ∨ q x) s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
inst_1 : (i : α) → Decidable (i ∈ t)
⊢ filter (fun (i : α) ↦ i ∈ t) s = s ∩ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
inst_1 : (i : α) → Decidable (i ∉ t)
⊢ filter (fun (i : α) ↦ i ∉ t) s = s \ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
s t : Finset α
⊢ filter p (s ∩ t) = filter p s ∩ filter p t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
s t : Finset α
⊢ filter p s ∩ t = filter p (s ∩ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
s t : Finset α
⊢ s ∩ filter p t = filter p (s ∩ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
a : α
s : Finset α
⊢ filter p (insert a s) = if p a then insert a (filter p s) else filter p s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
a : α
s : Finset α
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : DecidableEq α
s : Finset α
⊢ filter (fun (a : α) ↦ p a ∨ q a) s = filter p s ∪ filter q s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : DecidableEq α
s : Finset α
⊢ filter (fun (a : α) ↦ p a ∧ q a) s = filter p s ∩ filter q s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
s : Finset α
⊢ filter (fun (a : α) ↦ ¬p a) s = s \ filter p s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
p q : α → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred q
⊢ filter (fun (a : α) ↦ p a ∧ ¬q a) s = filter p s \ filter q s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ \ s₂ = filter (fun (x : α) ↦ x ∉ s₂) s₁

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁

Tactic:
⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩

Premises used: Membership.mem, And.intro, Exists.intro, Finset.filter, Not
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
refine_2 : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
refine_3 : (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) ⊆ t₂ \ t₁
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁

Tactic:
refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
⊢ filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
⊢ (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
x : α
refine_3 : x ∈ s → x ∉ t₁ → x ∈ t₂ \ t₁
⊢ x ∈ (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) → x ∈ t₂ \ t₁

Tactic:
simp only [coe_filter, Set.mem_setOf_eq, and_imp]

Premises used: Finset.coe_filter, and_imp, Set.mem_setOf_eq
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : x ∉ t₁
⊢ x ∈ t₂ \ t₁

Tactic:
⟨Or.resolve_left (h hx) hx₂, hx₂⟩

Premises used: Set.Mem, Set.diff, setOf, Or.resolve_left, And.intro
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : x ∉ t₁
⊢ x ∈ t₂ \ t₁

Tactic:
exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : (↑s : Set α) ⊆ t₁ ∪ t₂
refine_1 : filter (fun (x : α) ↦ x ∈ t₁) s ∪ filter (fun (x : α) ↦ x ∉ t₁) s = s
refine_2 : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
refine_3 : (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) ⊆ t₂ \ t₁
refine_2₁ : (↑(filter (fun (x : α) ↦ x ∈ t₁) s) : Set α) ⊆ t₁
refine_3₁ refine_3₂ : (↑(filter (fun (x : α) ↦ x ∉ t₁) s) : Set α) ⊆ t₂ \ t₁
⊢ ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ (↑s₁ : Set α) ⊆ t₁ ∧ (↑s₂ : Set α) ⊆ t₂ \ t₁

Tactic:
classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_setOf_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

Premises used: Finset.coe_filter, and_imp, Set.mem_setOf_eq
-- Module: Mathlib.Data.Finset.Basic
Goal:
β : Type u_2
inst : DecidableEq β
s : Finset β
b : β
⊢ filter (Eq b) s = if b ∈ s then {b} else ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
β : Type u_2
inst : DecidableEq β
s : Finset β
b : β
⊢ filter (fun (a : β) ↦ a = b) s = if b ∈ s then {b} else ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
β : Type u_2
inst : DecidableEq β
s : Finset β
b : β
⊢ filter (fun (a : β) ↦ b ≠ a) s = s.erase b

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
β : Type u_2
inst : DecidableEq β
s : Finset β
b x : β
h : x ∈ s
⊢ x ≠ b ↔ b ≠ x

Tactic:
simp_rw [@ne_comm _ b]

Premises used: ne_comm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : DecidableEq α
s : Finset α
h : Codisjoint p q
⊢ filter p s ∪ filter q s = s

Tactic:
(filter_or _ _ _).symm.trans <| filter_true_of_mem fun x _ => h.top_le x trivial

Premises used: trivial, Codisjoint.top_le, Finset.filter_true_of_mem, Finset.filter_or, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : DecidableEq α
inst_2 : (x : α) → Decidable ¬p x
s : Finset α
⊢ filter p s ∪ filter (fun (a : α) ↦ ¬p a) s = s

Tactic:
filter_union_filter_of_codisjoint _ _ _ <| @codisjoint_hnot_right _ _ p

Premises used: codisjoint_hnot_right, Finset.filter_union_filter_of_codisjoint
-- Module: Mathlib.Data.Finset.Basic
Goal:
n m : ℕ
⊢ filter (fun (x : ℕ) ↦ x = m) (range n) = if m < n then {m} else ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Basic
Goal:
m n : ℕ
h : ∀ (a : ℕ), a ∈ range m ∩ range n ↔ a ∈ range (min m n)
⊢ range m ∩ range n = range (min m n)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
m n a : ℕ
⊢ a ∈ range m ∩ range n ↔ a ∈ range (min m n)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
m n : ℕ
h : ∀ (a : ℕ), a ∈ range m ∪ range n ↔ a ∈ range (max m n)
⊢ range m ∪ range n = range (max m n)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
m n a : ℕ
⊢ a ∈ range m ∪ range n ↔ a ∈ range (max m n)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s + t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : ∀ (a : α), a ∈ (s ∪ t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ (s ∪ t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ m.toFinset = ∅ ↔ m = 0

Tactic:
Finset.val_inj.symm.trans Multiset.dedup_eq_zero

Premises used: Multiset.dedup_eq_zero, Iff.trans, Finset.val_inj, Iff.symm
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.toFinset.Nonempty ↔ s ≠ 0

Tactic:
simp only [toFinset_eq_empty, Ne, Finset.nonempty_iff_ne_empty]

Premises used: Multiset.toFinset_eq_empty, Ne, Finset.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
p : α → Prop
inst_1 : DecidablePred p
h : ∀ (a : α), a ∈ (filter p s).toFinset ↔ a ∈ Finset.filter p s.toFinset
⊢ (filter p s).toFinset = Finset.filter p s.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
p : α → Prop
inst_1 : DecidablePred p
a : α
⊢ a ∈ (filter p s).toFinset ↔ a ∈ Finset.filter p s.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : ∀ (a : α), a ∈ (l ∪ l').toFinset ↔ a ∈ l.toFinset ∪ l'.toFinset
⊢ (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
a : α
⊢ a ∈ (l ∪ l').toFinset ↔ a ∈ l.toFinset ∪ l'.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : ∀ (a : α), a ∈ (l ∩ l').toFinset ↔ a ∈ l.toFinset ∩ l'.toFinset
⊢ (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
a : α
⊢ a ∈ (l ∩ l').toFinset ↔ a ∈ l.toFinset ∩ l'.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
p : α → Bool
h : ∀ (a : α), a ∈ (filter p s).toFinset ↔ a ∈ Finset.filter (fun (x : α) ↦ p x = true) s.toFinset
⊢ (filter p s).toFinset = Finset.filter (fun (x : α) ↦ p x = true) s.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
p : α → Bool
a : α
⊢ a ∈ (filter p s).toFinset ↔ a ∈ Finset.filter (fun (x : α) ↦ p x = true) s.toFinset

Tactic:
simp [List.mem_filter]

Premises used: List.mem_filter
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
⊢ s.toList = [] ↔ s = ∅

Tactic:
Multiset.toList_eq_nil.trans val_eq_zero

Premises used: Finset.val_eq_zero, Finset.toList, Iff.trans, Multiset.toList_eq_nil
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
⊢ s.toList.isEmpty = true ↔ s = ∅

Tactic:
simp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (toList ∅) []

Tactic:
toList_eq_nil.mpr rfl

Premises used: Iff.mpr, Finset.toList_eq_nil, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ s.toList ≠ []

Tactic:
mt toList_eq_nil.mp hs.ne_empty

Premises used: mt, Finset.Nonempty.ne_empty, Finset.toList_eq_nil, Iff.mp
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ¬s.toList.isEmpty = true

Tactic:
mt empty_toList.mp hs.ne_empty

Premises used: mt, Finset.Nonempty.ne_empty, Iff.mp, Finset.empty_toList
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : Finset α
hp : ∃! a : α, a ∈ l ∧ p a
⊢ choose p l hp ∈ l ∧ p (choose p l hp)

Tactic:
(l.chooseX p hp).property

Premises used: Set.Mem, Finset.choose, setOf, Finset.chooseX, Subtype.property
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : Finset α
hp : ∃! a : α, a ∈ l ∧ p a
⊢ choose p l hp ∈ l

Tactic:
(choose_spec _ _ _).1

Premises used: And.left, Finset.choose_spec
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : Finset α
hp : ∃! a : α, a ∈ l ∧ p a
⊢ p (choose p l hp)

Tactic:
(choose_spec _ _ _).2

Premises used: And.right, Finset.choose_spec
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : ↥s
⊢ Eq (α := ↥(s ∪ t)) ((union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) (Sum.inl x) : ↥(s ∪ t))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ : ↥(s ∪ t))

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
y : ↥t
⊢ Eq (α := ↥(s ∪ t)) ((union s t h : (a : ↥s ⊕ ↥t) → ↥(s ∪ t)) (Sum.inr y) : ↥(s ∪ t))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑y : α) ⋯ : ↥(s ∪ t))

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ Eq (α := ↥s ⊕ ↥t)
    ((Equiv.symm (union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t) (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) i hi') : ↥s ⊕ ↥t)
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i hi) : ↥s ⊕ ↥t)

Tactic:
simp [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ Eq (α := ↥s ⊕ ↥t)
    ((Equiv.symm (union s t h) : (a : ↥(s ∪ t)) → ↥s ⊕ ↥t) (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) i hi') : ↥s ⊕ ↥t)
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) i hi) : ↥s ⊕ ↥t)

Tactic:
simp [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
x : ↥s
⊢ Eq (α := ↥(s.disjUnion t h))
    ((disjUnionEquiv s t h : (a : ↥s ⊕ ↥t) → ↥(s.disjUnion t h)) (Sum.inl x) : ↥(s.disjUnion t h))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s.disjUnion t h) (↑x : α) ⋯ : ↥(s.disjUnion t h))

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
y : ↥t
⊢ Eq (α := ↥(s.disjUnion t h))
    ((disjUnionEquiv s t h : (a : ↥s ⊕ ↥t) → ↥(s.disjUnion t h)) (Sum.inr y) : ↥(s.disjUnion t h))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s.disjUnion t h) (↑y : α) ⋯ : ↥(s.disjUnion t h))

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s.disjUnion t h
⊢ Eq (α := ↥s ⊕ ↥t)
    (((disjUnionEquiv s t h).symm : (a : ↥(s.disjUnion t h)) → ↥s ⊕ ↥t)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s.disjUnion t h) i hi') :
      ↥s ⊕ ↥t)
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i hi) : ↥s ⊕ ↥t)

Tactic:
simp [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Data.Finset.Basic
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s.disjUnion t h
⊢ Eq (α := ↥s ⊕ ↥t)
    (((disjUnionEquiv s t h).symm : (a : ↥(s.disjUnion t h)) → ↥s ⊕ ↥t)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s.disjUnion t h) i hi') :
      ↥s ⊕ ↥t)
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) i hi) : ↥s ⊕ ↥t)

Tactic:
simp [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq