mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Count

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂) + countP p l₂

Tactic:
rw [← countP_append]

Goal state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true

Tactic:
· simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t

Tactic:
cons_add,

Goal state after:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ (a ::ₘ 0 + t)
⊢ s = a ::ₘ a ::ₘ t
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ (a ::ₘ 0 + t)
⊢ s = a ::ₘ a ::ₘ t

Tactic:
cons_add,

Goal state after:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ (0 + t)
⊢ s = a ::ₘ a ::ₘ t
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ l

Tactic:
mem_iff_get,

Goal state after:
α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ ∃ n, l.get n = x
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg.inl
α : Type u
x hd : α
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
h : [hd].Nodup
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x

pp: case neg.inr
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
· simp

Goal state after:
case neg.inr
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ t + s = a ::ₘ (s + t)

Tactic:
cons_add,

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ (t + s) = a ::ₘ (s + t)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : ∀ (a : α), count a l = 1
a : α
⊢ 1 ≤ count a l

Tactic:
by grind

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)

pp: case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
· simp

Goal state after:
case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.map (fun p ↦ ⟨↑p, ⋯⟩) (List.pmap mk l ⋯)

Tactic:
List.map_pmap

Goal state after:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.pmap (fun a_1 h ↦ ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ (xs ++ ys).dedup = xs.dedup ++ ys.dedup

Tactic:
by
  rw [List.dedup_append, Disjoint.union_eq]
  intro a hx hy
  exact h hx (mem_dedup.mp hy)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
s : Multiset α
l : List α
⊢ (map f (Quot.mk (⇑(isSetoid α)) l)).dedup = map f (dedup (Quot.mk (⇑(isSetoid α)) l))

Tactic:
by simp [List.dedup_map_of_injective hf l]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ (Quot.mk (⇑(isSetoid α)) a✝ + Quot.mk (⇑(isSetoid α)) b✝).dedup = dedup (Quot.mk (⇑(isSetoid α)) b✝)

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.dedup_append_right h

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

pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a ↦ f x = f a) s → f x = f b

Tactic:
· simp

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a ↦ f x = f a) s → f x = f b
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t

Tactic:
and_iff_right_of_imp

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t → u + s = u ∪ s
Module: Mathlib.Data.Finset.Empty

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), ¬x ∈ s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ¬s ⊂ ∅

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
⊢ ↑∅ = ∅

Tactic:
by grind

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

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

Tactic:
by grind

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: case cons.succ
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
n : ℕ
h : n + 1 < (a :: l).tails.length
⊢ (a :: l).tails[n + 1] = drop (n + 1) (a :: l)

Tactic:
| succ n =>

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

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

Tactic:
| succ n =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hs : b ∈ s
hsa : ¬b ∈ s.erase a
⊢ b = a

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Tactic:
by
  rw [_root_.disjoint_comm, disjoint_left]

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

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Tactic:
simp only [disjoint_left, imp_not_comm, forall_eq']

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

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

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ↑{a} = {a}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ ↑s = {a} ↔ s = {a}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ ↑s ⊆ {a} ↔ s ⊆ {a}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ {a} ⊆ ↑s ↔ {a} ⊆ s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ s ⊂ {a} ↔ s = ∅

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ ↑{a, b} = {a, b}

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
simp_rw [← coe_subset]; simp [ha]

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 : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥(insert x t)
⊢ (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) ((fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) y) = y

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x

Tactic:
by grind

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

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

Tactic:
by grind

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 grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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 grind

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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

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

Tactic:
by grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Tactic:
rw [Pi.disjoint_iff] at h

Goal state after:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

Goal state after: