awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
simp : List.count a (List.filter (fun (b : α) ↦ decide (p b)) _l) = List.count a _l
⊢ count a (filter p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l)) =
    count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l)

Tactic:
simp only [quot_mk_to_coe'', filter_coe, coe_count]

Premises used: Multiset.coe_count, Multiset.filter_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
h₁ : decide (p a) = true
⊢ List.count a (List.filter (fun (b : α) ↦ decide (p b)) _l) = List.count a _l

Tactic:
apply count_filter

Premises used: List.count_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ decide (p a) = true

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
pos : ∀ (h : p a), count a (filter p s) = count a s
neg : ∀ (h : ¬p a), count a (filter p s) = 0
⊢ count a (filter p s) = if p a then count a s else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

Tactic:
count_filter_of_pos h

Premises used: Multiset.count_filter_of_pos
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

Tactic:
exact count_filter_of_pos h

Premises used: Multiset.count_filter_of_pos
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
count_filter_of_neg h

Premises used: Multiset.count_filter_of_neg
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
exact count_filter_of_neg h

Premises used: Multiset.count_filter_of_neg
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_3
β : Type u_4
f : α → β
s : Multiset α
inst : DecidableEq β
b : β
⊢ count b (map f s) = (filter (fun (a : α) ↦ b = f a) s).card

Tactic:
simp [count, countP_map]

Premises used: Multiset.count, Multiset.countP_map
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x : α | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
rw : count x (filter (fun (a : α) ↦ f x = f a) s) = count x s
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count, countP_map, ← this]

Premises used: Multiset.count, Multiset.countP_map
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x : α | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
⊢ count x (filter (fun (a : α) ↦ f x = f a) s) = count x s

Tactic:
count_filter_of_pos <| rfl

Premises used: Multiset.count_filter_of_pos, rfl
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x : α | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
⊢ count x (filter (fun (a : α) ↦ f x = f a) s) = count x s

Tactic:
exact count_filter_of_pos <| rfl

Premises used: Multiset.count_filter_of_pos, rfl
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x : α | x ∈ s}
x : α
H : x ∈ s
suffices : count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
⊢ count (f x) (map f s) = count x s

Tactic:
suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s) by
    rw [count, countP_map, ← this]
    exact count_filter_of_pos <| rfl
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x : α | x ∈ s}
x : α
H : x ∈ s
rw :
  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
rw₁ : ∀ (b : α) (hb : b ∈ filter (fun (a : α) ↦ f x = f a) s), f x = f b
⊢ count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card

Tactic:
rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]

Premises used: Iff.mpr, And.left, Iff.mp, Multiset.mem_filter, Multiset.eq_replicate_card, Eq.symm
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : 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
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x : α | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α) (hb : b ∈ filter (fun (a : α) ↦ f x = f a) s), f x = f b

Tactic:
simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]

Premises used: and_imp, eq_comm, imp_self, Multiset.mem_filter, implies_true
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
pos : ∀ (H : x ∈ s), count (f x) (map f s) = count x s
neg : ∀ (H : ¬x ∈ s), count (f x) (map f s) = count x s
⊢ count (f x) (map f s) = count x s

Tactic:
by_cases H : x ∈ s
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
count_map_eq_count f _ hf.injOn _ H

Premises used: Function.Injective.injOn, Multiset.count_map_eq_count
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
exact count_map_eq_count f _ hf.injOn _ H

Premises used: Function.Injective.injOn, Multiset.count_map_eq_count
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
neg : ¬∃ (a : α), a ∈ s ∧ f a = f x
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count_eq_zero_of_notMem H, count_eq_zero, mem_map]

Premises used: Multiset.mem_map, Multiset.count_eq_zero_of_notMem, Multiset.count_eq_zero
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : k ∈ s
hkx : f k = f x
⊢ x ∈ s

Tactic:
rw [hf hkx] at hks
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : k ∈ s
hkx : f k = f x
hks₁ : x ∈ s
⊢ f k = f x

Tactic:
rw [hf hkx] at hks
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : x ∈ s
hkx : f k = f x
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
b : α
l : List α
simp : (↑(List.filter (fun (b_1 : α) ↦ decide (b_1 = b)) l) : Multiset α) = replicate (List.count b l) b
⊢ filter (fun (x : α) ↦ x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b

Tactic:
simp only [quot_mk_to_coe, filter_coe, coe_count]

Premises used: Multiset.coe_count, Multiset.quot_mk_to_coe, Multiset.filter_coe
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
b : α
l : List α
rw : (↑(List.replicate (List.count b l) b) : Multiset α) = replicate (List.count b l) b
rw₁ rw₂ : replicate (List.count b l) b = replicate (List.count b l) b
⊢ (↑(List.filter (fun (b_1 : α) ↦ decide (b_1 = b)) l) : Multiset α) = replicate (List.count b l) b

Tactic:
rw [List.filter_eq, coe_replicate]

Premises used: List.filter_eq, Multiset.coe_replicate
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
b : α
simp_rw : filter (Eq b) s = filter (fun (x : α) ↦ x = b) s
⊢ filter (Eq b) s = replicate (count b s) b

Tactic:
simp_rw [← filter_eq', eq_comm]

Premises used: eq_comm, Multiset.filter_eq'
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s t : Multiset α
revert : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
⊢ filter p (s - t) = filter p s - filter p t

Tactic:
revert s
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - 0) = filter p s - filter p 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t : Multiset α
refine :
  ∀ (a : α) (t : Multiset α) (IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t) (s : Multiset α),
    filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t

Tactic:
refine Multiset.induction_on t (by simp) fun a t IH s => ?_
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
rw : filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)

Tactic:
rw [sub_cons, IH]

Premises used: Multiset.sub_cons
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
pos : ∀ (h : p a), filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
neg : ∀ (h : ¬p a), filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
by_cases h : p a
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
pos : filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
rw [filter_cons_of_pos _ h, sub_cons]

Premises used: Multiset.sub_cons, Multiset.filter_cons_of_pos
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
pos : filter p (s.erase a) = (filter p s).erase a
⊢ filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t

Tactic:
congr
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
pos : ∀ (m : a ∈ s), filter p (s.erase a) = (filter p s).erase a
neg : ∀ (m : ¬a ∈ s), filter p (s.erase a) = (filter p s).erase a
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
by_cases m : a ∈ s
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∈ s
pos : a ::ₘ filter p (s.erase a) = a ::ₘ (filter p s).erase a
pos₁ : filter p (a ::ₘ s.erase a) = a ::ₘ (filter p s).erase a
pos₂ : filter p (a ::ₘ s.erase a) = filter p s
pos₃ pos₄ : filter p s = filter p s
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]

Premises used: Multiset.cons_erase, Multiset.filter_cons_of_pos, Multiset.cons_inj_right, Multiset.mem_filter_of_mem
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
neg : filter p s = (filter p s).erase a
neg₁ neg₂ : filter p s = filter p s
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]

Premises used: mt, Multiset.mem_of_mem_filter, Multiset.erase_of_notMem
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
neg : filter p (s.erase a) - filter p t = filter p s - filter p t
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
rw [filter_cons_of_neg _ h]

Premises used: Multiset.filter_cons_of_neg
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
pos : ∀ (m : a ∈ s), filter p (s.erase a) - filter p t = filter p s - filter p t
neg : ∀ (m : ¬a ∈ s), filter p (s.erase a) - filter p t = filter p s - filter p t
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
by_cases m : a ∈ s
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
rw rw₁ : filter p (s.erase a) = filter p (s.erase a)
⊢ filter p (s.erase a) = filter p (a ::ₘ s.erase a)

Tactic:
rw [filter_cons_of_neg _ h]

Premises used: Multiset.filter_cons_of_neg
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
rw : filter p (s.erase a) = filter p (a ::ₘ s.erase a)
pos : filter p (a ::ₘ s.erase a) - filter p t = filter p s - filter p t
pos₁ pos₂ : filter p s - filter p t = filter p s - filter p t
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
        cons_erase m]

Premises used: Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
neg neg₁ : filter p s - filter p t = filter p s - filter p t
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
rw [erase_of_notMem m]

Premises used: Multiset.erase_of_notMem
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s : Multiset α
a : ∀ (a : α), count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
⊢ s - filter p s = filter (fun (a : α) ↦ ¬p a) s

Tactic:
ext a
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s : Multiset α
a : α
pos : ∀ (h : p a), count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
neg : ∀ (h : ¬p a), count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
⊢ count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)

Tactic:
by_cases h : p a
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s : Multiset α
a : α
h : p a
⊢ count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s : Multiset α
a : α
h : ¬p a
⊢ count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩

Premises used: Iff.mpr, Multiset.le_iff_count, Multiset.map_le_map, Iff.intro
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
refine : ∀ (h : map f s ≤ map f t) (a : α), count a s ≤ count a t
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t

Tactic:
simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

Premises used: Multiset.le_iff_count, Iff.mp, Multiset.count_map_eq_count'
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
refine : ∀ (h : map f s ≤ map f t) (a : α), count a s ≤ count a t
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
classical
    refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
    simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
rw : countP (fun (x : α) ↦ a = x) s = (filter (fun (x : α) ↦ a = x) s).card
rw₁ rw₂ : (filter (fun (x : α) ↦ a = x) s).card = (filter (fun (x : α) ↦ a = x) s).card
⊢ count a s = (filter (fun (x : α) ↦ a = x) s).card

Tactic:
rw [count, countP_eq_card_filter]

Premises used: Multiset.count, Multiset.countP_eq_card_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p : α → Prop
inst : DecidablePred p
⊢ count True (map p s) = (filter p s).card

Tactic:
simp only [count_eq_card_filter_eq, filter_map, card_map, Function.id_comp,
    eq_true_eq_id, Function.comp_apply]

Premises used: Multiset.count_eq_card_filter_eq, Multiset.filter_map, Function.comp_apply, eq_true_eq_id, Multiset.card_map, Function.id_comp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p : { a : α // a ∈ s } → Prop
inst : DecidableEq α
inst_1 : DecidablePred p
⊢ filter p s.attach =
    map
      (Subtype.map (p := fun (x : α) ↦
        x ∈ filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s) (q := Membership.mem s) id ⋯)
      (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach

Tactic:
Multiset.map_injective Subtype.val_injective ?_

Premises used: Subtype.val_injective, Multiset.map_injective
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p : { a : α // a ∈ s } → Prop
inst : DecidableEq α
inst_1 : DecidablePred p
refine :
  map (val (p := fun (a : α) ↦ a ∈ s)) (filter p s.attach) =
    map (α := { a : α // a ∈ s }) (val (p := fun (a : α) ↦ a ∈ s))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s) (q := Membership.mem s) id
          ⋯)
        (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)
⊢ filter p s.attach =
    map
      (Subtype.map (p := fun (x : α) ↦
        x ∈ filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s) (q := Membership.mem s) id ⋯)
      (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach

Tactic:
refine Multiset.map_injective Subtype.val_injective ?_

Premises used: Subtype.val_injective, Multiset.map_injective
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p : { a : α // a ∈ s } → Prop
inst : DecidableEq α
inst_1 : DecidablePred p
rw :
  filter (fun (b : α) ↦ ∃ (a : { a : α // a ∈ s }), p a ∧ (↑a : α) = b)
      (map (val (p := fun (a : α) ↦ a ∈ s)) s.attach) =
    map (α := { a : α // a ∈ s }) (val (p := fun (a : α) ↦ a ∈ s))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s) (q := Membership.mem s) id
          ⋯)
        (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)
⊢ map (val (p := fun (a : α) ↦ a ∈ s)) (filter p s.attach) =
    map (α := { a : α // a ∈ s }) (val (p := fun (a : α) ↦ a ∈ s))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s) (q := Membership.mem s) id
          ⋯)
        (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)

Tactic:
rw [map_filter' _ Subtype.val_injective]

Premises used: Subtype.val_injective, Multiset.map_filter'
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p : { a : α // a ∈ s } → Prop
inst : DecidableEq α
inst_1 : DecidablePred p
⊢ filter (fun (b : α) ↦ ∃ (a : { a : α // a ∈ s }), p a ∧ (↑a : α) = b)
      (map (val (p := fun (a : α) ↦ a ∈ s)) s.attach) =
    map (α := { a : α // a ∈ s }) (val (p := fun (a : α) ↦ a ∈ s))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s) (q := Membership.mem s) id
          ⋯)
        (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)

Tactic:
simp only [Function.comp, Subtype.exists, Subtype.map,
    exists_and_right, exists_eq_right, attach_map_val, map_map, id]

Premises used: Subtype.map, Multiset.attach_map_val, Function.comp, Subtype.exists, exists_eq_right, id, exists_and_right, Multiset.map_map