mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ Rel r (b ::ₘ m') (a ::ₘ t)

Tactic:
refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩

Goal state after:
case refine_2.refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b

case refine_2.refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ m'.card = t.card
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ b ::ₘ bs + bs₁ = b ::ₘ (bs + bs₁)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : [].Nodup
i : ℕ
h : i < [].length
⊢ [].erase [][i] = [].eraseIdx i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons.zero
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
h : 0 < (a :: l).length
⊢ (a :: l).erase (a :: l)[0] = (a :: l).eraseIdx 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
x✝ : ↥s
⊢ x✝ ∈ ↑s.attach ↔ x✝ ∈ Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
t : α
x✝ : Multiset α
⊢ (map f ∘ cons t) x✝ = (cons (f t) ∘ map f) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
x✝ : l₁.Nodup
⊢ l₁.diff [] = List.filter (fun x ↦ decide ¬x ∈ []) l₁

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hl : [].Nodup
⊢ map (update f x y) [] = if x ∈ [] then (map f []).set (idxOf x []) y else map f []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : ℕ
x✝ : [].Nodup
⊢ take n [] = List.filter (fun a ↦ elem a (take n [])) []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
x✝ : (b :: l).Nodup
⊢ take 0 (b :: l) = List.filter (fun a ↦ elem a (take 0 (b :: l))) (b :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
f : α → β
a : α
⊢ map f {a} = {f a}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ elem b (b :: List.filter (fun a ↦ elem a (take n l)) l) = true

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case empty
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case pos.refl
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
⊢ map f ((x ::ₘ s).erase x) = (map f (x ::ₘ s)).erase (f x)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case empty
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x : α
h : x ∈ 0
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case cons.inl
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
y : α
s : Multiset α
ih : y ∈ s → map f (s.erase y) = (map f s).erase (f y)
h : y ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(l₁.diff l₂) = foldl erase ↑l₁ ↑l₂

Tactic:
diff_eq_foldl l₁ l₂

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.foldl List.erase l₁ l₂) = foldl erase ↑l₁ ↑l₂
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ {t : Multiset β}, Rel r (map f 0) t ↔ Rel (fun a b ↦ r (f a) b) 0 t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup

Tactic:
| cons a l₁ IH =>

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
⊢ (map f []).dedup = map f [].dedup

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
ys : List α
h : [] ⊆ ys
⊢ [] ∪ ys = ys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
ys : List α
h : [].Disjoint ys
⊢ [] ∪ ys = [].dedup ++ ys

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ = [] ↔ [] ∩ l₂ = []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ <+ [] ∩ l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ [].bagInter t₁ = [].bagInter t₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
⊢ [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂

Tactic:
rw [List.map_append, List.map_diff finj]

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
by simp [(· ∪ ·), union]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
_l : List α
⊢ a ∈ filter p (Quot.mk (⇑(isSetoid α)) _l) ↔ a ∈ Quot.mk (⇑(isSetoid α)) _l ∧ p a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b ↦ decide (p b)) _l = _l ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → p a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b ↦ decide (p b)) _l = [] ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → ¬p a

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ filter (fun x ↦ False) s = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk (⇑(isSetoid α)) l)) = filter (fun a ↦ p a ∧ q a) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - 0 + 0 ∩ s = s

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
⊢ map f (filter p 0) = filterMap (fun a ↦ if p a then some (f a) else none) 0

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : p a
⊢ map (fun x ↦ f x) {a} = (some {f a}).getD 0

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : ¬p a
⊢ map (fun x ↦ f x) 0 = none.getD 0

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_6
α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countP p (filter (fun a ↦ ¬q a) (Quot.mk (⇑(isSetoid α)) l)) =
    List.countP (fun x ↦ decide (p x)) (List.filter (fun a ↦ !decide (q a)) l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(s.bagInter t)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.toList.toFinset ↔ a✝ ∈ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (replicate (filter (fun a ↦ f x = f a) s).card x) = (replicate (filter (fun a ↦ f x = f a) s).card x).card

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - 0) = filter p s - filter p 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Induction

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRecOn [] nil append_singleton = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Induction

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <+: (l₁ ++ l).flatten

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <:+ (l ++ l₁).flatten

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l l' : List (List α)
⊢ l₁.flatten <:+: (l ++ l₁ ++ l').flatten

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ ndinsert a s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
xs : List α
x : α
⊢ [] <:+: [x] ↔ [] = [] ∨ [] = [x]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = [] :: map (fun t ↦ a :: t) l.inits

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (a :: l) :: l.tails

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ ([] ++ []).inits = [].inits ++ map (fun l ↦ [] ++ l) [].inits.tail

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).inits = [].inits ++ map (fun l ↦ [] ++ l) (a :: t).inits.tail

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ ([] ++ []).tails = map (fun l ↦ l ++ []) [].tails ++ [].tails.tail

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).tails = map (fun l ↦ l ++ a :: t) [].tails ++ (a :: t).tails.tail

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ [].inits = (map reverse [].reverse.tails).reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ [].tails = (map reverse [].reverse.inits).reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
⊢ [].tails.length = [].length + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
h : n < [].tails.length
⊢ [].tails[n] = drop n []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons.zero
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
h : 0 < (a :: l).tails.length
⊢ (a :: l).tails[0] = drop 0 (a :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : Fin l.tails.length
⊢ l.tails.get n = drop (↑n) l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
h : n < [].inits.length
⊢ [].inits[n] = take n []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons.zero
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
h : 0 < (a :: l).inits.length
⊢ (a :: l).inits[0] = take 0 (a :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : Fin l.inits.length
⊢ l.inits.get n = take (↑n) l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case hl
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

Tactic:
simp [take_take] <;> grind

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]

Tactic:
simp [take_take] <;> grind

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} ⊆ {b} ↔ a = b

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
s t : Finset α
h : Disjoint s t
⊢ ∀ (x : α), x ∈ ↑(s.disjUnion t h) ↔ x ∈ ↑s ∪ ↑t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a b : α
s : Finset α
l : List α
h : Nodup ⟦[]⟧
⊢ ¬{ val := ⟦[]⟧, nodup := h }.Nontrivial

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a✝ b✝ : α
s : Finset α
l : List α
a b : α
tail✝ : List α
h : Nodup ⟦a :: b :: tail✝⟧
⊢ a ∈ ↑{ val := ⟦a :: b :: tail✝⟧, nodup := h }

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a✝ b✝ : α
s : Finset α
l : List α
a b : α
tail✝ : List α
h : Nodup ⟦a :: b :: tail✝⟧
⊢ b ∈ ↑{ val := ⟦a :: b :: tail✝⟧, nodup := h }

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
hm : Nodup 0
⊢ { val := 0, nodup := hm }.Nonempty ↔ 0 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u_1
a✝¹ : α
s✝ : Multiset α
a✝ : ∀ {hm : s✝.Nodup}, { val := s✝, nodup := hm }.Nonempty ↔ s✝ ≠ 0
hm : (a✝¹ ::ₘ s✝).Nodup
⊢ { val := a✝¹ ::ₘ s✝, nodup := hm }.Nonempty ↔ a✝¹ ::ₘ s✝ ≠ 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
⊢ x ∈ insert y s ↔ x ∈ insert y ↑s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
f : α → β
a : α
⊢ insert a ∅ = {a}

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].toFinset = ∅ ↔ [] = []

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).toFinset = ∅ ↔ head✝ :: tail✝ = []

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: m n a✝ : ℕ
⊢ a✝ ∈ range m ∩ range n ↔ a✝ ∈ range (min m n)

Tactic:
simp

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

Goal state before:
pp: m n a✝ : ℕ
⊢ a✝ ∈ range m ∪ range n ↔ a✝ ∈ range (max m n)

Tactic:
simp

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:
simp

Goal state after: