awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0

Tactic:
count_eq_zero_of_notMem h

Premises used: Multiset.count_eq_zero_of_notMem
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0

Tactic:
exact count_eq_zero_of_notMem h

Premises used: Multiset.count_eq_zero_of_notMem
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ (↑l : Multiset α).dedup = (↑l.dedup : Multiset α)

Tactic:
rfl

Premises used: Multiset.dedup, rfl
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Multiset α) (dedup 0) 0

Tactic:
rfl

Premises used: Multiset.dedup, List.dedup, Multiset.zero, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s.dedup ↔ a ∈ s

Tactic:
Quot.induction_on s fun _ => List.mem_dedup

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s → (a ::ₘ s).dedup = s.dedup

Tactic:
Quot.induction_on s fun _ m => @congr_arg _ _ _ _ ofList <| List.dedup_cons_of_mem m

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ ¬a ∈ s → (a ::ₘ s).dedup = a ::ₘ s.dedup

Tactic:
Quot.induction_on s fun _ m => congr_arg ofList <| List.dedup_cons_of_notMem m

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.dedup ≤ s

Tactic:
Quot.induction_on s fun _ => (dedup_sublist _).subperm

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.dedup ⊆ s

Tactic:
subset_of_le <| dedup_le _

Premises used: Multiset.subset_of_le, Multiset.dedup_le
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s ⊆ s.dedup

Tactic:
fun _ => mem_dedup.2

Premises used: Iff.mpr, Multiset.mem_dedup, Multiset.Subset
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.dedup ⊆ t ↔ s ⊆ t

Tactic:
⟨Subset.trans (subset_dedup _), Subset.trans (dedup_subset _)⟩

Premises used: Multiset.Subset.trans, Iff.intro, Multiset.subset_dedup, Multiset.dedup_subset
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ⊆ t.dedup ↔ s ⊆ t

Tactic:
⟨fun h => Subset.trans h (dedup_subset _), fun h => Subset.trans h (subset_dedup _)⟩

Premises used: Multiset.Subset.trans, Iff.intro, Multiset.subset_dedup, Multiset.dedup_subset
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.dedup.Nodup

Tactic:
Quot.induction_on s List.nodup_dedup

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.dedup = s ↔ s.Nodup

Tactic:
⟨fun e => e ▸ nodup_dedup s, Quot.induction_on s fun _ h => congr_arg ofList h.dedup⟩

Premises used: Eq.rec, Multiset.nodup_dedup, Quot.induction_on, Iff.intro
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
a : α
x : List α
simp : List.count a x.dedup = if a ∈ x then 1 else 0
⊢ count a (dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) x)) =
    if Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) x) a then 1 else 0

Tactic:
simp only [quot_mk_to_coe'', coe_dedup, mem_coe, coe_count]

Premises used: Multiset.coe_count, Multiset.mem_coe, Multiset.coe_dedup, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
a : α
x : List α
⊢ List.count a x.dedup = if a ∈ x then 1 else 0

Tactic:
apply List.count_dedup _ _

Premises used: List.count_dedup
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
⊢ m.dedup.dedup = m.dedup

Tactic:
Quot.induction_on m fun _ => @congr_arg _ _ _ _ ofList List.dedup_idem

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s.dedup = 0 ↔ s = 0

Tactic:
⟨fun h => eq_zero_of_subset_zero <| h ▸ subset_dedup _, fun h => h.symm ▸ dedup_zero⟩

Premises used: Multiset.eq_zero_of_subset_zero, Eq.rec, Multiset.dedup_zero, Iff.intro, Multiset.subset_dedup, Eq.symm
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Multiset α) (dedup {a}) {a}

Tactic:
(nodup_singleton _).dedup

Premises used: Multiset.Nodup.dedup, Multiset.nodup_singleton
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ≤ t.dedup ↔ s ≤ t ∧ s.Nodup

Tactic:
⟨fun h => ⟨le_trans h (dedup_le _), nodup_of_le h (nodup_dedup _)⟩,
   fun ⟨l, d⟩ => (le_iff_subset d).2 <| Subset.trans (subset_of_le l) (subset_dedup _)⟩

Premises used: Multiset.nodup_of_le, Multiset.le_iff_subset, Iff.mpr, Multiset.subset_of_le, _private.0.Multiset.le_dedup.match_1, Multiset.dedup, Multiset.nodup_dedup, Multiset.Subset.trans, LE.le, Multiset.dedup_le, And.intro, Iff.intro, Multiset.subset_dedup, le_trans
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
rw : s ≤ s ∧ s.Nodup ↔ s.Nodup
rw₁ rw₂ : s.Nodup ↔ s.Nodup
⊢ s ≤ s.dedup ↔ s.Nodup

Tactic:
rw [le_dedup, and_iff_right le_rfl]

Premises used: le_rfl, Multiset.le_dedup, and_iff_right
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t

Tactic:
simp [Nodup.ext]

Premises used: Multiset.Nodup.ext
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
s : Multiset α
l : List α
⊢ (map f (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)).dedup =
    map f (dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l))

Tactic:
simp [List.dedup_map_of_injective hf l]

Premises used: List.dedup_map_of_injective
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
⊢ (map f s.dedup).dedup = (map f s).dedup

Tactic:
simp [dedup_ext]

Premises used: Multiset.dedup_ext
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
hno : s.Nodup
⊢ s ≤ t.dedup ↔ s ≤ t

Tactic:
simp [le_dedup, hno]

Premises used: Multiset.le_dedup
-- Module: Mathlib.Data.Multiset.Dedup
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)),
    (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
          (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
      dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ (s + t).dedup = t.dedup

Tactic:
induction s, t using Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.Dedup
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)
⊢ (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)

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

Premises used: Multiset.dedup, List.Subset.dedup_append_right, congr_arg, Multiset.ofList
-- Module: Mathlib.Data.Multiset.Dedup
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)
⊢ (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)

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

Premises used: List.Subset.dedup_append_right, congr_arg, Multiset.ofList
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : t ⊆ s
rw : (t + s).dedup = s.dedup
rw₁ rw₂ : s.dedup = s.dedup
⊢ (s + t).dedup = s.dedup

Tactic:
rw [s.add_comm, Subset.dedup_add_right h]

Premises used: Multiset.add_comm, Multiset.Subset.dedup_add_right
-- Module: Mathlib.Data.Multiset.Dedup
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)),
    (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
          (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
      dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) +
        dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)
⊢ (s + t).dedup = s.dedup + t.dedup

Tactic:
induction s, t using Quot.induction_on₂
-- Module: Mathlib.Data.Multiset.Dedup
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.Dedup
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)
⊢ (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)).dedup =
    dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) +
      dedup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) b)

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

Premises used: List.Disjoint.dedup_append, congr_arg, Multiset.ofList
-- Module: Mathlib.Data.Multiset.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
h : t ⊆ s
rw : (↑(s ++ t).dedup : Multiset α) = (↑s.dedup : Multiset α)
rw₁ : (↑(s ++ t) : Multiset α).dedup = (↑s.dedup : Multiset α)
rw₂ : ((↑s : Multiset α) + (↑t : Multiset α)).dedup = (↑s.dedup : Multiset α)
rw₃ : (↑s : Multiset α).dedup = (↑s.dedup : Multiset α)
rw₄ rw₅ : (↑s.dedup : Multiset α) = (↑s.dedup : Multiset α)
⊢ (s ++ t).dedup ~ s.dedup

Tactic:
rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]

Premises used: Multiset.coe_add, Multiset.coe_eq_coe, Multiset.coe_dedup, Multiset.Subset.dedup_add_left
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ ⟦l⟧ = (↑l : Multiset α)

Tactic:
rfl

Premises used: Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ Quot.mk (fun (x1 x2 : List α) ↦ x1 ≈ x2) l = (↑l : Multiset α)

Tactic:
rfl

Premises used: Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l = (↑l : Multiset α)

Tactic:
rfl

Premises used: Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_3
β : Type u_4
x : List α
f : List α → β
h : ∀ (a b : List α), a ≈ b → f a = f b
⊢ Quotient.lift f h (↑x : Multiset α) = f x

Tactic:
Quotient.lift_mk _ _ _

Premises used: Quotient.lift_mk
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ (↑l₁ : Multiset α) = (↑l₂ : Multiset α) ↔ l₁ ~ l₂

Tactic:
Quotient.eq

Premises used: Multiset, Multiset.ofList, Quotient.eq
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
a : α
l : List α
⊢ a ∈ (↑l : Multiset α) ↔ a ∈ l

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiset.Mem
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ (↑l₁ : Multiset α) ⊆ (↑l₂ : Multiset α) ↔ l₁ ⊆ l₂

Tactic:
Iff.rfl

Premises used: List.Subset, Iff.rfl, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s : Multiset α
⊢ s ⊆ s

Tactic:
fun _ h => h

Premises used: Multiset.Subset
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t u : Multiset α
⊢ s ⊆ t → t ⊆ u → s ⊆ u

Tactic:
fun h₁ h₂ _ m => h₂ (h₁ m)

Premises used: Multiset.Subset
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
⊢ s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiset.Subset
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
a : α
h : s ⊆ t
⊢ a ∈ s → a ∈ t

Tactic:
@h _
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
a : Multiset α
l : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)

Tactic:
Subperm.refl _

Premises used: Multiset.Le, List.Subperm.refl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
a : Multiset α
l : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)

Tactic:
exact Subperm.refl _

Premises used: List.Subperm.refl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
a : Multiset α
l₁ : List α
b : Multiset α
l₂ : List α
c : Multiset α
l₃ : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂) →
    Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₃) →
      Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₃)

Tactic:
@Subperm.trans _ _ _ _

Premises used: Multiset.Le, List.Subperm.trans
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
a : Multiset α
l₁ : List α
b : Multiset α
l₂ : List α
c : Multiset α
l₃ : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂) →
    Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₃) →
      Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
        (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₃)

Tactic:
exact @Subperm.trans _ _ _ _

Premises used: List.Subperm.trans
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
a : Multiset α
l₁ : List α
b : Multiset α
l₂ : List α
h₁ :
  Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)
h₂ :
  Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
⊢ Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)

Tactic:
Quot.sound (Subperm.antisymm h₁ h₂)

Premises used: Quot.sound, Multiset, Quotient, List.Subperm.antisymm
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
a : Multiset α
l₁ : List α
b : Multiset α
l₂ : List α
h₁ :
  Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)
h₂ :
  Multiset.Le (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
⊢ Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)

Tactic:
exact Quot.sound (Subperm.antisymm h₁ h₂)

Premises used: Quot.sound, List.Subperm.antisymm
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
⊢ s ≤ t → s ⊆ t

Tactic:
Quotient.inductionOn₂ s t fun _ _ => Subperm.subset

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
a : α
h : s ≤ t
⊢ a ∈ s → a ∈ t

Tactic:
mem_of_subset (subset_of_le h)

Premises used: Multiset.subset_of_le, Multiset.mem_of_subset
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
a : α
h : s ⊆ t
⊢ ¬a ∈ t → ¬a ∈ s

Tactic:
mt <| @h _

Premises used: mt
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ (↑l₁ : Multiset α) ≤ (↑l₂ : Multiset α) ↔ l₁ <+~ l₂

Tactic:
Iff.rfl

Premises used: Multiset.Le, Iff.rfl, List.Subperm
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
C : Multiset α → Multiset α → Prop
s t : Multiset α
h : s ≤ t
H : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → C (↑l₁ : Multiset α) (↑l₂ : Multiset α)
⊢ C s t

Tactic:
Quotient.inductionOn₂ s t (fun l₁ _ ⟨l, p, s⟩ => (show ⟦l⟧ = ⟦l₁⟧ from Quot.sound p) ▸ H s) h

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).card = l.length

Tactic:
rfl

Premises used: Multiset.card, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
h : s ≤ t
⊢ s.card ≤ t.card

Tactic:
leInductionOn h Sublist.length_le

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
h : s ≤ t
⊢ t.card ≤ s.card → s = t

Tactic:
leInductionOn h fun s h₂ => congr_arg _ <| s.eq_of_length_le h₂

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
h : s < t
⊢ s.card < t.card

Tactic:
lt_of_not_ge fun h₂ => _root_.ne_of_lt h <| eq_of_le_of_card_le (le_of_lt h) h₂

Premises used: lt_of_not_ge, le_of_lt, Multiset.eq_of_le_of_card_le, ne_of_lt
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
⊢ Monotone.{u_1, 0} (α := Multiset α) card

Tactic:
fun _a _b => card_le_card

Premises used: Multiset.card_le_card, Monotone
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
⊢ StrictMono.{u_1, 0} (α := Multiset α) card

Tactic:
fun _ _ ↦ card_lt_card

Premises used: StrictMono, Multiset.card_lt_card
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
⊢ WellFoundedLT.{u_1} (Multiset α)

Tactic:
⟨Subrelation.wf Multiset.card_lt_card (measure Multiset.card).2⟩

Premises used: IsWellFounded.mk, Subrelation.wf, WellFoundedRelation.wf, Multiset.card_lt_card
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ (↑l.reverse : Multiset α) = (↑l : Multiset α)

Tactic:
Quot.sound <| reverse_perm _

Premises used: Quot.sound, Multiset, Multiset.ofList, Quotient, List.reverse_perm
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : (↑l₁ : Multiset α) = s₂
_ :
  ∀ {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
        (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) e H =
      (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)
⊢ ∀ {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
        (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) e H =
      (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)

Tactic:
_
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : (↑l₁ : Multiset α) = s₂
H : ∀ (a : α), a ∈ s₂ → p a
subst :
  ∀ {H : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a},
    Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
        (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) ⋯ H =
      (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)
⊢ Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
      (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) e H =
    (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)

Tactic:
subst e
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
H : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a
⊢ Eq.ndrec (motive := fun (s : Multiset α) ↦ (∀ (a : α), a ∈ s → p a) → Multiset β)
      (fun (x : ∀ (a : α), a ∈ (↑l₁ : Multiset α) → p a) ↦ (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)) ⋯ H =
    (↑(List.pmap (P := p) f l₁ H₁) : Multiset β)

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (p := p) f (↑l : Multiset α) H = (↑(List.pmap (P := p) f l H) : Multiset β)

Tactic:
rfl

Premises used: Multiset.ofList, Multiset.pmap, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
s : Multiset α
⊢ ∀ {H₁ : ∀ (a : α), a ∈ s → p a} {H₂ : ∀ (a : α), a ∈ s → q a},
    (∀ (a : α), a ∈ s → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap (p := p) f s H₁ = pmap (p := q) g s H₂

Tactic:
@(Quot.inductionOn s (fun l _H₁ _H₂ h => congr_arg _ <| List.pmap_congr_left l h))

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
H : ∀ (a : α), a ∈ s → p a
b : β
⊢ b ∈ pmap (p := p) f s H ↔ ∃ (a : α), ∃ (h : a ∈ s), f a ⋯ = b

Tactic:
Quot.inductionOn s (fun _l _H => List.mem_pmap) H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
H : ∀ (a : α), a ∈ s → p a
⊢ (pmap (p := p) f s H).card = s.card

Tactic:
Quot.inductionOn s (fun _l _H => length_pmap) H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).attach = (↑l.attach : Multiset { x : α // x ∈ l })

Tactic:
rfl

Premises used: List.attachWith, Multiset.Mem, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s : Multiset α
⊢ ∀ (x : { x : α // x ∈ s }), x ∈ s.attach

Tactic:
Quot.inductionOn s fun _l => List.mem_attach _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
m : Multiset α
⊢ m.attach.card = m.card

Tactic:
card_pmap _ _ _

Premises used: Multiset.card_pmap, Multiset.attach
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
p : α → Prop
inst : (a : α) → Decidable (p a)
l : List α
⊢ (∀ (a : α), a ∈ l → p a) ↔ ∀ (a : α), a ∈ ⟦l⟧ → p a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β_1 : Type v
γ : Type u_2
m : Multiset α
β : α → Type u_3
inst : (a : α) → DecidableEq (β a)
f g : (a : α) → a ∈ m → β a
⊢ (∀ (a : α) (h : a ∈ m), f a h = g a h) ↔ f = g

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
p : α → Prop
inst : DecidablePred p
l : List α
⊢ (∃ (a : α), a ∈ l ∧ p a) ↔ ∃ (x : α), x ∈ ⟦l⟧ ∧ p x

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (a : List α), (↑l : Multiset α) = (↑a : Multiset α) ∧ List.Pairwise r a ↔ l ~ a ∧ List.Pairwise r a

Tactic:
simp