awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
pos :
  p a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
neg :
  ¬p a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases p a
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : p a
pos :
  q a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
neg :
  ¬q a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases q a
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : ¬p a
pos :
  q a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
neg :
  ¬q a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases q a
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : p a
h_1 : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : p a
h_1 : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : ¬p a
h_1 : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : ¬p a
h_1 : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
rw : s + 0 = s
rw₁ : ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)
rw₂ : ∀ (a : α), a ∈ s → p a ∨ ¬p a
⊢ filter p s + filter (fun (a : α) ↦ ¬p a) s = s

Tactic:
rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]

Premises used: Iff.mpr, Multiset.filter_eq_self, Multiset.filter_add_filter, Multiset.filter_eq_nil
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ s + 0 = s

Tactic:
simp only [Multiset.add_zero]

Premises used: Multiset.add_zero
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)

Tactic:
simp [-Bool.not_eq_true, -not_and]

Premises used: Bool.not_eq_true, not_and
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a

Tactic:
simp only [implies_true, Decidable.em]

Premises used: Decidable.em, implies_true
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
p : α → Prop
inst : DecidablePred p
f : β → α
s : Multiset β
l : List β
simp :
  List.map f (List.filter ((fun (b : α) ↦ decide (p b)) ∘ f) l) ~
    List.map f (List.filter ((fun (b : α) ↦ decide (p b)) ∘ f) l)
⊢ filter p (map f (Quot.mk (⇑(isSetoid β) : List β → List β → Prop) l)) =
    map f (filter (p ∘ f) (Quot.mk (⇑(isSetoid β) : List β → List β → Prop) l))

Tactic:
simp [List.filter_map]

Premises used: List.filter_map
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
p : α → Prop
inst : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun (b : α) ↦ decide (p b)) ∘ f) l) ~
    List.map f (List.filter ((fun (b : α) ↦ decide (p b)) ∘ f) l)

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
p : α → Prop
inst : DecidablePred p
f : α → β
hf : Injective f
s : Multiset α
inst_1 : DecidablePred fun (b : β) ↦ ∃ (a : α), p a ∧ f a = b
⊢ map f (filter p s) = filter (fun (b : β) ↦ ∃ (a : α), p a ∧ f a = b) (map f s)

Tactic:
simp [filter_map, hf.eq_iff]

Premises used: Function.Injective.eq_iff, Multiset.filter_map
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
mp : (filter P s).card ≤ n → ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a
mpr : (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n
⊢ (filter P s).card ≤ n ↔ ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a

Tactic:
fconstructor
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
mp : ∀ (rid : ∀ (a : α) (_ : a ∈ s'), P a), False
⊢ ∃ (a : α), a ∈ s' ∧ ¬P a

Tactic:
by_contra! rid
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ (a : α) (_ : a ∈ s'), P a
⊢ (filter P s').card ≤ n

Tactic:
have card := card_le_card (monotone_filter_left P hs') |>.trans H
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ (a : α) (_ : a ∈ s'), P a
card : (filter P s').card ≤ n
⊢ False

Tactic:
s'_card.not_ge (filter_eq_self.mpr rid ▸ card)

Premises used: Iff.mpr, Multiset.filter_eq_self, Eq.rec, LT.lt.not_ge
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ (a : α) (_ : a ∈ s'), P a
card : (filter P s').card ≤ n
⊢ False

Tactic:
exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)

Premises used: Iff.mpr, Multiset.filter_eq_self, Eq.rec, LT.lt.not_ge
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
mpr : n < (filter P s).card → ∃ (s' : Multiset α), s' ≤ s ∧ n < s'.card ∧ ∀ (a : α) (_ : a ∈ s'), P a
⊢ (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n

Tactic:
contrapose!
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
⊢ n < (filter P s).card → ∃ (s' : Multiset α), s' ≤ s ∧ n < s'.card ∧ ∀ (a : α) (_ : a ∈ s'), P a

Tactic:
fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

Premises used: Multiset.filter_le, And.right, And.intro, Exists.intro, Iff.mp, Multiset.mem_filter, Multiset.filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
⊢ n < (filter P s).card → ∃ (s' : Multiset α), s' ≤ s ∧ n < s'.card ∧ ∀ (a : α) (_ : a ∈ s'), P a

Tactic:
exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
l : List α
⊢ filterMap f (↑l : Multiset α) = (↑(List.filterMap f l) : Multiset β)

Tactic:
rfl

Premises used: Multiset.filterMap, rfl
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
⊢ filterMap f 0 = 0

Tactic:
rfl

Premises used: Multiset.filterMap, Multiset.zero, Multiset.ofList, List.filterMap, rfl
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
h : f a = none
⊢ filterMap f (a ::ₘ s) = filterMap f s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList <| List.filterMap_cons_none h

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
b : β
h : f a = some b
⊢ filterMap f (a ::ₘ s) = b ::ₘ filterMap f s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList <| List.filterMap_cons_some h

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
h : f a = none
⊢ filterMap f (a ::ₘ s) = Option.getD (Option.map singleton none) 0 + filterMap f s

Tactic:
simp [filterMap_cons_none a s h]

Premises used: Multiset.filterMap_cons_none
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
b : β
h : f a = some b
⊢ filterMap f (a ::ₘ s) = Option.getD (Option.map singleton (some b)) 0 + filterMap f s

Tactic:
simp [filterMap_cons_some f a s h]

Premises used: Multiset.filterMap_cons_some
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
cases : ∀ (x : Option β) (h : f a = x), filterMap f (a ::ₘ s) = Option.getD (Option.map singleton x) 0 + filterMap f s
⊢ filterMap f (a ::ₘ s) = Option.getD (Option.map singleton (f a)) 0 + filterMap f s

Tactic:
cases h : f a with
  | none => simp [filterMap_cons_none a s h]
  | some b => simp [filterMap_cons_some f a s h]

Premises used: Option.some, Option.none
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
s t : Multiset α
⊢ filterMap f (s + t) = filterMap f s + filterMap f t

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg ofList <| filterMap_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
⊢ filterMap (some ∘ f) = map f

Tactic:
funext fun s =>
    Quot.inductionOn s fun l => congr_arg ofList <| congr_fun List.filterMap_eq_map l

Premises used: Quot.inductionOn, funext
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
l : List α
rw rw₁ :
  List.filterMap (Option.guard fun (b : α) ↦ decide (p b)) l =
    List.filterMap (Option.guard fun (x : α) ↦ decide (p x)) l
⊢ List.filterMap (Option.guard fun (b : α) ↦ decide (p b)) l = List.filter (fun (b : α) ↦ decide (p b)) l

Tactic:
rw [← List.filterMap_eq_filter]

Premises used: List.filterMap_eq_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → Option β
g : β → Option γ
s : Multiset α
⊢ filterMap g (filterMap f s) = filterMap (fun (x : α) ↦ (f x).bind g) s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_filterMap

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → Option β
g : β → γ
s : Multiset α
⊢ map g (filterMap f s) = filterMap (fun (x : α) ↦ Option.map g (f x)) s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList List.map_filterMap

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → β
g : β → Option γ
s : Multiset α
⊢ filterMap g (map f s) = filterMap (g ∘ f) s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_map

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
p : β → Prop
inst : DecidablePred p
s : Multiset α
⊢ filter p (filterMap f s) = filterMap (fun (x : α) ↦ Option.filter (fun (b : β) ↦ decide (p b)) (f x)) s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList List.filter_filterMap

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
p : α → Prop
inst : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun (b : α) ↦ decide (p b)) l) =
    List.filterMap (fun (x : α) ↦ if p x then f x else none) l

Tactic:
simpa using List.filterMap_filter (f := f) (p := p)

Premises used: List.filterMap_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
⊢ filterMap some s = s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_some

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
s : Multiset α
b : β
⊢ b ∈ filterMap f s ↔ ∃ (a : α), a ∈ s ∧ f a = some b

Tactic:
Quot.inductionOn s fun _ => List.mem_filterMap

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
g : β → α
H : ∀ (x : α), Option.map g (f x) = some x
s : Multiset α
⊢ map g (filterMap f s) = s

Tactic:
Quot.inductionOn s fun _ => congr_arg ofList <| List.map_filterMap_of_inv H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → Option β
s t : Multiset α
h : s ≤ t
⊢ filterMap f s ≤ filterMap f t

Tactic:
leInductionOn h fun h => (h.filterMap _).subperm

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
⊢ map f (filter p 0) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
ih : map f (filter p s) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) s
cons :
  HAdd.hAdd (α := Multiset β) (map (fun (x : α) ↦ f x) (if p a then {a} else 0))
      (filterMap (fun (a : α) ↦ if p a then some (f a) else none) s) =
    HAdd.hAdd (α := Multiset β) (Option.getD (if p a then some {f a} else none) 0)
      (filterMap (fun (a : α) ↦ if p a then some (f a) else none) s)
⊢ map f (filter p (a ::ₘ s)) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) (a ::ₘ s)

Tactic:
simp only [filter_cons, map_add, ih, filterMap_cons, Option.map_if]

Premises used: Multiset.filter_cons, Multiset.filterMap_cons, Multiset.map_add, Option.map_if
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
cons :
  Eq (α := Multiset β) (map (fun (x : α) ↦ f x) (if p a then {a} else 0))
    (Option.getD (if p a then some {f a} else none) 0)
⊢ HAdd.hAdd (α := Multiset β) (map (fun (x : α) ↦ f x) (if p a then {a} else 0))
      (filterMap (fun (a : α) ↦ if p a then some (f a) else none) s) =
    HAdd.hAdd (α := Multiset β) (Option.getD (if p a then some {f a} else none) 0)
      (filterMap (fun (a : α) ↦ if p a then some (f a) else none) s)

Tactic:
congr
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
pos : p a → Eq (α := Multiset β) (map (fun (x : α) ↦ f x) {a}) (Option.getD (some {f a}) 0)
neg : ¬p a → Eq.{v + 1} (α := Multiset β) (map (fun (x : α) ↦ f x) 0) (Option.getD none 0)
⊢ Eq (α := Multiset β) (map (fun (x : α) ↦ f x) (if p a then {a} else 0))
    (Option.getD (if p a then some {f a} else none) 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ Eq (α := Multiset β) (map (fun (x : α) ↦ f x) {a}) (Option.getD (some {f a}) 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ Eq.{v + 1} (α := Multiset β) (map (fun (x : α) ↦ f x) 0) (Option.getD none 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
s : Multiset α
empty : map f (filter p 0) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) 0
cons :
  ∀ (a : α) (s : Multiset α) (ih : map f (filter p s) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) s),
    map f (filter p (a ::ₘ s)) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) (a ::ₘ s)
⊢ map f (filter p s) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) s

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons a s ih =>
    simp only [filter_cons, map_add, ih, filterMap_cons, Option.map_if]; clear ih; congr
    split_ifs <;> simp

Premises used: Multiset.filter_cons, Multiset.cons, Multiset.filterMap_cons, Multiset.map_add, Option.map_if
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ countP p s = (filter p s).card

Tactic:
Quot.inductionOn s fun l => l.countP_eq_length_filter (p := (p ·))

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s : Multiset α
⊢ countP p (filter q s) = countP (fun (a : α) ↦ p a ∧ q a) s

Tactic:
simp [countP_eq_card_filter]

Premises used: Multiset.countP_eq_card_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
l : List α
⊢ List.countP (fun (x : α) ↦ decide (p x)) l =
    List.countP (fun (x : α) ↦ decide (p x)) (List.filter (fun (x : α) ↦ decide (q x)) l) +
      List.countP (fun (x : α) ↦ decide (p x)) (List.filter (fun (a : α) ↦ !decide (q a)) l)

Tactic:
l.countP_eq_countP_filter_add (p ·) (q ·)

Premises used: List.countP_eq_countP_filter_add, Decidable.decide
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
l : List α
h :
  countP p (filter (fun (a : α) ↦ ¬q a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)) =
    List.countP (fun (x : α) ↦ decide (p x)) (List.filter (fun (a : α) ↦ !decide (q a)) l)
⊢ countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) =
    countP p (filter q (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)) +
      countP p (filter (fun (a : α) ↦ ¬q a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l))

Tactic:
convert! l.countP_eq_countP_filter_add (p ·) (q ·)

Premises used: List.countP_eq_countP_filter_add, Decidable.decide
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
l : List α
⊢ countP p (filter (fun (a : α) ↦ ¬q a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)) =
    List.countP (fun (x : α) ↦ decide (p x)) (List.filter (fun (a : α) ↦ !decide (q a)) l)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst : DecidablePred p
⊢ countP p (map f s) = (filter (fun (a : α) ↦ p (f a)) s).card

Tactic:
Multiset.induction_on s ?_ fun a t IH => ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst : DecidablePred p
refine_1 : countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
refine_2 :
  ∀ (a : α) (t : Multiset α) (IH : countP p (map f t) = (filter (fun (a : α) ↦ p (f a)) t).card),
    countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
⊢ countP p (map f s) = (filter (fun (a : α) ↦ p (f a)) s).card

Tactic:
refine Multiset.induction_on s ?_ fun a t IH => ?_
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst : DecidablePred p
refine_1 : countP p 0 = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
refine_1₁ : 0 = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
refine_1₂ : 0 = card.{u_1} (α := α) 0
refine_1₃ refine_1₄ : Eq (α := ℕ) 0 0
⊢ countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)

Tactic:
rw [map_zero, countP_zero, filter_zero, card_zero]

Premises used: Multiset.map_zero, Multiset.card_zero, Multiset.filter_zero, Multiset.countP_zero
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun (a : α) ↦ p (f a)) t).card
refine_2 : countP p (f a ::ₘ map f t) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
refine_2₁ : (countP p (map f t) + if p (f a) then 1 else 0) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
refine_2₂ :
  ((filter (fun (a : α) ↦ p (f a)) t).card + if p (f a) then 1 else 0) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
refine_2₃ :
  ((filter (fun (a : α) ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    ((if p (f a) then {a} else 0) + filter (fun (a : α) ↦ p (f a)) t).card
refine_2₄ :
  ((filter (fun (a : α) ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    card (α := α) (if p (f a) then {a} else 0) + (filter (fun (a : α) ↦ p (f a)) t).card
refine_2₅ :
  ((filter (fun (a : α) ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then card (α := α) {a} else card.{u_1} (α := α) 0) + (filter (fun (a : α) ↦ p (f a)) t).card
refine_2₆ :
  ((filter (fun (a : α) ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then card (α := α) {a} else 0) + (filter (fun (a : α) ↦ p (f a)) t).card
refine_2₇ :
  ((filter (fun (a : α) ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then 1 else 0) + (filter (fun (a : α) ↦ p (f a)) t).card
refine_2₈ refine_2₉ :
  (if p (f a) then 1 else 0) + (filter (fun (a : α) ↦ p (f a)) t).card =
    (if p (f a) then 1 else 0) + (filter (fun (a : α) ↦ p (f a)) t).card
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card

Tactic:
rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]

Premises used: Multiset.filter_cons, Multiset.map_cons, Multiset.countP_cons, Multiset.card_add, apply_ite, Multiset.card_singleton, Multiset.card_zero, Multiset.card, Nat.add_comm
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p : α → Prop
inst : DecidablePred p
⊢ filter (fun (a : { a : α // a ∈ s }) ↦ p (↑a : α)) s.attach =
    map (Subtype.map (p := fun (x : α) ↦ x ∈ filter p s) (q := Membership.mem s) id ⋯) (filter p s).attach

Tactic:
Quotient.inductionOn s fun l ↦ congr_arg _ (List.filter_attach l p)

Premises used: Quotient.inductionOn