awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ Eq (α := Multiset ((a : α) × σ a))
    ((↑l₁ : Multiset α).bind fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (↑(l₂ a) : Multiset (σ a)))
    ((↑l₁ : Multiset α).bind fun (a : α) ↦
      (↑(List.map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) : Multiset ((a : α) × σ a)))

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
t : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (σ := σ) 0 t = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.sigma, Multiset.join, List.foldr, Multiset.bind, rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (a ::ₘ s).sigma (σ := σ) t = map (Sigma.mk (β := σ) a) (t a) + s.sigma (σ := σ) t

Tactic:
simp [Multiset.sigma]

Premises used: Multiset.sigma
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
β : Type v
a : α
b : α → β
⊢ Eq (α := Multiset ((_ : α) × β)) (Multiset.sigma (σ := fun (a : α) ↦ β) {a} fun (a : α) ↦ {b a})
    {Sigma.mk (β := fun (a : α) ↦ β) a (b a)}

Tactic:
rfl

Premises used: Multiset.sum, Multiset.add, Multiset.foldr, Multiset.sigma, Multiset.cons, List.append, Multiset.ofList, Multiset.join, List.foldr, Multiset.bind, rfl
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ (s + t).sigma (σ := σ) u = s.sigma (σ := σ) u + t.sigma (σ := σ) u

Tactic:
simp [Multiset.sigma]

Premises used: Multiset.sigma
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
s_1 : Multiset α
a : α
s : Multiset α
IH :
  ∀ (t u : (a : α) → Multiset (σ a)),
    (s.sigma (σ := σ) fun (a : α) ↦ t a + u a) = s.sigma (σ := σ) t + s.sigma (σ := σ) u
t u : (a : α) → Multiset (σ a)
rw :
  map (Sigma.mk (β := σ) a) (t a + u a) + (s.sigma (σ := σ) t + s.sigma (σ := σ) u) =
    (a ::ₘ s).sigma (σ := σ) t + (a ::ₘ s).sigma (σ := σ) u
⊢ ((a ::ₘ s).sigma (σ := σ) fun (a : α) ↦ t a + u a) = (a ::ₘ s).sigma (σ := σ) t + (a ::ₘ s).sigma (σ := σ) u

Tactic:
rw [cons_sigma, IH]

Premises used: Multiset.cons_sigma
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
s_1 : Multiset α
a : α
s : Multiset α
IH :
  ∀ (t u : (a : α) → Multiset (σ a)),
    (s.sigma (σ := σ) fun (a : α) ↦ t a + u a) = s.sigma (σ := σ) t + s.sigma (σ := σ) u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk (β := σ) a) (t a + u a) + (s.sigma (σ := σ) t + s.sigma (σ := σ) u) =
    (a ::ₘ s).sigma (σ := σ) t + (a ::ₘ s).sigma (σ := σ) u

Tactic:
simp [add_comm, add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, add_comm
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (s.sigma (σ := σ) t).card = sum (map (fun (a : α) ↦ (t a).card) s)

Tactic:
simp [Multiset.sigma, (· ∘ ·)]

Premises used: Multiset.sigma, Function.comp
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ Sigma.mk (β := fun (a : α) ↦ σ a) a b ∈ s.sigma (σ := σ) t ↔
    (Sigma.mk (β := fun (a : α) ↦ σ a) a b).fst (β := fun (a : α) ↦ σ a) ∈ s ∧
      Membership.mem (γ := Multiset (σ ((Sigma.mk (β := fun (a : α) ↦ σ a) a b).fst (β := fun (a : α) ↦ σ a))))
        (t ((Sigma.mk (β := fun (a : α) ↦ σ a) a b).fst (β := fun (a : α) ↦ σ a)))
        ((Sigma.mk (β := fun (a : α) ↦ σ a) a b).snd (β := fun (a : α) ↦ σ a))

Tactic:
simp [Multiset.sigma, and_left_comm]

Premises used: Multiset.sigma, and_left_comm
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
choose :
  ∀ (f : (a : α) → List (σ a)) (hf : ∀ (a : α), ⟦f a⟧ = t a),
    Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) →
      (∀ (a : α), (t a).Nodup) →
        (Multiset.sigma (σ := σ) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) t).Nodup
⊢ Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) →
    (∀ (a : α), (t a).Nodup) →
      (Multiset.sigma (σ := σ) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) t).Nodup

Tactic:
choose f hf using fun a => Quotient.exists_rep (t a)

Premises used: Quotient.exists_rep
-- Module: Mathlib.Data.Multiset.Bind
Goal:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), ⟦f a⟧ = t a
⊢ Nodup (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) →
    (∀ (a : α), (t a).Nodup) →
      (Multiset.sigma (σ := σ) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l₁) t).Nodup

Tactic:
simpa [← funext hf] using List.Nodup.sigma

Premises used: List.Nodup.sigma, funext
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : List α
⊢ countP p (↑l : Multiset α) = List.countP (fun (b : α) ↦ decide (p b)) l

Tactic:
rfl

Premises used: Multiset.countP, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ countP p 0 = 0

Tactic:
rfl

Premises used: List.countP.go, Multiset.countP, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α),
    p a →
      countP p (a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a_1) =
        countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a_1) + 1

Tactic:
simpa using fun _ => List.countP_cons_of_pos (p := (p ·))

Premises used: List.countP_cons_of_pos
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α),
    ¬p a →
      countP p (a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a_1) =
        countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a_1)

Tactic:
simpa using fun _ => List.countP_cons_of_neg (p := (p ·))

Premises used: List.countP_cons_of_neg
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
b : α
s : Multiset α
⊢ ∀ (a : List α),
    countP p (b ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) =
      countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) a) + if p b then 1 else 0

Tactic:
simp [List.countP_cons]

Premises used: List.countP_cons
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ countP p s ≤ s.card

Tactic:
Quot.inductionOn s fun _l => countP_le_length (p := (p ·))

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
l : List α
⊢ card (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) =
    countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) +
      countP (fun (x : α) ↦ ¬p x) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)

Tactic:
simp [l.length_eq_countP_add_countP p]

Premises used: List.length_eq_countP_add_countP
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Multiset α
h : s ≤ t
⊢ countP p s ≤ countP p t

Tactic:
leInductionOn h fun s => s.countP_le

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s : Multiset α
⊢ countP (fun (x : α) ↦ True) s = s.card

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

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s : Multiset α
⊢ countP (fun (x : α) ↦ False) s = 0

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

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
l : List α
simp :
  countP (fun (a : { a : α // a ∈ (↑l : Multiset α) }) ↦ p (↑a : α)) (↑l.attach : Multiset { x : α // x ∈ l }) =
    List.countP (fun (a : { x : α // x ∈ l }) ↦ decide (p (↑a : α))) l.attach
⊢ countP (fun (a : { a : α // a ∈ ⟦l⟧ }) ↦ p (↑a : α)) (attach ⟦l⟧) = countP p ⟦l⟧

Tactic:
simp only [quot_mk_to_coe, coe_countP, coe_attach, coe_countP, ← List.countP_attach (l := l)]

Premises used: List.countP_attach, Multiset.coe_countP, Multiset.quot_mk_to_coe, Multiset.coe_attach
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun (a : { a : α // a ∈ (↑l : Multiset α) }) ↦ p (↑a : α)) (↑l.attach : Multiset { x : α // x ∈ l }) =
    List.countP (fun (a : { x : α // x ∈ l }) ↦ decide (p (↑a : α))) l.attach

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
_l : List α
⊢ 0 < countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    ∃ (a : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a ∧ p a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) = 0 ↔
    ∀ (a : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a → ¬p a

Tactic:
simp [List.countP_eq_zero]

Premises used: List.countP_eq_zero
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) =
      card (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    ∀ (a : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a → p a

Tactic:
simp [List.countP_eq_length]

Premises used: List.countP_eq_length
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
a : α
h : a ∈ s
pa : p a
⊢ 0 < countP p s

Tactic:
countP_pos.2 ⟨_, h, pa⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Multiset.countP_pos
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
hp : ∀ (x : α), x ∈ s → p x = p' x
revert : ∀ (hs : s = s') (hp : ∀ (x : α), x ∈ s → p x = p' x), countP p s = countP p' s'
⊢ countP p s = countP p' s'

Tactic:
revert hs hp
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
l l' : List α
hs :
  Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
    (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l')
hp : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x → p x = p' x
⊢ l ~ l'

Tactic:
simp only [quot_mk_to_coe'', coe_eq_coe] at hs

Premises used: Multiset.coe_eq_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
l l' : List α
hp : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x → p x = p' x
hs : l ~ l'
apply : ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)
⊢ countP p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) =
    countP p' (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l')

Tactic:
apply hs.countP_congr

Premises used: List.Perm.countP_congr
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
l l' : List α
hp : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)

Tactic:
simpa using hp
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred p'
⊢ ∀ (hs : s = s') (hp : ∀ (x : α), x ∈ s → p x = p' x), countP p s = countP p' s'

Tactic:
exact Quot.induction_on₂ s s'
    (fun l l' hs hp => by
      simp only [quot_mk_to_coe'', coe_eq_coe] at hs
      apply hs.countP_congr
      simpa using hp)
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
simp_rw : List.countP (fun (b : α) ↦ decide (b = a)) l = List.countP (fun (x : α) ↦ x == a) l
⊢ count a (↑l : Multiset α) = List.count a l

Tactic:
simp_rw [count, List.count, coe_countP (a = ·) l, @eq_comm _ a]

Premises used: Multiset.coe_countP, Multiset.count, eq_comm, List.count, Eq
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ List.countP (fun (b : α) ↦ decide (b = a)) l = List.countP (fun (x : α) ↦ x == a) l

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ count a 0 = 0

Tactic:
rfl

Premises used: Multiset.count, List.countP.go, Multiset.countP, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ count a (a ::ₘ s) = count a s + 1

Tactic:
countP_cons_of_pos _ <| rfl

Premises used: Multiset.count, Multiset.countP_cons_of_pos, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
h : a ≠ b
s : Multiset α
⊢ count a (b ::ₘ s) = count a s

Tactic:
countP_cons_of_neg _ <| h

Premises used: Multiset.count, Multiset.countP_cons_of_neg
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ count a s ≤ s.card

Tactic:
countP_le_card _ _

Premises used: Multiset.countP_le_card, Multiset.count
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ s ≤ t → count a s ≤ count a t

Tactic:
countP_le_of_le _

Premises used: Multiset.count, Multiset.countP_le_of_le
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
⊢ count a s ≤ count a (b ::ₘ s)

Tactic:
count_le_of_le _ (le_cons_self _ _)

Premises used: Multiset.count_le_of_le, Multiset.le_cons_self
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
⊢ count a (b ::ₘ s) = count a s + if a = b then 1 else 0

Tactic:
countP_cons (a = ·) _ _

Premises used: Multiset.countP_cons, Multiset.count, Eq
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ count a {a} = 1

Tactic:
count_eq_one_of_mem (nodup_singleton a) <| mem_singleton_self a

Premises used: List.nodup_singleton, Multiset.count, List.countP.go, List.count_eq_one_of_mem, Multiset.mem_singleton_self, Multiset.countP, Decidable.decide, Not
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
⊢ count a {b} = if a = b then 1 else 0

Tactic:
simp only [count_cons, ← cons_zero, count_zero, Nat.zero_add]

Premises used: Multiset.count_cons, Multiset.count_zero, Nat.zero_add, Multiset.cons_zero
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a x : { x : α // x ∈ s }
h : x ∈ s.attach
⊢ (a = x) = ((↑a : α) = (↑x : α))

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ 0 < count a s ↔ a ∈ s

Tactic:
simp [count, countP_pos]

Premises used: Multiset.count, Multiset.countP_pos
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
rw : 0 < count a s ↔ a ∈ s
rw₁ rw₂ : a ∈ s ↔ a ∈ s
⊢ 1 ≤ count a s ↔ a ∈ s

Tactic:
rw [succ_le_iff, count_pos]

Premises used: Multiset.count_pos, Nat.succ_le_iff
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ count a s = 0

Tactic:
by_contradiction fun h' => h <| count_pos.1 (Nat.pos_of_ne_zero h')

Premises used: Multiset.count_pos, Nat.pos_of_ne_zero, by_contradiction, Iff.mp
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ count a s ≠ 0 ↔ a ∈ s

Tactic:
Nat.pos_iff_ne_zero.symm.trans count_pos

Premises used: Nat.pos_iff_ne_zero, Multiset.count_pos, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ count a s = 0 ↔ ¬a ∈ s

Tactic:
count_ne_zero.not_right

Premises used: Multiset.count_ne_zero, Iff.not_right
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ count a s = s.card ↔ ∀ (x : α), x ∈ s → a = x

Tactic:
simp [countP_eq_card, count, @eq_comm _ a]

Premises used: Multiset.count, eq_comm, Multiset.countP_eq_card
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
simp : (isSetoid α : List α → List α → Prop) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
⊢ (isSetoid α : List α → List α → Prop) _l₁ _l₂ ↔ ∀ (a : α), count a ⟦_l₁⟧ = count a ⟦_l₂⟧

Tactic:
simp only [quot_mk_to_coe, coe_count]

Premises used: Multiset.coe_count, Multiset.quot_mk_to_coe
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α : List α → List α → Prop) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂

Tactic:
apply perm_iff_count

Premises used: List.perm_iff_count
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s = count a t) → s = t

Tactic:
ext.2

Premises used: Iff.mpr, Multiset.ext
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Injective (β := (a : α) → ℕ) fun (s : Multiset α) (a : α) ↦ count a s

Tactic:
fun _s _t hst ↦ ext' <| congr_fun hst

Premises used: Function.Injective, congr_fun, Multiset.ext'
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
x x_1 : List α
⊢ ⟦x⟧ ≤ ⟦x_1⟧ ↔ ∀ (a : α), count a ⟦x⟧ ≤ count a ⟦x_1⟧

Tactic:
simp [subperm_iff_count]

Premises used: List.subperm_iff_count
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
empty empty₁ : countP (r x) 0 = countP (r x) 0
⊢ countP (r x) 0 = countP (r x) t

Tactic:
rw [rel_zero_left.mp h]

Premises used: Iff.mp, Multiset.rel_zero_left
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
t : Multiset α
h : Rel r (y ::ₘ s) t
cons :
  ∀ (b : α) (bs : Multiset α) (hb1 : r y b) (hb2 : Rel r s bs) (h : Rel r (y ::ₘ s) (b ::ₘ bs)),
    countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) t

Tactic:
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h

Premises used: Multiset.rel_cons_left, Iff.mp, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
cons : (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)

Tactic:
rw [countP_cons, countP_cons, ih hb2]

Premises used: Multiset.countP_cons
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
cons : Eq (α := ℕ) (if r x y then 1 else 0) (if r x b then 1 else 0)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0

Tactic:
simp only [Nat.add_right_inj]

Premises used: Nat.add_right_inj
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ Eq (α := ℕ) (if r x y then 1 else 0) (if r x b then 1 else 0)

Tactic:
(if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)

Premises used: trans, if_congr, Iff.intro, symm, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
x : α
inst_2 : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ Eq (α := ℕ) (if r x y then 1 else 0) (if r x b then 1 else 0)

Tactic:
exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)

Premises used: trans, if_congr, Iff.intro, symm, rfl
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Symm r
s t : Multiset α
x : α
inst_2 : DecidablePred (r x)
h : Rel r s t
empty : ∀ {t : Multiset α} (h : Rel r 0 t), countP (r x) 0 = countP (r x) t
cons :
  ∀ (y : α) (s : Multiset α) (ih : ∀ {t : Multiset α} (h : Rel r s t), countP (r x) s = countP (r x) t) {t : Multiset α}
    (h : Rel r (y ::ₘ s) t), countP (r x) (y ::ₘ s) = countP (r x) t
⊢ countP (r x) s = countP (r x) t

Tactic:
induction s using Multiset.induction_on generalizing t with
  | empty => rw [rel_zero_left.mp h]
  | cons y s ih =>
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
    rw [countP_cons, countP_cons, ih hb2]
    simp only [Nat.add_right_inj]
    exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)

Premises used: Multiset.countP_cons, Multiset.rel_cons_left, Multiset.Rel.cons, Iff.mp, Multiset.rel_zero_left, rfl, Nat.add_right_inj
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
_l : List α
simp : _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1
⊢ Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    ∀ (a : α), count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ≤ 1

Tactic:
simp only [quot_mk_to_coe'', coe_nodup, coe_count]

Premises used: Multiset.coe_count, Multiset.coe_nodup, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
_l : List α
⊢ _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1

Tactic:
List.nodup_iff_count_le_one

Premises used: List.nodup_iff_count_le_one
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
_l : List α
⊢ _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1

Tactic:
exact List.nodup_iff_count_le_one

Premises used: List.nodup_iff_count_le_one
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
s : Multiset α
inst : DecidableEq α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    ∀ (a : α),
      Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a →
        count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) = 1

Tactic:
simpa using List.nodup_iff_count_eq_one

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

Tactic:
nodup_iff_count_eq_one.mp d a h

Premises used: Multiset.nodup_iff_count_eq_one, Iff.mp
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
pos : ∀ (h : a ∈ s), count a s = 1
neg : ∀ (h : ¬a ∈ s), count a s = 0
⊢ count a s = if a ∈ s then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Multiset.Count
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∈ s
⊢ count a s = 1

Tactic:
count_eq_one_of_mem d h

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

Tactic:
exact count_eq_one_of_mem d h

Premises used: Multiset.count_eq_one_of_mem