awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u

Tactic:
sup_le_iff

Premises used: sup_le_iff
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∪ t = t ∪ s

Tactic:
sup_comm ..

Premises used: sup_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t = t ∩ s

Tactic:
inf_comm ..

Premises used: inf_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ≤ t
rw : t ∪ s = t
rw₁ rw₂ : t = t
⊢ s ∪ t = t

Tactic:
rw [union_comm, eq_union_left h]

Premises used: Multiset.union_comm, Multiset.eq_union_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ≤ t
u : Multiset α
⊢ u ∪ s ≤ u ∪ t

Tactic:
sup_le_sup_left h _

Premises used: sup_le_sup_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∪ t ≤ s + t

Tactic:
union_le (le_add_right ..) (le_add_left ..)

Premises used: Multiset.le_add_left, Multiset.union_le, Multiset.le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : s + u - (u + t) = s - t
rw₁ : s + u - u - t = s - t
rw₂ rw₃ : s - t = s - t
⊢ s + u - (t + u) = s - t

Tactic:
rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]

Premises used: Multiset.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s ∪ t + u = s + u ∪ (t + u)

Tactic:
simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using
    show s + u - (t + u) = s - t by
      rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]

Premises used: Multiset.add_assoc, eq_comm, Union.union, Multiset.add_left_inj, Multiset.union
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∪ u + s = s + t ∪ (s + u)
rw₁ : t + s ∪ (u + s) = s + t ∪ (s + u)
rw₂ : t + s ∪ (u + s) = t + s ∪ (s + u)
rw₃ rw₄ : t + s ∪ (u + s) = t + s ∪ (u + s)
⊢ s + (t ∪ u) = s + t ∪ (s + u)

Tactic:
rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]

Premises used: Multiset.add_comm, Multiset.union_add_distrib
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

Tactic:
simpa using add_union_distrib (a ::ₘ 0) s t

Premises used: Multiset.cons, Multiset.add_union_distrib, OfNat.ofNat
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
by_contra! : ∀ (h : s ∩ t + u ≠ (s + u) ∩ (t + u)), False
⊢ s ∩ t + u = (s + u) ∩ (t + u)

Tactic:
by_contra! h
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
obtain : ∀ (a : α) (ha : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter
    (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)

Premises used: Multiset.lt_iff_cons_le, Multiset.le_inter, Multiset.inter_le_right, Multiset.add_le_add_right, Multiset.inter_le_left, Iff.mp, Ne.lt_of_le
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)
⊢ a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)

Tactic:
rw [← cons_add] at ha

Premises used: Multiset.cons_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
⊢ False

Tactic:
(lt_cons_self (s ∩ t) a).not_ge <| le_inter
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

Premises used: Multiset.le_inter, Inter.inter, Multiset.lt_cons_self, Multiset.inter_le_right, Multiset.inter_le_left, LE.le.trans, LT.lt.not_ge, Multiset.le_of_add_le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
⊢ False

Tactic:
exact (lt_cons_self (s ∩ t) a).not_ge <| le_inter
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

Premises used: Multiset.le_inter, Inter.inter, Multiset.lt_cons_self, Multiset.inter_le_right, Multiset.inter_le_left, LE.le.trans, LT.lt.not_ge, Multiset.le_of_add_le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∩ u + s = (s + t) ∩ (s + u)
rw₁ : (t + s) ∩ (u + s) = (s + t) ∩ (s + u)
rw₂ : (t + s) ∩ (u + s) = (t + s) ∩ (s + u)
rw₃ rw₄ : (t + s) ∩ (u + s) = (t + s) ∩ (u + s)
⊢ s + t ∩ u = (s + t) ∩ (s + u)

Tactic:
rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]

Premises used: Multiset.add_comm, Multiset.inter_add_distrib
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : s ∪ t + s ∩ t ≤ s + t
a₁ : s + t ≤ s ∪ t + s ∩ t
⊢ s ∪ t + s ∩ t = s + t

Tactic:
apply _root_.le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : s + s ∩ t ∪ (t + s ∩ t) ≤ s + t
⊢ s ∪ t + s ∩ t ≤ s + t

Tactic:
rw [union_add_distrib]

Premises used: Multiset.union_add_distrib
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t

Tactic:
union_le (Multiset.add_le_add_left inter_le_right) ?_

Premises used: Multiset.union_le, Multiset.inter_le_right, Multiset.add_le_add_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : t + s ∩ t ≤ s + t
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t

Tactic:
refine union_le (Multiset.add_le_add_left inter_le_right) ?_

Premises used: Multiset.union_le, Multiset.inter_le_right, Multiset.add_le_add_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : s ∩ t + t ≤ s + t
⊢ t + s ∩ t ≤ s + t

Tactic:
rw [Multiset.add_comm]

Premises used: Multiset.add_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t

Tactic:
Multiset.add_le_add_right inter_le_left

Premises used: Multiset.add_le_add_right, Multiset.inter_le_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t

Tactic:
exact Multiset.add_le_add_right inter_le_left

Premises used: Multiset.add_le_add_right, Multiset.inter_le_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
⊢ s + t ≤ s ∪ t + s ∩ t

Tactic:
rw [Multiset.add_comm, add_inter_distrib]

Premises used: Multiset.add_inter_distrib, Multiset.add_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)

Tactic:
le_inter (Multiset.add_le_add_right le_union_right) ?_

Premises used: Multiset.le_union_right, Multiset.le_inter, Multiset.add_le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : t + s ≤ s ∪ t + t
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)

Tactic:
refine le_inter (Multiset.add_le_add_right le_union_right) ?_

Premises used: Multiset.le_union_right, Multiset.le_inter, Multiset.add_le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : s + t ≤ s ∪ t + t
⊢ t + s ≤ s ∪ t + t

Tactic:
rw [Multiset.add_comm]

Premises used: Multiset.add_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t

Tactic:
Multiset.add_le_add_right le_union_left

Premises used: Multiset.le_union_left, Multiset.add_le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t

Tactic:
exact Multiset.add_le_add_right le_union_left

Premises used: Multiset.le_union_left, Multiset.add_le_add_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : s - t + t ∩ s = s
⊢ s - t + s ∩ t = s

Tactic:
rw [inter_comm]

Premises used: Multiset.inter_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
revert : ∀ (s : Multiset α), s - t + t ∩ s = s
⊢ s - t + t ∩ s = s

Tactic:
revert s
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - 0 + 0 ∩ s = s

Tactic:
simp
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
refine :
  ∀ (a : α) (t : Multiset α) (IH : ∀ (s : Multiset α), s - t + t ∩ s = s) (s : Multiset α),
    s - a ::ₘ t + (a ::ₘ t) ∩ s = s
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s

Tactic:
refine Multiset.induction_on t (by simp) fun a t IH s => ?_
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
pos : ∀ (h : a ∈ s), s - a ::ₘ t + (a ::ₘ t) ∩ s = s
neg : ∀ (h : ¬a ∈ s), s - a ::ₘ t + (a ::ₘ t) ∩ s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
pos : s - a ::ₘ t + a ::ₘ t ∩ s.erase a = s
pos₁ : s.erase a - t + a ::ₘ t ∩ s.erase a = s
pos₂ : a ::ₘ (s.erase a - t + t ∩ s.erase a) = s
pos₃ : a ::ₘ s.erase a = s
pos₄ pos₅ : s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]

Premises used: Multiset.add_cons, Multiset.cons_inter_of_pos, Multiset.sub_cons, Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
neg : s - a ::ₘ t + t ∩ s = s
neg₁ : s.erase a - t + t ∩ s = s
neg₂ : s - t + t ∩ s = s
neg₃ neg₄ : s = s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]

Premises used: Multiset.sub_cons, Multiset.erase_of_notMem, Multiset.cons_inter_of_neg
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s - s ∩ t = s - t

Tactic:
(Multiset.eq_sub_of_add_eq <| sub_add_inter ..).symm

Premises used: Multiset.eq_sub_of_add_eq, Multiset.sub_add_inter, Eq.symm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
a₁ : count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
⊢ count a (s ∩ t) = min (count a s) (count a t)

Tactic:
apply @Nat.add_left_cancel (count a (s - t))

Premises used: Nat.add_left_cancel
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
a₁ : count a (s - t + s ∩ t) = count a (s - t) + min (count a s) (count a t)
a₂ : count a s = count a (s - t) + min (count a s) (count a t)
a₃ : count a s = count a s - count a t + min (count a s) (count a t)
a₄ a₅ : count a s = count a s
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)

Tactic:
rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]

Premises used: Multiset.count_sub, Multiset.count_add, Multiset.sub_add_inter, Nat.sub_add_min_cancel
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
a : ∀ (a : α), count a ((↑s : Multiset α) ∩ (↑t : Multiset α)) = count a (↑(s.bagInter t) : Multiset α)
⊢ (↑s : Multiset α) ∩ (↑t : Multiset α) = (↑(s.bagInter t) : Multiset α)

Tactic:
ext
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
a : α
⊢ count a ((↑s : Multiset α) ∩ (↑t : Multiset α)) = count a (↑(s.bagInter t) : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
β : Type v
γ : Type u_2
inst : DecidableEq α
s_1 t_1 u_1 : Multiset α
a_1 : α
s t u : Multiset α
a : α
⊢ count a (s ⊔ t ⊓ u) = count a ((s ⊔ t) ⊓ (s ⊔ u))

Tactic:
simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union,
      Multiset.count_union, Multiset.inf_eq_inter]

Premises used: Multiset.sup_eq_union, max_min_distrib_left, Multiset.count_union, Multiset.count_inter, Multiset.inf_eq_inter
-- Module: Mathlib.Data.Multiset.UnionInter
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

Tactic:
le_antisymm (le_inter (filter_le_filter _ inter_le_left) (filter_le_filter _ inter_le_right)) <|
    le_filter.2 ⟨inf_le_inf (filter_le _ _) (filter_le _ _), fun _a h =>
      of_mem_filter (mem_of_le inter_le_left h)⟩

Premises used: Iff.mpr, Multiset.filter_le_filter, inf_le_inf, Multiset.le_inter, Multiset.of_mem_filter, Multiset.filter_le, le_antisymm, Multiset.mem_of_le, Multiset.inter_le_right, And.intro, Multiset.inter_le_left, Multiset.le_filter
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
a : ∀ (y : α), count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
⊢ replicate n x ∩ s = replicate (min n (count x s)) x

Tactic:
ext y
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
a : min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)

Tactic:
rw [count_inter, count_replicate, count_replicate]

Premises used: Multiset.count_replicate, Multiset.count_inter
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
pos : ∀ (h : x = y), min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
neg : ∀ (h : ¬x = y), min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
by_cases h : x = y
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
simp only [h, if_true]

Premises used: if_true
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
simp only [h, if_false, Nat.zero_min]

Premises used: if_false, Nat.zero_min
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
x : α
rw : replicate n x ∩ s = replicate (min (count x s) n) x
rw₁ : replicate (min n (count x s)) x = replicate (min (count x s) n) x
rw₂ rw₃ : replicate (min (count x s) n) x = replicate (min (count x s) n) x
⊢ s ∩ replicate n x = replicate (min (count x s) n) x

Tactic:
rw [inter_comm, replicate_inter, min_comm]

Premises used: min_comm, Multiset.replicate_inter, Multiset.inter_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
a : ∀ (x : α), count x (N ∩ Q + (P - M)) = count x N
⊢ N ∩ Q + (P - M) = N

Tactic:
ext x
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
a : min (count x N) (count x Q) + (count x P - count x M) = count x N
⊢ count x (N ∩ Q + (P - M)) = count x N

Tactic:
rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]

Premises used: Multiset.count_sub, Multiset.count_inter, Multiset.count_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
rw : ∀ (h : ∀ (a : α), count a (M + N) = count a (P + Q)) (x : α), count x M + count x N = count x P + count x Q
⊢ count x M + count x N = count x P + count x Q

Tactic:
rw [Multiset.ext] at h

Premises used: Multiset.ext
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), count a (M + N) = count a (P + Q)
x : α
⊢ count x M + count x N = count x P + count x Q

Tactic:
simp_all only [Multiset.count_add]

Premises used: Multiset.count_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x M + count x N = count x P + count x Q

Tactic:
have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.count_add]
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
h0 : count x M + count x N = count x P + count x Q
⊢ min (count x N) (count x Q) + (count x P - count x M) = count x N

Tactic:
omega
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t

Tactic:
⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
refine_1 : ∀ (h : _root_.Disjoint s t) (a : α) (hs : a ∈ s) (ht : a ∈ t), False
refine_2 : ∀ (h : ∀ {a : α}, a ∈ s → ¬a ∈ t) (u : Multiset α) (hs : u ≤ s) (ht : u ≤ t), u ≤ ⊥
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t

Tactic:
refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False

Tactic:
simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)

Premises used: Iff.mpr, Multiset.singleton_le
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
refine_2 : ∀ (a : α), ¬a ∈ u
⊢ u ≤ ⊥

Tactic:
rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]

Premises used: le_bot_iff, Multiset.eq_zero_iff_forall_notMem, Multiset.bot_eq_zero
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ ∀ (a : α), ¬a ∈ u

Tactic:
fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

Premises used: Multiset.subset_of_le, Not
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ ∀ (a : α), ¬a ∈ u

Tactic:
exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

Premises used: Multiset.subset_of_le
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ _root_.Disjoint (↑l₁ : Multiset α) (↑l₂ : Multiset α) ↔ l₁.Disjoint l₂

Tactic:
disjoint_left

Premises used: List.Disjoint, Multiset.Mem, Multiset.disjoint_left, Not
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ t → ¬a ∈ s

Tactic:
disjoint_comm.trans disjoint_left

Premises used: disjoint_comm, Multiset.disjoint_left, Iff.trans
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b

Tactic:
simp [disjoint_left, imp_not_comm]

Premises used: Multiset.disjoint_left, imp_not_comm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t u : Multiset α
h : s ⊆ u
d : _root_.Disjoint u t
⊢ _root_.Disjoint s t

Tactic:
disjoint_left.mpr fun ha ↦ disjoint_left.mp d <| h ha

Premises used: Iff.mpr, Multiset.disjoint_left, Iff.mp
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t u : Multiset α
h : t ⊆ u
d : _root_.Disjoint s u
⊢ _root_.Disjoint s t

Tactic:
(disjoint_of_subset_left h d.symm).symm

Premises used: Disjoint.symm, Multiset.disjoint_of_subset_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
l : Multiset α
⊢ _root_.Disjoint 0 l

Tactic:
disjoint_bot_left

Premises used: disjoint_bot_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint {a} l ↔ ¬a ∈ l

Tactic:
simp [disjoint_left]

Premises used: Multiset.disjoint_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
l : Multiset α
a : α
rw : _root_.Disjoint {a} l ↔ ¬a ∈ l
rw₁ rw₂ : ¬a ∈ l ↔ ¬a ∈ l
⊢ _root_.Disjoint l {a} ↔ ¬a ∈ l

Tactic:
rw [_root_.disjoint_comm, singleton_disjoint]

Premises used: disjoint_comm, Multiset.singleton_disjoint
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint (s + t) u ↔ _root_.Disjoint s u ∧ _root_.Disjoint t u

Tactic:
simp [disjoint_left, or_imp, forall_and]

Premises used: or_imp, Multiset.disjoint_left, forall_and
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t u : Multiset α
rw : _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
⊢ _root_.Disjoint s (t + u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
rw [_root_.disjoint_comm, disjoint_add_left]

Premises used: Multiset.disjoint_add_left, disjoint_comm