awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
          ⋯)
        (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:
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]

Premises used: Subtype.map, Subtype.val_injective, Multiset.attach_map_val, Function.comp, Subtype.exists, exists_eq_right, id, exists_and_right, Multiset.map_injective, Multiset.map_map, Multiset.map_filter'
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ s.Nodup → (Multiset.filter p s).Nodup

Tactic:
Quot.induction_on s fun _ => List.Nodup.filter (p ·)

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
x : List α
d : Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) x)
⊢ x.erase a = List.filter (fun (b : α) ↦ decide ((fun (x : α) ↦ x ≠ a) b)) x

Tactic:
simpa using List.Nodup.erase_eq_filter d a

Premises used: List.Nodup.erase_eq_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → Option β
H : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
⊢ s.Nodup → (filterMap f s).Nodup

Tactic:
Quot.induction_on s fun _ => List.Nodup.filterMap H

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Filter
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
rw₂ rw₃ : a ≠ b ∧ a ∈ l ↔ a ≠ b ∧ a ∈ l
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Tactic:
rw [d.erase_eq_filter b, mem_filter, and_comm]

Premises used: Multiset.Nodup.erase_eq_filter, and_comm, Multiset.mem_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : s.Nodup
⊢ ¬a ∈ s.erase a

Tactic:
fun ha =>
  (h.mem_erase_iff.1 ha).1 rfl

Premises used: And.left, Multiset.Nodup.mem_erase_iff, Iff.mp, Not, rfl
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ ndinsert a (↑l : Multiset α) = (↑(insert a l) : Multiset α)

Tactic:
rfl

Premises used: Multiset.ndinsert, rfl
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ ndinsert a 0 = {a}

Tactic:
rfl

Premises used: Multiset.cons, Multiset.ofList, Multiset.ndinsert, rfl, ite
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s → ndinsert a s = s

Tactic:
Quot.inductionOn s fun _ h => congr_arg ((↑) : List α → Multiset α) <| insert_of_mem h

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ ¬a ∈ s → ndinsert a s = a ::ₘ s

Tactic:
Quot.inductionOn s fun _ h => congr_arg ((↑) : List α → Multiset α) <| insert_of_not_mem h

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
⊢ a ∈ ndinsert b s ↔ a = b ∨ a ∈ s

Tactic:
Quot.inductionOn s fun _ => mem_insert_iff

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ s ≤ ndinsert a s

Tactic:
Quot.inductionOn s fun _ => (sublist_insert _ _).subperm

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ ndinsert a s

Tactic:
simp
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
h : a ∈ s
⊢ a ∈ ndinsert b s

Tactic:
mem_ndinsert.2 (Or.inr h)

Premises used: Iff.mpr, Multiset.mem_ndinsert, Or.inr
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (ndinsert a s).card = s.card

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (ndinsert a s).card = s.card + 1

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
pos : ∀ (h : a ∈ s), (a ::ₘ s).dedup = ndinsert a s.dedup
neg : ∀ (h : ¬a ∈ s), (a ::ₘ s).dedup = ndinsert a s.dedup
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
simp [h]
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ s.Nodup → (Multiset.ndinsert a s).Nodup

Tactic:
Quot.inductionOn s fun _ => Nodup.insert

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h_1 : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∈ s
⊢ ndinsert a s ≤ t

Tactic:
simp [h, l]
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h_1 : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
rw : s ≤ t
⊢ ndinsert a s ≤ t

Tactic:
rw [ndinsert_of_notMem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_notMem h,
          cons_erase m]

Premises used: Multiset.ndinsert_of_notMem, Multiset.cons_erase, Multiset.le_cons_of_notMem, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h_1 : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t

Tactic:
l
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h_1 : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t

Tactic:
exact l
-- Module: Mathlib.Data.Multiset.FinsetOps
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)
neg :
  ∀ (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)

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Multiset.FinsetOps
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
h : a ∈ s
⊢ s = t

Tactic:
rw [ndinsert_of_mem h] at ht

Premises used: Multiset.ndinsert_of_mem
-- Module: Mathlib.Data.Multiset.FinsetOps
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
h : a ∈ s
ht₁ : s = t
⊢ a ∈ s

Tactic:
rw [ndinsert_of_mem h] at ht

Premises used: Multiset.ndinsert_of_mem
-- Module: Mathlib.Data.Multiset.FinsetOps
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_1 : ndinsert a s = t
ht : s = t
h : a ∈ s
pos :
  ∀ (ht : ndinsert a s = s),
    s.attach =
      ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯)
        (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑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)

Tactic:
subst ht
-- Module: Mathlib.Data.Multiset.FinsetOps
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
h : a ∈ s
ht : ndinsert a s = s
pos : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯) (map id s.attach)
pos₁ : s.attach = ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯) s.attach
pos₂ pos₃ : s.attach = s.attach
⊢ s.attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑p : α) ⋯) s.attach)

Tactic:
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]

Premises used: Multiset.map_id, Multiset.mem_attach, Multiset.ndinsert_of_mem
-- Module: Mathlib.Data.Multiset.FinsetOps
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
h : ¬a ∈ s
⊢ a ::ₘ s = t

Tactic:
rw [ndinsert_of_notMem h] at ht

Premises used: Multiset.ndinsert_of_notMem
-- Module: Mathlib.Data.Multiset.FinsetOps
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
h : ¬a ∈ s
ht₁ : a ::ₘ s = t
⊢ ¬a ∈ s

Tactic:
rw [ndinsert_of_notMem h] at ht

Premises used: Multiset.ndinsert_of_notMem
-- Module: Mathlib.Data.Multiset.FinsetOps
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_1 : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
neg :
  ∀ (ht : ndinsert a s = a ::ₘ s),
    (a ::ₘ s).attach =
      ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ a ::ₘ s) a ⋯)
        (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ a ::ₘ s) (↑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)

Tactic:
subst ht
-- Module: Mathlib.Data.Multiset.FinsetOps
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
h : ¬a ∈ s
ht : ndinsert a s = a ::ₘ s
⊢ (a ::ₘ s).attach =
    ndinsert (Subtype.mk (p := fun (x : α) ↦ x ∈ a ::ₘ s) a ⋯)
      (map (fun (p : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ a ::ₘ s) (↑p : α) ⋯) s.attach)

Tactic:
simp [attach_cons, h]

Premises used: Multiset.attach_cons
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint (ndinsert a s) t ↔ _root_.Disjoint (a ::ₘ s) t

Tactic:
simp [disjoint_left]

Premises used: Multiset.disjoint_left
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
rw : ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
⊢ _root_.Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_ndinsert_left]

Premises used: disjoint_comm, Multiset.disjoint_ndinsert_left
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
mp : ¬a ∈ s ∧ _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mpr : ¬a ∈ s ∧ _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mp₁ mp₂ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s ∧ _root_.Disjoint s t
mp₃ : ¬a ∈ s → _root_.Disjoint t s → ¬a ∈ s
mp₄ : ¬a ∈ s → _root_.Disjoint t s → _root_.Disjoint s t
mpr₁ mpr₂ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s ∧ _root_.Disjoint t s
mpr₃ : ¬a ∈ s → _root_.Disjoint s t → ¬a ∈ s
mpr₄ : ¬a ∈ s → _root_.Disjoint s t → _root_.Disjoint t s
mp₅ mp₆ mp₇ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mpr₅ mpr₆ mpr₇ : ¬a ∈ s → _root_.Disjoint s t → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mp₈ mp₉ mp₁₀ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mpr₈ mpr₉ mpr₁₀ : ¬a ∈ s → _root_.Disjoint s t → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mp₁₁ mp₁₂ mp₁₃ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mpr₁₁ mpr₁₂ mpr₁₃ : ¬a ∈ s → _root_.Disjoint s t → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mp₁₄ mp₁₅ : ¬a ∈ s → _root_.Disjoint t s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mpr₁₄ mpr₁₅ : ¬a ∈ s → _root_.Disjoint s t → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
tauto
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁ : Multiset α).ndunion (↑l₂ : Multiset α) = (↑(l₁ ∪ l₂) : Multiset α)

Tactic:
rfl

Premises used: Multiset.ndunion, rfl
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ ndunion 0 s = s

Tactic:
Quot.inductionOn s fun _ => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ (a ::ₘ s).ndunion t = ndinsert a (s.ndunion t)

Tactic:
Quot.induction_on₂ s t fun _ _ => rfl

Premises used: Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s.ndunion t ↔ a ∈ s ∨ a ∈ t

Tactic:
Quot.induction_on₂ s t fun _ _ => List.mem_union_iff

Premises used: Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t ≤ s.ndunion t

Tactic:
Quot.induction_on₂ s t fun _ _ => (suffix_union_right _ _).sublist.subperm

Premises used: Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t ⊆ s.ndunion t

Tactic:
subset_of_le (le_ndunion_right s t)

Premises used: Multiset.subset_of_le, Multiset.le_ndunion_right
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndunion t ≤ s + t

Tactic:
Quot.induction_on₂ s t fun _ _ => (union_sublist_append _ _).subperm

Premises used: Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u

Tactic:
simp [zero_ndunion]

Premises used: Multiset.zero_ndunion
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
x : α
x_1 : Multiset α
h : x_1.ndunion t ≤ u ↔ x_1 ⊆ u ∧ t ≤ u
⊢ (x ::ₘ x_1).ndunion t ≤ u ↔ x ::ₘ x_1 ⊆ u ∧ t ≤ u

Tactic:
simp only [cons_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h,
        and_assoc]

Premises used: Multiset.cons_subset, and_left_comm, Multiset.cons_ndunion, and_comm, and_assoc, Multiset.ndinsert_le
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ⊆ s.ndunion t

Tactic:
fun _ h =>
  mem_ndunion.2 <| Or.inl h

Premises used: Iff.mpr, Multiset.mem_ndunion, Or.inl, Multiset.Subset
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ s ≤ s.ndunion t

Tactic:
(le_iff_subset d).2 <| subset_ndunion_left _ _

Premises used: Multiset.le_iff_subset, Iff.mpr, Multiset.subset_ndunion_left
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.ndunion t ≤ s ∪ t

Tactic:
ndunion_le.2 ⟨subset_of_le le_union_left, le_union_right⟩

Premises used: Iff.mpr, Multiset.subset_of_le, Multiset.le_union_right, Multiset.ndunion_le, Multiset.le_union_left, And.intro
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t.Nodup → (s.ndunion t).Nodup

Tactic:
Quot.induction_on₂ s t fun _ _ => List.Nodup.union _

Premises used: Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ s.ndunion t = s ∪ t

Tactic:
le_antisymm (ndunion_le_union _ _) <| union_le (le_ndunion_left _ d) (le_ndunion_right _ _)

Premises used: Multiset.ndunion_le_union, le_antisymm, Multiset.union_le, Multiset.le_ndunion_left, Multiset.le_ndunion_right
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ (s + t).dedup = s.ndunion t.dedup

Tactic:
Quot.induction_on₂ s t fun _ _ => congr_arg ((↑) : List α → Multiset α) <| dedup_append _ _

Premises used: Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
h₁ :
  ∀ (a b : List α)
    (h :
      _root_.Disjoint (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
    ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
      dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) + Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b
⊢ s.ndunion t = s.dedup + t

Tactic:
induction s, t using Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  _root_.Disjoint (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ a.Disjoint b

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  _root_.Disjoint (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) + Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq <| by simpa using h

Premises used: congr_arg, Multiset.ofList, List.Disjoint.union_eq
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ⊆ t
h₁ :
  ∀ (a b : List α)
    (h :
      Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)),
    ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
      Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b
⊢ s.ndunion t = t

Tactic:
induction s, t using Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b

Tactic:
congr_arg ((↑) : List α → Multiset α) <| List.Subset.union_eq_right h

Premises used: List.Subset.union_eq_right, congr_arg, Multiset.ofList, Multiset.ndunion
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a b : List α
h :
  Subset (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ ndunion (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b) =
    Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.union_eq_right h

Premises used: List.Subset.union_eq_right, congr_arg, Multiset.ofList
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
simp : List.filter (fun (b : α) ↦ elem b l₂) l₁ ~ l₁ ∩ l₂
⊢ (↑l₁ : Multiset α).ndinter (↑l₂ : Multiset α) = (↑(l₁ ∩ l₂) : Multiset α)

Tactic:
simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]

Premises used: Multiset.mem_coe, Multiset.coe_eq_coe, List.elem_eq_mem, Multiset.filter_coe, Multiset.ndinter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ List.filter (fun (b : α) ↦ elem b l₂) l₁ ~ l₁ ∩ l₂

Tactic:
apply Perm.refl

Premises used: List.Perm.refl
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ ndinter 0 s = 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, List.filter, Multiset.ndinter, rfl, Multiset.filter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s).ndinter t = a ::ₘ s.ndinter t

Tactic:
simp [ndinter, h]

Premises used: Multiset.ndinter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s).ndinter t = s.ndinter t

Tactic:
simp [ndinter, h]

Premises used: Multiset.ndinter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t

Tactic:
simp [ndinter, mem_filter]

Premises used: Multiset.mem_filter, Multiset.ndinter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.Nodup → (s.ndinter t).Nodup

Tactic:
Nodup.filter _

Premises used: Multiset.Nodup.filter, Multiset.ndinter
-- Module: Mathlib.Data.Multiset.FinsetOps
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u

Tactic:
simp [ndinter, le_filter, subset_iff]

Premises used: Multiset.subset_iff, Multiset.le_filter, Multiset.ndinter