awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s
have neg : ¬∃ (a : α), a ∈ s ∧ f a = f x
Tactic: rw [count_eq_zero_of_notMem H, count_eq_zero, mem_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (hypothesis)
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
⊢ False
have hks₁ : x ∈ s
Tactic: rw [hf hkx] at hks
Cleared hypotheses: hks, hkx
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun (x : α) ↦ x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b
have simp : (↑(List.filter (fun (b_1 : α) ↦ decide (b_1 = b)) l) : Multiset α) = replicate (List.count b l) b
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 α
s : Multiset α
b : α
l : List α
⊢ (↑(List.filter (fun (b_1 : α) ↦ decide (b_1 = b)) l) : Multiset α) = replicate (List.count b l) b
have rw : (↑(List.replicate (List.count b l) b) : Multiset α) = replicate (List.count b l) b
Tactic: rw [List.filter_eq, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ (↑(List.filter (fun (b_1 : α) ↦ decide (b_1 = b)) l) : Multiset α) = replicate (List.count b l) b
have rw₁ : replicate (List.count b l) b = replicate (List.count b l) b
Tactic: rw [List.filter_eq, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b
have simp_rw : filter (Eq b) s = filter (fun (x : α) ↦ x = b) s
Tactic: simp_rw [← filter_eq', eq_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s t : Multiset α
⊢ filter p (s - t) = filter p s - filter p t
have revert : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
Tactic: revert s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
have 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)
Tactic: refine Multiset.induction_on t (by simp) fun a t IH s => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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 α
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)
have rw : filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
Tactic: rw [sub_cons, IH]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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 α
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
have pos : ∀ (h : p a), filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
have neg : ∀ (h : ¬p a), filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
have pos : filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t
Tactic: rw [filter_cons_of_pos _ h, sub_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t
have pos : filter p (s.erase a) = (filter p s).erase a
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have pos : ∀ (m : a ∈ s), filter p (s.erase a) = (filter p s).erase a
Tactic: by_cases m : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have neg : ∀ (m : ¬a ∈ s), filter p (s.erase a) = (filter p s).erase a
Tactic: by_cases m : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have pos : a ::ₘ filter p (s.erase a) = 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have pos₁ : filter p (a ::ₘ s.erase a) = 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have pos₂ : filter p (a ::ₘ s.erase a) = filter p s
Tactic: rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have pos₃ : filter p s = filter p s
Tactic: rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have neg : filter p s = (filter p s).erase a
Tactic: rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = (filter p s).erase a
have neg₁ : filter p s = filter p s
Tactic: rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
have neg : filter p (s.erase a) - filter p t = filter p s - filter p t
Tactic: rw [filter_cons_of_neg _ h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
have pos : ∀ (m : a ∈ s), filter p (s.erase a) - filter p t = filter p s - filter p t
Tactic: by_cases m : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
have neg : ∀ (m : ¬a ∈ s), filter p (s.erase a) - filter p t = filter p s - filter p t
Tactic: by_cases m : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) = filter p (a ::ₘ s.erase a)
have rw : filter p (s.erase a) = filter p (s.erase a)
Tactic: rw [filter_cons_of_neg _ h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
have rw : filter p (s.erase a) = filter p (a ::ₘ s.erase a)
Tactic: rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
        cons_erase m]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
have pos : filter p (a ::ₘ 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
have pos₁ : filter p s - 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t
have neg : filter p s - filter p t = filter p s - filter p t
Tactic: rw [erase_of_notMem m]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s : Multiset α
⊢ s - filter p s = filter (fun (a : α) ↦ ¬p a) s
have a : ∀ (a : α), count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
have pos : ∀ (h : p a), count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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)
⊢ count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
have neg : ∀ (h : ¬p a), count a (s - filter p s) = count a (filter (fun (a : α) ↦ ¬p a) s)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t
have refine : ∀ (h : map f s ≤ map f t) (a : α), count a s ≤ count a t
Tactic: refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t
have refine : ∀ (h : map f s ≤ map f t) (a : α), count a s ≤ count a 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)
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ count a s = (filter (fun (x : α) ↦ a = x) s).card
have rw : countP (fun (x : α) ↦ a = x) s = (filter (fun (x : α) ↦ a = x) s).card
Tactic: rw [count, countP_eq_card_filter]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
rw : countP (fun (x : α) ↦ a = x) s = (filter (fun (x : α) ↦ a = x) s).card
⊢ count a s = (filter (fun (x : α) ↦ a = x) s).card
have rw₁ : (filter (fun (x : α) ↦ a = x) s).card = (filter (fun (x : α) ↦ a = x) s).card
Tactic: rw [count, countP_eq_card_filter]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
have 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 sorry)
      (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 ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
s : Multiset α
p : { a : α // a ∈ s } → Prop
inst : DecidableEq α
inst_1 : DecidablePred p
⊢ 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)
have 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 sorry)
      (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)
Tactic: rw [map_filter' _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
have 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 sorry)
      (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)
Tactic: classical
  refine Multiset.map_injective Subtype.val_injective ?_
  rw [map_filter' _ Subtype.val_injective]
  simp only [Function.comp, Subtype.exists, Subtype.map,
    exists_and_right, exists_eq_right, attach_map_val, map_map, id]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
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
have refine₁ : 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 sorry)
      (filter (fun (x : α) ↦ ∃ (h : x ∈ s), p (mk (p := fun (a : α) ↦ a ∈ s) x h)) s).attach)
Tactic: classical
  refine Multiset.map_injective Subtype.val_injective ?_
  rw [map_filter' _ Subtype.val_injective]
  simp only [Function.comp, Subtype.exists, Subtype.map,
    exists_and_right, exists_eq_right, attach_map_val, map_map, id]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
have rw : a ∈ Multiset.filter (fun (x : α) ↦ x ≠ b) l ↔ a ≠ b ∧ a ∈ l
Tactic: rw [d.erase_eq_filter b, mem_filter, and_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
rw : a ∈ Multiset.filter (fun (x : α) ↦ x ≠ b) l ↔ a ≠ b ∧ a ∈ l
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
have rw₁ : a ∈ l ∧ a ≠ b ↔ a ≠ b ∧ a ∈ l
Tactic: rw [d.erase_eq_filter b, mem_filter, and_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
rw : a ∈ Multiset.filter (fun (x : α) ↦ x ≠ b) l ↔ a ≠ b ∧ a ∈ l
rw₁ : a ∈ l ∧ a ≠ b ↔ a ≠ b ∧ a ∈ l
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
have rw₂ : a ≠ b ∧ a ∈ l ↔ a ≠ b ∧ a ∈ l
Tactic: rw [d.erase_eq_filter b, mem_filter, and_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup
have pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup = ndinsert a s.dedup
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup = ndinsert a s.dedup
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup
have neg : ∀ (h : ¬a ∈ s), (a ::ₘ s).dedup = ndinsert a s.dedup
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
t : Multiset α
ht : ndinsert a s = t
⊢ t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
have pos : ∀ (h : a ∈ s),
  t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a sorry)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) sorry) s.attach)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.FinsetOps (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
eq :
  ∀ (h : ∀ (p : { x : α // x ∈ s }), (↑p : α) ∈ s),
    Eq.{u_1 + 1} (α := (p : { x : α // x ∈ s }) → { x : α // x ∈ s })
      (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) id
t : Multiset α
ht : ndinsert a s = t
pos :
  ∀ (h : a ∈ s),
    t.attach =
      ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
        (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
⊢ t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) ⋯) s.attach)
have neg : ∀ (h : ¬a ∈ s),
  t.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a sorry)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑p : α) sorry) s.attach)
Tactic: by_cases h : a ∈ s