awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n ↔ ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a
have mp : (filter P s).card ≤ n → ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ (filter P s).card ≤ n ↔ ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a
have mpr : (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ ∃ (a : α), a ∈ s' ∧ ¬P a
have mp : ∀ (rid : ∀ (a : α) (_ : a ∈ s'), P a), False
Tactic: by_contra! rid
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (hypothesis)
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
⊢ False
have card : (filter P s').card ≤ n
Tactic: have card := card_le_card (monotone_filter_left P hs') |>.trans H
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
s : Multiset α
P : α → Prop
inst : DecidablePred P
n : ℕ
⊢ (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n
have mpr : n < (filter P s).card → ∃ (s' : Multiset α), s' ≤ s ∧ n < s'.card ∧ ∀ (a : α) (_ : a ∈ s'), P a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
⊢ filterMap f (a ::ₘ s) = Option.getD (Option.map singleton (f a)) 0 + filterMap f s
have cases : ∀ (x : Option β) (h : f a = x), filterMap f (a ::ₘ s) = Option.getD (Option.map singleton x) 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard fun (b : α) ↦ decide (p b)) l = List.filter (fun (b : α) ↦ decide (p b)) l
have rw : List.filterMap (Option.guard fun (b : α) ↦ decide (p b)) l = List.filterMap (Option.guard fun (x : α) ↦ decide (p x)) l
Tactic: rw [← List.filterMap_eq_filter]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ map f (filter p (a ::ₘ s)) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) (a ::ₘ s)
have 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)
Tactic: simp only [filter_cons, map_add, ih, filterMap_cons, Option.map_if]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
⊢ 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)
have pos : p a → Eq (α := Multiset β) (map (fun (x : α) ↦ f x) {a}) (Option.getD (some {f a}) 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ 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)
have neg : ¬p a → Eq.{v + 1} (α := Multiset β) (map (fun (x : α) ↦ f x) 0) (Option.getD none 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ map f (filter p s) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) s
have empty : map f (filter p 0) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) 0
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ map f (filter p s) = filterMap (fun (a : α) ↦ if p a then some (f a) else none) s
have 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)
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
s : Multiset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
l : List α
⊢ 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))
have 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)
Tactic: convert! l.countP_eq_countP_filter_add (p ·) (q ·)
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
have refine_1 : countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
Tactic: refine Multiset.induction_on s ?_ fun a t IH => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ countP p (map f s) = (filter (fun (a : α) ↦ p (f a)) s).card
have 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
Tactic: refine Multiset.induction_on s ?_ fun a t IH => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst : DecidablePred p
⊢ countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
have refine_1 : countP p 0 = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
Tactic: rw [map_zero, countP_zero, filter_zero, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
have refine_1₁ : 0 = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
Tactic: rw [map_zero, countP_zero, filter_zero, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
have refine_1₂ : 0 = card.{u_1} (α := α) 0
Tactic: rw [map_zero, countP_zero, filter_zero, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f 0) = card.{u_1} (α := α) (filter (fun (a : α) ↦ p (f a)) 0)
have refine_1₃ : Eq (α := ℕ) 0 0
Tactic: rw [map_zero, countP_zero, filter_zero, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have refine_2 : countP p (f a ::ₘ map f 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have refine_2₁ : (countP p (map f t) + if p (f a) then 1 else 0) = (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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ countP p (map f (a ::ₘ t)) = (filter (fun (a : α) ↦ p (f a)) (a ::ₘ t)).card
have 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
Tactic: rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ count a (filter p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l)) =
    count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l)
have simp : List.count a (List.filter (fun (b : α) ↦ decide (p b)) _l) = List.count a _l
Tactic: simp only [quot_mk_to_coe'', filter_coe, coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ List.count a (List.filter (fun (b : α) ↦ decide (p b)) _l) = List.count a _l
have h₁ : decide (p a) = true
Tactic: apply count_filter
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0
have pos : ∀ (h : p a), count a (filter p s) = count a s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ count a (filter p s) = if p a then count a s else 0
have neg : ∀ (h : ¬p a), count a (filter p s) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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 (f x) (map f s) = count x s
have rw : count x (filter (fun (a : α) ↦ f x = f a) s) = count x s
Tactic: rw [count, countP_map, ← this]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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 (f x) (map f s) = count x s
have suffices : count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
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
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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 (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
have 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
Tactic: rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ count x (filter (fun (a : α) ↦ f x = f a) s) = (filter (fun (a : α) ↦ f x = f a) s).card
have rw₁ : ∀ (b : α) (hb : b ∈ filter (fun (a : α) ↦ f x = f a) s), f x = f b
Tactic: rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
⊢ count (f x) (map f s) = count x s
have pos : ∀ (H : x ∈ s), count (f x) (map f s) = count x s
Tactic: by_cases H : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ count (f x) (map f s) = count x s
have neg : ∀ (H : ¬x ∈ s), count (f x) (map f s) = count x s
Tactic: by_cases H : x ∈ s