awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (s.sort r).length = s.card

Tactic:
Quot.inductionOn s <| length_mergeSort

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Multiset β
⊢ Eq (α := Multiset (α ⊕ β)) (disjSum 0 t) (map inr t)

Tactic:
Multiset.zero_add _

Premises used: Multiset.map, List.map, Multiset.zero, Multiset.zero_add, Multiset.ofList, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
⊢ Eq (α := Multiset (α ⊕ β)) (s.disjSum 0) (map inl s)

Tactic:
Multiset.add_zero _

Premises used: Multiset.add_zero, Multiset.map, List.map, Multiset.zero, Multiset.ofList, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
rw : (map inl s + map inr t).card = s.card + t.card
rw₁ : card (α := α ⊕ β) (map inl s) + card (α := α ⊕ β) (map inr t) = s.card + t.card
rw₂ : s.card + card (α := α ⊕ β) (map inr t) = s.card + t.card
rw₃ rw₄ : s.card + t.card = s.card + t.card
⊢ (s.disjSum t).card = s.card + t.card

Tactic:
rw [disjSum, card_add, card_map, card_map]

Premises used: Multiset.card_add, Multiset.card_map, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
simp_rw : x ∈ map inl s + map inr t ↔ (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
simp_rw₁ :
  Membership.mem (γ := Multiset (α ⊕ β)) (map inl s) x ∨ Membership.mem (γ := Multiset (α ⊕ β)) (map inr t) x ↔
    (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
⊢ x ∈ s.disjSum t ↔ (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x

Tactic:
simp_rw [disjSum, mem_add, mem_map]

Premises used: Multiset.mem_map, Multiset.mem_add, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
rw : (∃ (a_1 : α), a_1 ∈ s ∧ Eq (α := α ⊕ β) (inl a_1) (inl a)) ↔ a ∈ s
rw₁ : ¬∃ (b : β), b ∈ t ∧ inr b = inl a
⊢ inl a ∈ s.disjSum t ↔ a ∈ s

Tactic:
rw [mem_disjSum, or_iff_left]

Premises used: Multiset.mem_disjSum, or_iff_left
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ (∃ (a_1 : α), a_1 ∈ s ∧ Eq (α := α ⊕ β) (inl a_1) (inl a)) ↔ a ∈ s

Tactic:
simp only [inl.injEq, exists_eq_right]

Premises used: exists_eq_right, Sum.inl.injEq
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
b : β
left : b ∈ t
hb : inr b = inl a
⊢ False

Tactic:
inr_ne_inl hb

Premises used: Sum.inr_ne_inl
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
b : β
left : b ∈ t
hb : inr b = inl a
⊢ False

Tactic:
exact inr_ne_inl hb

Premises used: Sum.inr_ne_inl
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
rw : (∃ (b_1 : β), b_1 ∈ t ∧ Eq (α := α ⊕ β) (inr b_1) (inr b)) ↔ b ∈ t
rw₁ : ¬∃ (a : α), a ∈ s ∧ inl a = inr b
⊢ inr b ∈ s.disjSum t ↔ b ∈ t

Tactic:
rw [mem_disjSum, or_iff_right]

Premises used: Multiset.mem_disjSum, or_iff_right
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ (∃ (b_1 : β), b_1 ∈ t ∧ Eq (α := α ⊕ β) (inr b_1) (inr b)) ↔ b ∈ t

Tactic:
simp only [inr.injEq, exists_eq_right]

Premises used: Sum.inr.injEq, exists_eq_right
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
a : α
left : a ∈ s
ha : inl a = inr b
⊢ False

Tactic:
inl_ne_inr ha

Premises used: Sum.inl_ne_inr
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
a : α
left : a ∈ s
ha : inl a = inr b
⊢ False

Tactic:
exact inl_ne_inr ha

Premises used: Sum.inl_ne_inr
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
hs : s₁ ≤ s₂
ht : t₁ ≤ t₂
⊢ s₁.disjSum t₁ ≤ s₂.disjSum t₂

Tactic:
add_le_add (map_le_map hs) (map_le_map ht)

Premises used: add_le_add, Multiset.map_le_map, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Multiset β
⊢ Monotone (β := Multiset (α ⊕ β)) fun (s : Multiset α) ↦ s.disjSum t

Tactic:
fun _ _ hs => Multiset.add_le_add_right (map_le_map hs)

Premises used: Monotone, Multiset.map_le_map, Multiset.add_le_add_right, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
⊢ Monotone (α := Multiset β) s.disjSum

Tactic:
fun _ _ ht =>
  Multiset.add_le_add_left (map_le_map ht)

Premises used: Monotone, Multiset.map_le_map, Multiset.add_le_add_left, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
hs : s₁ < s₂
ht : t₁ ≤ t₂
⊢ s₁.disjSum t₁ < s₂.disjSum t₂

Tactic:
add_lt_add_of_lt_of_le (map_lt_map hs) (map_le_map ht)

Premises used: Multiset.map_le_map, add_lt_add_of_lt_of_le, Multiset.map_lt_map, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
hs : s₁ ≤ s₂
ht : t₁ < t₂
⊢ s₁.disjSum t₁ < s₂.disjSum t₂

Tactic:
add_lt_add_of_le_of_lt (map_le_map hs) (map_lt_map ht)

Premises used: add_lt_add_of_le_of_lt, Multiset.map_le_map, Multiset.map_lt_map, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
t : Multiset β
⊢ StrictMono (β := Multiset (α ⊕ β)) fun (s : Multiset α) ↦ s.disjSum t

Tactic:
fun _ _ hs => disjSum_lt_disjSum_of_lt_of_le hs le_rfl

Premises used: le_rfl, StrictMono, Multiset.disjSum_lt_disjSum_of_lt_of_le
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
⊢ StrictMono (α := Multiset β) s.disjSum

Tactic:
fun _ _ =>
  disjSum_lt_disjSum_of_le_of_lt le_rfl

Premises used: le_rfl, StrictMono, Multiset.disjSum_lt_disjSum_of_le_of_lt
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ (s.disjSum t).Nodup

Tactic:
((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_

Premises used: Iff.mpr, Multiset.Nodup.map, Sum.inr_injective, Sum.inl_injective, Multiset.Nodup.add_iff, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
refine : Disjoint (Multiset.map inl s) (Multiset.map inr t)
⊢ (s.disjSum t).Nodup

Tactic:
refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_

Premises used: Iff.mpr, Multiset.Nodup.map, Sum.inr_injective, Sum.inl_injective, Multiset.Nodup.add_iff
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
rw : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → inl a ≠ inr b
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)

Tactic:
rw [disjoint_map_map]

Premises used: Multiset.disjoint_map_map
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → inl a ≠ inr b

Tactic:
fun _ _ _ _ ↦ inr_ne_inl.symm

Premises used: Ne.symm, Sum.inr_ne_inl
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → inl a ≠ inr b

Tactic:
exact fun _ _ _ _ ↦ inr_ne_inl.symm

Premises used: Ne.symm, Sum.inr_ne_inl
-- Module: Mathlib.Data.Multiset.Sum
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
simp_rw :
  map f (map inl s + map inr t) =
    HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
simp_rw₁ :
  map f (map inl s) + map f (map inr t) =
    HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
simp_rw₂ :
  map (f ∘ inl) s + map (f ∘ inr) t =
    HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
⊢ map f (s.disjSum t) = HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)

Tactic:
simp_rw [disjSum, map_add, map_map, Function.comp_def]

Premises used: Function.comp_def, Multiset.map_map, Multiset.map_add, Multiset.disjSum
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
β : Type u_2
m : Multiset α
x x_1 : List α
h : x ≈ x_1
rw : x.sym2.Perm x_1.sym2
⊢ Eq.{u_1 + 1} (α := Multiset (Sym2 α)) ((fun (xs : List α) ↦ (↑xs.sym2 : Multiset (Sym2 α))) x)
    ((fun (xs : List α) ↦ (↑xs.sym2 : Multiset (Sym2 α))) x_1)

Tactic:
rw [coe_eq_coe]

Premises used: Multiset.coe_eq_coe
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
β : Type u_2
m : Multiset α
x x_1 : List α
h : x ≈ x_1
⊢ x.sym2.Perm x_1.sym2

Tactic:
h.sym2

Premises used: List.Perm.sym2
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
β : Type u_2
m : Multiset α
x x_1 : List α
h : x ≈ x_1
⊢ x.sym2.Perm x_1.sym2

Tactic:
exact h.sym2

Premises used: List.Perm.sym2
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
xs : List α
⊢ (↑xs : Multiset α).sym2 = (↑xs.sym2 : Multiset (Sym2 α))

Tactic:
rfl

Premises used: Multiset.sym2, rfl
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
xs : List α
⊢ Multiset.sym2 ⟦xs⟧ = 0 ↔ ⟦xs⟧ = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset (Sym2 α)) (Multiset.sym2 0) 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, List.sym2, Multiset.sym2, rfl
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
a : α
m : Multiset α
⊢ (a ::ₘ m).sym2 = map (fun (b : α) ↦ s(a, b)) (a ::ₘ m) + m.sym2

Tactic:
m.inductionOn fun _ => rfl

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : Multiset α
xs : List α
⊢ (map f ⟦xs⟧).sym2 = map (Sym2.map f) (Multiset.sym2 ⟦xs⟧)

Tactic:
simp [List.sym2_map]

Premises used: List.sym2_map
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
a b : α
xs : List α
⊢ s(a, b) ∈ Multiset.sym2 ⟦xs⟧ ↔ a ∈ ⟦xs⟧ ∧ b ∈ ⟦xs⟧

Tactic:
simp [List.mk_mem_sym2_iff]

Premises used: List.mk_mem_sym2_iff
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
z : Sym2 α
xs : List α
⊢ z ∈ Multiset.sym2 ⟦xs⟧ ↔ ∀ y ∈ z, y ∈ ⟦xs⟧

Tactic:
simp [List.mem_sym2_iff]

Premises used: List.mem_sym2_iff
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
z : Sym2 α
a b : α
⊢ Membership.mem (γ := Set (Sym2 α)) {z : Sym2 α | z ∈ m.sym2} s(a, b) ↔
    Membership.mem (γ := Set (Sym2 α)) (Set.sym2 {x : α | x ∈ m}) s(a, b)

Tactic:
simp [mk_mem_sym2_iff]

Premises used: Multiset.mk_mem_sym2_iff
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
h : m.Nodup
⊢ m.sym2.Nodup

Tactic:
m.inductionOn (fun _ h => List.Nodup.sym2 h) h

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m m' : Multiset α
h : m ≤ m'
h₁ : ∀ (xs ys : List α) (h : ⟦xs⟧ ≤ ⟦ys⟧), Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧
⊢ m.sym2 ≤ m'.sym2

Tactic:
induction m, m' using Quotient.inductionOn₂ with | _ xs ys
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
h₁ : xs <+~ ys
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧

Tactic:
suffices xs <+~ ys from this.sym2
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ xs <+~ ys

Tactic:
simpa only [quot_mk_to_coe, coe_le, sym2_coe] using h

Premises used: Multiset.coe_le, Multiset.quot_mk_to_coe, Multiset.sym2_coe
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Multiset α) Multiset.sym2

Tactic:
fun _ _ => sym2_mono

Premises used: Monotone, Multiset.sym2_mono
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
⊢ m.sym2.card = (m.card + 1).choose 2

Tactic:
m.inductionOn fun xs => ?_

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
refine : ∀ (xs : List α), (Multiset.sym2 ⟦xs⟧).card = (card ⟦xs⟧ + 1).choose 2
⊢ m.sym2.card = (m.card + 1).choose 2

Tactic:
refine m.inductionOn fun xs => ?_
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).card = (card ⟦xs⟧ + 1).choose 2

Tactic:
simp [List.length_sym2]

Premises used: List.length_sym2
-- Module: Mathlib.Data.Multiset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).dedup = (dedup ⟦xs⟧).sym2

Tactic:
simp [List.dedup_sym2]

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

Tactic:
rfl

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

Tactic:
Multiset.le_sub_add

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

Tactic:
le_add_left _ _

Premises used: Multiset.le_add_left, Multiset.union
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t ≤ s → s ∪ t = s

Tactic:
Multiset.sub_add_cancel

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

Tactic:
Multiset.add_le_add_right <| Multiset.sub_le_sub_right h

Premises used: Multiset.sub_le_sub_right, Multiset.add_le_add_right, Multiset.union
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
rw : s ∪ t ≤ u ∪ t
⊢ s ∪ t ≤ u

Tactic:
rw [← eq_union_left h₂]

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

Tactic:
union_le_union_right h₁ t

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

Tactic:
exact union_le_union_right h₁ t

Premises used: Multiset.union_le_union_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

Tactic:
⟨fun h => (mem_add.1 h).imp_left (mem_of_le <| Multiset.sub_le_self _ _),
    (Or.elim · (mem_of_le le_union_left) (mem_of_le le_union_right))⟩

Premises used: Multiset.sub_le_self, Or.imp_left, Multiset.le_union_right, Multiset.mem_add, Multiset.le_union_left, Multiset.mem_of_le, Iff.intro, Iff.mp, Or.elim
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
rw : List.map f (l₁.diff l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
rw₁ rw₂ : (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂

Tactic:
rw [List.map_append, List.map_diff finj]

Premises used: List.map_diff, List.map_append
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ 0 ∪ s = s

Tactic:
simp [union_def, Multiset.zero_sub]

Premises used: Multiset.zero_sub, Multiset.union_def
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s ∪ 0 = s

Tactic:
simp [union_def]

Premises used: Multiset.union_def
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∪ t) = max (count a s) (count a t)

Tactic:
simp [(· ∪ ·), union, Nat.sub_add_eq_max]

Premises used: Nat.sub_add_eq_max, Union.union, Multiset.union
-- 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:
simp [(· ∪ ·), union]

Premises used: Union.union, Multiset.union
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s ∩ 0 = 0

Tactic:
Quot.inductionOn s fun l => congr_arg ofList l.bagInter_nil

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

Tactic:
Quot.inductionOn s fun l => congr_arg ofList l.nil_bagInter

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
⊢ a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_mem _ h

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
⊢ ¬a ∈ t → (a ::ₘ s) ∩ t = s ∩ t

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_not_mem _ h

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

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ => bagInter_sublist_left.subperm

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
⊢ 0 ∩ t ≤ t

Tactic:
(zero_inter t).symm ▸ zero_le _

Premises used: Eq.rec, Multiset.zero_inter, Multiset.zero_le, Eq.symm
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
⊢ 0 ∩ t ≤ t

Tactic:
exact (zero_inter t).symm ▸ zero_le _
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
pos : ∀ (h : a ∈ t), (a ::ₘ s) ∩ t ≤ t
neg : ∀ (h : ¬a ∈ t), (a ::ₘ s) ∩ t ≤ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
by_cases h : a ∈ t
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
simpa [h] using cons_le_cons a (IH (t := t.erase a))

Premises used: Multiset.cons_le_cons
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
simp [h, IH]
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
empty : ∀ {t : Multiset α}, 0 ∩ t ≤ t
cons : ∀ (a : α) (s : Multiset α) (IH : ∀ {t : Multiset α}, s ∩ t ≤ t) {t : Multiset α}, (a ::ₘ s) ∩ t ≤ t
⊢ s ∩ t ≤ t

Tactic:
induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h₁ : s ≤ t
h₂ : s ≤ u
revert : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
⊢ s ≤ t ∩ u

Tactic:
revert s u
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u

Tactic:
@(Multiset.induction_on t ?_ fun a t IH => ?_)

Premises used: Multiset.induction_on
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
refine_1 : ∀ {s u : Multiset α} (h₁ : s ≤ 0) (h₂ : s ≤ u), s ≤ 0 ∩ u
refine_2 :
  ∀ (a : α) (t : Multiset α) (IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u) {s u : Multiset α}
    (h₁ : s ≤ a ::ₘ t) (h₂ : s ≤ u), s ≤ (a ::ₘ t) ∩ u
⊢ ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u

Tactic:
refine @(Multiset.induction_on t ?_ fun a t IH => ?_)
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u

Tactic:
simpa only [zero_inter] using h₁

Premises used: Multiset.zero_inter
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
pos : ∀ (h : a ∈ u), s ≤ (a ::ₘ t) ∩ u
neg : ∀ (h : ¬a ∈ u), s ≤ (a ::ₘ t) ∩ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
by_cases h : a ∈ u
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
pos : s.erase a ≤ t ∩ u.erase a
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]

Premises used: Multiset.cons_inter_of_pos, Multiset.erase_le_iff_le_cons
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s.erase a ≤ t ∩ u.erase a

Tactic:
IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)

Premises used: Iff.mpr, Multiset.erase_le_erase, Multiset.erase_le_iff_le_cons
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s.erase a ≤ t ∩ u.erase a

Tactic:
exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)

Premises used: Iff.mpr, Multiset.erase_le_erase, Multiset.erase_le_iff_le_cons
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
neg : s ≤ t ∩ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
rw [cons_inter_of_neg _ h]

Premises used: Multiset.cons_inter_of_neg
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u

Tactic:
IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

Premises used: mt, Multiset.mem_of_le, Iff.mp, Multiset.le_cons_of_notMem
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u

Tactic:
exact IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

Premises used: mt, Multiset.mem_of_le, Iff.mp, Multiset.le_cons_of_notMem
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
rw : a ∈ a ::ₘ s.erase a ∩ t.erase a
⊢ a ∈ s ∩ t

Tactic:
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]

Premises used: Multiset.cons_inter_of_pos, Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a

Tactic:
apply mem_cons_self

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u

Tactic:
le_inf_iff

Premises used: le_inf_iff