mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.13
β : α → Type u_4
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : Fintype α
f g : (a : α) → β a
⊢ (∀ (a : α), a ∈ univ → f a = g a) ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ (∀ (a : α), a ∈ univ → p a) ↔ ∀ (a : α), p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ (∃ a, a ∈ univ ∧ p a) ↔ ∃ a, p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ (Multiset.map f univ.val).Nodup ↔ Injective f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ { elems := s₁, complete := h₁ } = { elems := s₂, complete := h₂ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ {true, false}.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
⊢ x ∈ { val := {true, false}, nodup := fintype._proof_1 }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ {lt, eq, gt}.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
⊢ x ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
⊢ s.erase a \ s.erase b = {b}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s \ {a} = s.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ Disjoint (insert a s) (t.erase a) ↔ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ∩ t.erase a = (s ∩ t).erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s.erase a ∩ t = (s ∩ t).erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a \ t = (s \ t).erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a ∩ t = s ∩ t.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (s \ t).erase a = s.erase a \ t.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a : α
ha : a ∈ t
s : Finset α
⊢ s.erase a ∪ t = s ∪ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
t : Finset α
⊢ s ∪ t.erase a = s ∪ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hts : t ⊆ s
ha : a ∈ t
⊢ s \ t ∪ t.erase a = s.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
⊢ s \ insert x t = (s \ t).erase x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
hxs : x ∈ s
hxt : x ∉ t
⊢ insert x (s \ insert x t) = s \ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ s
⊢ s \ t.erase a = insert a (s \ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ s \ s.erase a = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.attach.Nonempty ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.attach = ∅ ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ Disjoint (filter p s) (filter q t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t u : Finset α
h : Disjoint s t
⊢ Disjoint (s.disjUnion t h) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t u : Finset α
h : Disjoint t u
⊢ Disjoint s (t.disjUnion u h) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ filter p (s₁ ∪ s₂) = filter p s₁ ∪ filter p s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
⊢ filter p s ∪ filter q s = filter (fun x ↦ p x ∨ q x) s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ t)
⊢ filter (fun i ↦ i ∈ t) s = s ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∉ t)
⊢ filter (fun i ↦ i ∉ t) s = s \ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p (s ∩ t) = filter p s ∩ filter p t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p s ∩ t = filter p (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ filter p t = filter p (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (insert a s) = if p a then insert a (filter p s) else filter p s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a ↦ p a ∨ q a) s = filter p s ∪ filter q s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a ↦ p a ∧ q a) s = filter p s ∩ filter q s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a ↦ ¬p a) s = s \ filter p s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun a ↦ p a ∧ ¬q a) s = filter p s \ filter q s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ \ s₂ = filter (fun x ↦ x ∉ s₂) s₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (Eq b) s = if b ∈ s then {b} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (fun a ↦ a = b) s = if b ∈ s then {b} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (fun a ↦ b ≠ a) s = s.erase b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: n m : ℕ
⊢ filter (fun x ↦ x = m) (range n) = if m < n then {m} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: m n : ℕ
⊢ range m ∩ range n = range (min m n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nonempty ↔ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: m n : ℕ
⊢ range m ∪ range n = range (max m n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ = ∅ ↔ IsEmpty α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s + t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nontrivial ↔ Nontrivial α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : α
⊢ {a} ≠ univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ sᶜ ↔ a ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ sᶜ ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ s ⇨ t ↔ a ∈ s → a ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s.toFinset.Nonempty ↔ s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ s ⇔ t ↔ (a ∈ s ↔ a ∈ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter p s).toFinset = Finset.filter p s.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ s ⊆ {a}ᶜ ↔ a ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ (s.erase a)ᶜ = insert a sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ (insert a s)ᶜ = sᶜ.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ insert x {x}ᶜ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ ∀ (a : α), a ∈ (filter p univ)ᶜ ↔ a ∈ {x | ¬p x}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ sᶜ ≠ univ ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
⊢ (filter p s).toFinset = Finset.filter (fun x ↦ p x = true) s.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s : List α
p : α → Prop
inst✝ : DecidablePred p
⊢ Finset.filter p s.toFinset = (filter (fun b ↦ decide (p b)) s).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.isEmpty = true ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (union s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s.disjUnion t h
⊢ (disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ {a}ᶜ = univ.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s.disjUnion t h
⊢ (disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) ↑sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ univ ∩ s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ s ∩ univ = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a : α
⊢ {a} = univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ b ∈ map f.toEmbedding s ↔ f.symm b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
b : β
⊢ e.toEmbedding (e.symm b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
⊢ (∀ (y : β) (H : y ∈ map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p (f x) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ↑(map f s) = ⇑f '' ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y ↦ ∃ x, f x = y
inst✝ : DecidableEq β
⊢ {y | ∃ x, f x = y} = image f univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ↑(map f s) ⊆ Set.range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
x✝ : β
⊢ x✝ ∈ map f s.toFinset ↔ x✝ ∈ (Multiset.map (⇑f) s).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y ↦ y ∈ Set.range f
inst✝ : DecidableEq β
⊢ {y | y ∈ Set.range f} = image f univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
s : Finset α
x✝ : α
⊢ x✝ ∈ map (Embedding.refl α) s ↔ x✝ ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(filter p univ) = {x | p x}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α β : Type u_4
h : α = β
s : Finset α
⊢ map (Equiv.cast h).toEmbedding s ≍ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p univ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ (map g (map f s)).val = (map (f.trans g) s).val

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map Subtype.val univ.val = (filter p univ).val

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ map f s₁ ⊆ map f s₂

Tactic:
by

Goal state after: