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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ y, y ∈ l ∧ y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
ih : 0 - s = 0
⊢ 0 - a ::ₘ s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬xs.Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ ∀ (a_1 b : List α), count a (⟦a_1⟧ - ⟦b⟧) = count a ⟦a_1⟧ - count a ⟦b⟧

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u
l : List α
hne : l ≠ []
hnd : l.Nodup
⊢ l.head hne = l.getLast hne ↔ ∃ x, l = [x]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
⊢ s + t - u = s + (t - u)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ idxOf (l.get i) l = ↑i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ x ∈ l → count x l = 1

Tactic:
by

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

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

Tactic:
by

Goal state after:
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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hstu : s + t = u
⊢ s = u - t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ (l₂ ++ l₁).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
⊢ (l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ (s - t).card + t.card = s.card

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ∈ s - t ↔ count a t < count a s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ b ::ₘ (bs₀ + bs₁) = b ::ₘ bs₀ + bs₁

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l : List α
d : (map f l).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y

Tactic:
by

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

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

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ l.Nodup → (List.filter p l).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ Pairwise (fun a b ↦ b ≠ a) l ↔ l.Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
u : α
⊢ (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 β
⊢ Rel r (a ::ₘ s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m1 m2 : Multiset α
r : α → α → Prop
h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b
hc : m1.card = m2.card
⊢ Rel r m1 m2

Tactic:
by

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

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u

Tactic:
rel_zero_right.mp r1,

Goal state after:
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r 0 u
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:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l[0]? = l.getLast?
⊢ l.reverse.tail.Nodup ↔ l.tail.Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+ l₂
hne : l₂ ≠ []
hl : l₂.head hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <+: l₂
hne : l₂ ≠ []
hl : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₂ ≠ []
hl : l₂.head hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ <+: l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₂ ≠ []
hl : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ <:+ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₂ ≠ []
hlh : l₂.head hne ∈ l₁
hlg : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑s.attach = Set.univ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l.Nodup
i : Fin l.length
⊢ l.erase (l.get i) = l.eraseIdx ↑i

Tactic:
by

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

Goal state before:
pp: α : Type u
L : List (List α)
⊢ L.flatten.Nodup ↔ (∀ (l : List α), l ∈ L → l.Nodup) ∧ Pairwise Disjoint L

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (flatMap f l₁).Nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).Nodup) ∧ Pairwise (Disjoint on f) l₁

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
h₂ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a : α
x✝ : a ∈ l₁
b b' : σ a
h : ⟨a, b⟩ = ⟨a, b'⟩
⊢ b = b'

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
h₂ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b' ∈ f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → β
s t : Multiset α
⊢ s = t → (∀ (x : α), x ∈ t → f x = g x) → map f s = map g t

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l.concat a).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β β' : Type v
m : Multiset α
f : α → β
f' : α → β'
h : β = β'
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ map f m ≍ map f' m

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
h : l₂.Nodup
⊢ (l₁ ∪ l₂).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
k : ℕ
a : α
⊢ map f (replicate k a) = replicate k (f a)

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
⊢ ∀ (x : Multiset α), (∀ (x_1 : α), x_1 ∈ x → p x_1) → ∃ y, map c y = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = map f s ↔ s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl₁ : l₁.Nodup
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l

Tactic:
by

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s

Tactic:
by

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
⊢ take (n + 1) (b :: l) = List.filter (fun a ↦ elem a (take (n + 1) (b :: l))) (b :: l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) ↑l
⊢ b₁ ∈ replicate (↑l).card b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ x ∈ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ Surjective (map f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr f x s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f x s)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ map val (s.attach.erase x) = s.erase ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
s : Multiset α
f : α → β
x : { x // x ∈ s }
⊢ map (fun j ↦ f ↑j) (s.attach.erase x) = map f (s.erase ↑x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ⟦l₁⟧ - ⟦l₂⟧ = foldl erase ⟦l₁⟧ ⟦l₂⟧

Tactic:
by

Goal state after:
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:
by

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

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Multiset α
hst : Rel r s t
a✝ b✝ : α
as✝ bs✝ : Multiset α
hab : r a✝ b✝
_hst : Rel r as✝ bs✝
ih : map (Quot.mk r) as✝ = map (Quot.mk r) bs✝
⊢ map (Quot.mk r) (a✝ ::ₘ as✝) = map (Quot.mk r) (b✝ ::ₘ bs✝)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ t = map (fun x ↦ i ↑x ⋯) s.attach

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map f s = pmap (fun x x_1 ↦ f x) s ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l.dedup.tail = l'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ pmap (fun x x_1 ↦ f x) s ⋯ = map (fun x ↦ f ↑x) s.attach

Tactic:
by

Goal state after: