mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
x : α
⊢ x ∈ (cons a s h).toList ↔ x ∈ a :: s.toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 ↦ f ↑a_1) ↔ _root_.Pairwise (r on fun a ↦ f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
h inst✝ : DecidablePred p
⊢ filter p s = filter p s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ True
s : Finset α
⊢ filter (fun x ↦ True) s = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ False
s : Finset α
⊢ filter (fun x ↦ False) s = ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = insert n (range n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n ∉ range n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n ∈ range (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ (filter p s).Nonempty ↔ ∃ a, a ∈ s ∧ p a

Tactic:
by

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
⊢ range n ⊆ s ↔ ∀ x < n, x ∈ s

Tactic:
by

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

Goal state before:
pp: s : Finset ℕ
n : ℕ
⊢ s ⊆ range n ↔ ∀ x ∈ s, x < n

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ range n ⊆ range m ↔ n ≤ m

Tactic:
by

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

Goal state before:
pp: x✝ : ℕ
⊢ range x✝ ⊂ range (x✝ + 1)

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ a ∈ range b.succ ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
⊢ filter (fun _a ↦ p) s = if p then s else ∅

Tactic:
by

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

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ x ≤ n

Tactic:
by

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

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ n - x ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝ : (range n).Nonempty
k : ℕ
hk : k ∈ range n
⊢ n ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), a ∈ s → p a → q a
⊢ filter p s ⊆ filter q s

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ 0 ∈ range n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ range n = ∅ ↔ n = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ 0 ∈ Set.Iio n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (range n).Nontrivial

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) i
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ t ∧ f x = i

Tactic:
by

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

Goal state before:
pp: s : Finset ℕ
⊢ ∃ n, ∅ ⊆ range n

Tactic:
by

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

Goal state before:
pp: s : Finset ℕ
a : ℕ
x✝² : Finset ℕ
x✝¹ : a ∉ x✝²
x✝ : ∃ n, x✝² ⊆ range n
n : ℕ
hn : x✝² ⊆ range n
⊢ insert a x✝² ⊆ range (max (a + 1) n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
k j : ℕ
⊢ j + k ∉ range k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
⊢ Function.LeftInverse (fun j ↦ ⟨j + k, ⋯⟩) fun i ↦ ↑i - k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
⊢ Function.RightInverse (fun j ↦ ⟨j + k, ⋯⟩) fun i ↦ ↑i - k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
⊢ x ∈ t ∧ f x = j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
⊢ s.PairwiseDisjoint fun x ↦ filter (fun x_1 ↦ f x_1 = x) t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ Disjoint (filter (fun x ↦ p x ∧ ¬q x) s) (filter (fun x ↦ q x ∧ ¬p x) s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Finset α
⊢ filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidablePred fun x ↦ x ∈ s
hst : s ⊆ t
⊢ filter (fun x ↦ x ∈ s) t = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ (s₂ \ s₁) = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ ∀ (a b : Finset α), a ⊓ b ⊔ a \ b = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ ∀ (a b : Finset α), a ⊓ b ⊓ a \ b = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ a ∉ s \ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ a ∉ s \ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ s ∪ t \ s = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ s₂ \ s₁ ∪ s₁ = s₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u v : Finset α
hst : s ⊆ t
hvu : v ⊆ u
⊢ s \ u ⊆ t \ v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ s \ u ⊆ t \ u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ u \ t ⊆ u \ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun x ↦ x ∪ s) {t | Disjoint s t}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun x ↦ x \ s) {t | s ⊆ t}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∪ t \ s = t ∪ s \ t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t s : Finset α
x : α
h : x ∈ t
⊢ insert x s \ t = s \ t

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
⊢ insert a s \ insert b s = {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
hb : b ∉ s
⊢ cons a s ha \ cons b s hb = {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
⊢ s \ insert x t = s \ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s \ t ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : t ⊆ s
ht : t.Nonempty
⊢ s \ t ⊂ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ (s \ {c}).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ s.Finite ↔ t.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
p : α → Prop
⊢ (∀ (a : α), a ∈ s ∪ t → p a) ↔ (∀ (a : α), a ∈ s → p a) ∧ ∀ (a : α), a ∈ t → p a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x✝ : α
⊢ x✝ ∈ s ∪ (t ∪ u) ↔ x✝ ∈ t ∪ (s ∪ u)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t

Tactic:
simp only [mem_union, or_assoc, @or_comm (x ∈ t)]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = s ∪ t ↔ t ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = t ∪ s ↔ t ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ u : Finset α
⊢ s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ s₂ = s₂ ∩ s₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a✝ : α
a b c : Finset α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊆ a ⊔ b ⊓ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ s ∨ x ∈ ∅ ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ ∅ ∨ x ∈ s ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ s ∪ {x} = insert x s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
⊢ ∀ (a b : Finset α), P a b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ s ∧ x✝ ∈ ∅ ↔ x✝ ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ ∅ ∧ x✝ ∈ s ↔ x✝ ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x = a → x ∈ s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
⊢ ¬(x = a ∧ x ∈ s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), x ∉ {a} ∩ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ {a} ∩ s = if a ∈ s then {a} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s ∩ {a} = if a ∈ s then {a} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

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.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ s.disjUnion t h = s ∪ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∈ s, a ∈ t) ↔ (s ∩ t).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ (s ∩ t).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
ι : Type u_4
s : Set ι
f : ι → Finset α
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirectedOrder (Finset α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nontrivial
⊢ ∀ (a_1 : α), a_1 ∈ s ∧ a_1 ≠ a → a_1 ∈ s.erase a

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.erase a).Nonempty ↔ s.Nontrivial

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
ha : a ∉ s
hb : a ≠ b
⊢ (cons a s ha).erase b = cons a (s.erase b) ⋯

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : a ∈ s
ht : a ∉ t
⊢ s.erase a = t ↔ s = insert a t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s.erase a ⊂ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊂ t ↔ ∃ 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 : Finset α
a : α
⊢ s.erase a ⊆ (insert a s).erase a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ⊆ insert a t ↔ s.erase 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 : α
h : a ∉ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ∀ (x : α), x ∈ univ.val

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ ↔ ∀ (x : α), x ∈ s

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 ∈ t
⊢ s.erase a ⊆ t ↔ s ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ↑univ = Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ ↑s = Set.univ ↔ s = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x

Tactic:
by

Goal state after: