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

Goal state before:
pp: α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : Fin l.length
hg : (fun i ↦ l[↑i]) i = (fun i ↦ l[↑i]) j
⊢ i = j

Tactic:
by
      obtain ⟨i, hi⟩ := i; obtain ⟨j, hj⟩ := j
      rcases Nat.lt_trichotomy i j with (hij | rfl | hji)
      · exact (h i j hi hj hij hg).elim
      · rfl
      · exact (h j i hj hi hji hg.symm).elim

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t ≤ s

Tactic:
by
  rw [Multiset.sub_le_iff_le_add]
  exact le_add_right _ _

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : l.Nodup
⊢ (List.pmap f l H).Nodup

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
rw [← rel_flip, rel_add_left]; simp [rel_flip]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l.dedup
⊢ ∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b

Tactic:
by simpa only [forall_mem_ne] using! h

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

Goal state before:
pp: α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [a].bagInter l₁ = if a ∈ l₁ then [a] else []

Tactic:
by
  grind

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

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

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.dedup_append (by simpa using h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : List α
⊢ a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

Tactic:
simp only [Finset.ext_iff, mem_toFinset]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ _root_.Disjoint u s ∧ s = t

Tactic:
rw [← add_eq_union_iff_disjoint]
  refine ⟨fun h0 ↦ ?_, ?_⟩
  · rw [and_iff_right_of_imp]
    · exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h
    · rintro rfl
      exact h0
  · rintro ⟨h0, rfl⟩
    exact h0

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ (∃ x, x ∈ ∅ ∧ p x) ↔ False

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ (∀ (x : α), x ∈ ∅ → p x) ↔ True

Tactic:
by
  grind

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

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

Tactic:
simp [tails_append s t]

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

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

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Set α
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 = ∅ ∨ s = {a}

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
a : α
hs : {a}.Nontrivial
⊢ False

Tactic:
exact not_nontrivial_singleton hs

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
h : a ∉ s
p : α → Prop
⊢ (∀ x ∈ cons a s h, 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
s t : Finset α
⊢ s ⊂ t ↔ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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 (fun a ↦ p a ∧ q a) s

Tactic:
by
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  grind

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
  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 ∩ filter p 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 (s.erase a) = (filter p s).erase a

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 (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
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
  grind

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
  grind

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

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

Tactic:
by
  rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]

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
  grind

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
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ c ∈ image (const α b) s ↔ s.Nonempty ∧ b = c

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
⊢ f a ∈ image f s ↔ a ∈ s

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
hf : Set.InjOn f ↑s
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x ≠ y
⊢ (image f s).Nontrivial

Tactic:
exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

Goal state after:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
predAbove_of_succ_le _ _ h,

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (i.rev.pred ⋯).rev
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
h : n = m
⊢ Fin.cast h = cast ⋯

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
h : i < p
⊢ i.succ ≠ last n

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List α
f : α → β
⊢ (ofFn fun i ↦ f l[↑i]) = map f l

Tactic:
← Function.comp_def,

Goal state after:
α : Type u
β : Type u_1
l : List α
f : α → β
⊢ ofFn (f ∘ fun i ↦ l[↑i]) = map f l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : #s < #t
⊢ (t \ s).Nonempty

Tactic:
by
  grind

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
rw [card_eq_succ]
    grind [card_eq_three]

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

Goal state before:
pp: n m : ℕ
h : Fin n = Fin m
⊢ cast h = Fin.cast ⋯

Tactic:
cases fin_injective h

Goal state after:
case refl
n : ℕ
h : Fin n = Fin n
⊢ cast h = Fin.cast ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ snoc p x i.castSucc = p i

Tactic:
simp only [snoc, val_castSucc, is_lt, dite_true]
  convert! cast_eq rfl (p i)

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

Goal state before:
pp: case mp
α : Type u_1
l l' : List α
H : l <+ l'
⊢ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
induction H with
    | slnil => simp
    | cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
      simpa using hf
    | cons_cons _ _ IH =>
      obtain ⟨f, hf⟩ := IH
      refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
      · rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
      · rintro ⟨_ | i⟩
        · simp
        · simpa using hf _

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

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hf : l[i]? = l'[f i]?
hi : i < l.length
⊢ f i < l'.length

Tactic:
rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf

Goal state after:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : ∃ h, l'[f i] = l[i]
⊢ f i < l'.length
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
rw [← toFinset_card, toFinset_ofPred, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Infinite
ht : (s \ t).Finite
⊢ (s ∩ t).Infinite

Tactic:
by
  simpa using hs.sdiff ht

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Tactic:
simp only [Set.Infinite, finite_union, not_and_or]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLT ↔ l.SortedLT

Tactic:
simp_rw [sortedLT_iff_pairwise]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (⇑e) l) ↔ List.Pairwise (fun x1 x2 ↦ x1 < x2) l
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)

Tactic:
· rw [Fin.natAdd_lt_natAdd_iff] at hi
    exact Fin.find_min hⱼ hi

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z ≤ x ↔ x ≥ y ∧ x ≥ z

Tactic:
exact max_le_iff

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
rw [rotate_eq_rotate']

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
rw [rotate_eq_rotate']

Goal state after:
α : Type u
l l' : List α
⊢ (l ++ l').rotate' l.length = l' ++ l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l

Tactic:
rw [rotate_eq_rotate']

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' n ~ l
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
l : List α
⊢ (map (fun x ↦ count x l) (filter p l.dedup)).sum = countP p l

Tactic:
induction l with
  | nil => simp
  | cons a as h =>
    simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ l[n % l.length]? = l[n]?

Tactic:
Nat.mod_eq_of_lt h

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ l[n]? = l[n]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ l = [x].rotate ([x].length - n % [x].length) ↔ l = [x]

Tactic:
rotate_singleton

Goal state after:
α : Type u
l : List α
n : ℕ
x : α
⊢ l = [x] ↔ l = [x]
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
⊢ False

Tactic:
obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
          obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
          refine disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb
          rintro rfl
          exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.disjiUnion singleton ⋯ = s

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))

Tactic:
simp_rw [mem_map, mem_range, isRotated_iff_mod]

Goal state after:
α : Type u
l l' : List α
⊢ (∃ n, n ≤ l.length ∧ l.rotate n = l') ↔ ∃ a, a < l.length + 1 ∧ l.rotate a = l'
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ 0) 0 = fold op b₀ 0

Tactic:
fold_zero

Goal state after:
case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op b₀ 0 = fold op b₀ 0
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ s.disjiUnion (fun a ↦ (f a).disjUnion (g a) ⋯) ⋯ = (s.disjiUnion f hf).disjUnion (s.disjiUnion g hg) ⋯

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
⊢ s₁.biUnion t₁ = s₂.biUnion t₂

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.biUnion singleton = s

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
⊢ (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂

Tactic:
rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
h₁ : a'' ≠ a
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂

case inr
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁ ≍ cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α × α → β
s : Finset α
⊢ image f s.diag = image (fun x ↦ f (x, x)) s

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.diag ∪ s.offDiag = s ×ˢ s

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
has : a ∉ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
by
  grind

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝¹ : DecidableEq ι
I : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ I
s : Finset ↑I
u : (i : ↑I) → Set (π ↑i)
⊢ I.domRestrict ⁻¹' (↑s).pi u = (↑(image Subtype.val s)).pi fun i ↦ if h : i ∈ I then u ⟨i, h⟩ else Set.univ

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
s : (a : α) → Finset (γ a)
t : (a : α) → Finset (δ a)
x✝¹ x✝ : (a : α) → a ∈ univ → δ a
⊢ (fun f a ↦ f a ⋯) x✝¹ = (fun f a ↦ f a ⋯) x✝ → x✝¹ = x✝

Tactic:
by simp +contextual [funext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s t : (a : α) → Finset (δ a)
⊢ (piFinset fun i ↦ s i ∩ t i) = piFinset s ∩ piFinset t

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ {f ∈ piFinset t | f a = x} = ∅

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
⊢ piFinset (update s i t) = {f ∈ piFinset s | f i ∈ t}

Tactic:
by
  grind

Goal state after: