awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t u : Multiset α
mp : _root_.Disjoint t s ∧ _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mpr : _root_.Disjoint s t ∧ _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mp₁ mp₂ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t ∧ _root_.Disjoint s u
mp₃ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s t
mp₄ : _root_.Disjoint t s → _root_.Disjoint u s → _root_.Disjoint s u
mpr₁ mpr₂ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s ∧ _root_.Disjoint u s
mpr₃ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint t s
mpr₄ : _root_.Disjoint s t → _root_.Disjoint s u → _root_.Disjoint u s
mp₅ mp₆ mp₇ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mp₈ mp₉ mp₁₀ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ u → x ≤ ⊥
mpr₅ mpr₆ mpr₇ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mpr₈ mpr₉ mpr₁₀ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ u → x ≤ s → x ≤ ⊥
mp₁₁ mp₁₂ mp₁₃ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mp₁₄ mp₁₅ mp₁₆ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ u → x ≤ ⊥
mpr₁₁ mpr₁₂ mpr₁₃ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mpr₁₄ mpr₁₅ mpr₁₆ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ u → x ≤ s → x ≤ ⊥
mp₁₇ mp₁₈ mp₁₉ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mp₂₀ mp₂₁ mp₂₂ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ u → x ≤ ⊥
mpr₁₇ mpr₁₈ mpr₁₉ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mpr₂₀ mpr₂₁ mpr₂₂ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ u → x ≤ s → x ≤ ⊥
mp₂₃ mp₂₄ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ t → x ≤ ⊥
mp₂₅ mp₂₆ : _root_.Disjoint t s → _root_.Disjoint u s → ∀ ⦃x : Multiset α⦄, x ≤ s → x ≤ u → x ≤ ⊥
mpr₂₃ mpr₂₄ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ t → x ≤ s → x ≤ ⊥
mpr₂₅ mpr₂₆ : _root_.Disjoint s t → _root_.Disjoint s u → ∀ ⦃x : Multiset α⦄, x ≤ u → x ≤ s → x ≤ ⊥
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
tauto
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
a : α
s t : Multiset α
rw rw₁ : ¬a ∈ t ∧ _root_.Disjoint s t ↔ ¬a ∈ t ∧ _root_.Disjoint s t
⊢ _root_.Disjoint {a} t ∧ _root_.Disjoint s t ↔ ¬a ∈ t ∧ _root_.Disjoint s t

Tactic:
rw [singleton_disjoint]

Premises used: Multiset.singleton_disjoint
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
⊢ _root_.Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_cons_left]

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

Tactic:
tauto
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : s ∩ t ⊆ 0 ↔ _root_.Disjoint s t
⊢ s ∩ t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]

Premises used: Multiset.subset_zero
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
simp [subset_iff, disjoint_left]

Premises used: Multiset.disjoint_left, Multiset.subset_iff
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ _root_.Disjoint (s ∪ t) u ↔ _root_.Disjoint s u ∧ _root_.Disjoint t u

Tactic:
disjoint_sup_left

Premises used: disjoint_sup_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ _root_.Disjoint s (t ∪ u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
disjoint_sup_right

Premises used: disjoint_sup_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
simp_rw : s + t = s ∪ t ↔ s ∩ t = 0
simp_rw₁ : (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₂ : (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₃ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
simp_rw₄ :
  (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = count a 0
simp_rw₅ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = 0
simp_rw₆ : (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a s = 0 ∨ count a t = 0
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t

Tactic:
simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]

Premises used: Nat.min_eq_zero_iff, Multiset.ext, Nat.add_eq_max_iff, Multiset.count_union, Multiset.count_zero, Multiset.count_inter, Multiset.count_add, Multiset.inter_eq_zero_iff_disjoint
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
rw : u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t
⊢ u + s = u ∪ t ↔ _root_.Disjoint u s ∧ s = t

Tactic:
rw [← add_eq_union_iff_disjoint]

Premises used: Multiset.add_eq_union_iff_disjoint
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t

Tactic:
⟨fun h0 ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
refine_1 : ∀ (h0 : u + s = u ∪ t), u + s = u ∪ s ∧ s = t
refine_2 : u + s = u ∪ s ∧ s = t → u + s = u ∪ t
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t

Tactic:
refine ⟨fun h0 ↦ ?_, ?_⟩
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
refine_1 : s = t
refine_1₁ : s = t → u + s = u ∪ s
⊢ u + s = u ∪ s ∧ s = t

Tactic:
rw [and_iff_right_of_imp]

Premises used: and_iff_right_of_imp
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

Tactic:
(Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h

Premises used: LE.le.antisymm, Multiset.le_of_add_le_add_left, Eq.trans_le, Multiset.union_le_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

Tactic:
exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h

Premises used: LE.le.antisymm, Multiset.le_of_add_le_add_left, Eq.trans_le, Multiset.union_le_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s u : Multiset α
h : s ≤ s
h0 : u + s = u ∪ s
⊢ u + s = u ∪ s

Tactic:
h0
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s u : Multiset α
h : s ≤ s
h0 : u + s = u ∪ s
⊢ u + s = u ∪ s

Tactic:
exact h0
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s u : Multiset α
h0 : u + s = u ∪ s
h : s ≤ s
⊢ u + s = u ∪ s

Tactic:
h0
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s u : Multiset α
h0 : u + s = u ∪ s
h : s ≤ s
⊢ u + s = u ∪ s

Tactic:
exact h0
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
x y z : Multiset α
h : z ≤ y
⊢ x + y = x ∪ z ↔ y = z ∧ _root_.Disjoint x y

Tactic:
simpa only [and_comm] using add_eq_union_left_of_le h

Premises used: and_comm, Multiset.add_eq_union_left_of_le
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
⊢ _root_.Disjoint (map f s) (map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b

Tactic:
simp [disjoint_iff_ne]

Premises used: Multiset.disjoint_iff_ne
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a : α | a ∈ m} fun (a₁ a₂ : α) ↦ r (f a₁) (f a₂)
b₁ : β
h₁ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} b₁
b₂ : β
h₂ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} b₂
hn : b₁ ≠ b₂
obtain :
  ∀ (a₁ : α) (H₁ : a₁ ∈ m) (h₁ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₁)) (a₂ : α) (H₂ : a₂ ∈ m)
    (h₂ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₂)) (hn : f a₁ ≠ f a₂), r (f a₁) (f a₂)
⊢ r b₁ b₂

Tactic:
obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a : α | a ∈ m} fun (a₁ a₂ : α) ↦ r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₁)
a₂ : α
H₂ : a₂ ∈ m
h₂ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₂)
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)

Tactic:
h H₁ H₂ (mt (congr_arg f) hn)

Premises used: mt, congr_arg
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a : α | a ∈ m} fun (a₁ a₂ : α) ↦ r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₁)
a₂ : α
H₂ : a₂ ∈ m
h₂ : Membership.mem (γ := Set β) {b : β | b ∈ map f m} (f a₂)
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)

Tactic:
exact h H₁ H₂ (mt (congr_arg f) hn)

Premises used: mt, congr_arg
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
x x_1 : List α
⊢ (⟦x⟧ + ⟦x_1⟧).Nodup ↔ Nodup ⟦x⟧ ∧ Nodup ⟦x_1⟧ ∧ _root_.Disjoint ⟦x⟧ ⟦x_1⟧

Tactic:
simp [nodup_append, disjoint_iff_ne]

Premises used: List.nodup_append, Multiset.disjoint_iff_ne
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
d : (s + t).Nodup
⊢ _root_.Disjoint s t

Tactic:
(nodup_add.1 d).2.2

Premises used: And.right, Iff.mp, Multiset.nodup_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s t : Multiset α
d₁ : s.Nodup
d₂ : t.Nodup
⊢ (s + t).Nodup ↔ _root_.Disjoint s t

Tactic:
simp [nodup_add, d₁, d₂]

Premises used: Multiset.nodup_add
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
s : Multiset α
inst : DecidableEq α
t : Multiset α
⊢ s.Nodup → (s ∩ t).Nodup

Tactic:
nodup_of_le inter_le_left

Premises used: Multiset.nodup_of_le, Multiset.inter_le_left
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
t : Multiset α
inst : DecidableEq α
s : Multiset α
⊢ t.Nodup → (s ∩ t).Nodup

Tactic:
nodup_of_le inter_le_right

Premises used: Multiset.nodup_of_le, Multiset.inter_le_right
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
rw : max (count a s) (count a t) ≤ 1
⊢ count a (s ∪ t) ≤ 1

Tactic:
rw [count_union]

Premises used: Multiset.count_union
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ max (count a s) (count a t) ≤ 1

Tactic:
max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)

Premises used: Multiset.nodup_iff_count_le_one, max_le, Iff.mp
-- Module: Mathlib.Data.Multiset.UnionInter
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ max (count a s) (count a t) ≤ 1

Tactic:
exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)

Premises used: Multiset.nodup_iff_count_le_one, max_le, Iff.mp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
inst : IsEmpty α
a : Multiset α
⊢ Eq.{u_1 + 1} (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) []) 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
inst : IsEmpty α
a_1 : Multiset α
a : α
l : List α
⊢ Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (a :: l)) 0

Tactic:
isEmptyElim a

Premises used: isEmptyElim
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
inst : IsEmpty α
a : Multiset α
⊢ Eq.{u_1 + 1} (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) []) 0

Tactic:
exacts [rfl, isEmptyElim a]

Premises used: rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) (↑[] : Multiset α) 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) ∅ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α) = 0 ↔ l = []

Tactic:
Iff.trans coe_eq_coe perm_nil

Premises used: List.perm_nil, Multiset.coe_eq_coe, Iff.trans
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α) = 0 ↔ l.isEmpty = true

Tactic:
Iff.trans (coe_eq_zero l) isEmpty_iff.symm

Premises used: Multiset.coe_eq_zero, List.isEmpty_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ insert a s = a ::ₘ s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
l : List α
⊢ a ::ₘ (↑l : Multiset α) = (↑(a :: l) : Multiset α)

Tactic:
rfl

Premises used: Multiset.cons, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
s : Multiset α
⊢ a ::ₘ s = b ::ₘ s ↔ a = b

Tactic:
⟨Quot.inductionOn s fun l e =>
      have : [a] ++ l ~ [b] ++ l := Quotient.exact e
      singleton_perm_singleton.1 <| (perm_append_right_iff _).1 this,
    congr_arg (· ::ₘ _)⟩

Premises used: Quot.inductionOn, Multiset.cons, congr_arg, Iff.intro
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
l₁ : List α
t : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁ =
      a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂ ↔
    Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₁)
      (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l₂)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) [])

Tactic:
empty

Premises used: Multiset.zero, Multiset.ofList
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) [])

Tactic:
exact empty
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
head : α
tail : List α
ih : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) tail)
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (head :: tail))

Tactic:
cons _ _ ih

Premises used: Multiset.cons, Multiset.ofList
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
head : α
tail : List α
ih : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) tail)
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (head :: tail))

Tactic:
exact cons _ _ ih
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s : Multiset α
l : List α
mk : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) [])
mk₁ :
  ∀ (head : α) (tail : List α) (ih : p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) tail)),
    p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (head :: tail))
⊢ p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)

Tactic:
induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih

Premises used: List.nil
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
s : Multiset α
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
⊢ p s

Tactic:
Multiset.induction empty cons s

Premises used: Multiset.induction
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
s : Multiset α
⊢ a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s

Tactic:
Quot.inductionOn s fun _ => Quotient.sound <| Perm.swap _ _ _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x x_1 : List α
h : x ≈ x_1
a : α
l l' : List α
b : C ⟦l⟧
b' : C ⟦l'⟧
hl : l ~ l'
h_1 : b ≍ b'
e_2 : ⟦l⟧ = ⟦l'⟧
⊢ C_cons a ⟦l⟧ b ≍ C_cons a ⟦l'⟧ b'

Tactic:
congr 1
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x x_1 : List α
h : x ≈ x_1
a : α
l l' : List α
b : C ⟦l⟧
b' : C ⟦l'⟧
hl : l ~ l'
h_1 : b ≍ b'
⊢ ⟦l⟧ = ⟦l'⟧

Tactic:
Quot.sound hl

Premises used: Quot.sound, Multiset, Quotient
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x x_1 : List α
h : x ≈ x_1
a : α
l l' : List α
b : C ⟦l⟧
b' : C ⟦l'⟧
hl : l ~ l'
h_1 : b ≍ b'
⊢ ⟦l⟧ = ⟦l'⟧

Tactic:
exact Quot.sound hl

Premises used: Quot.sound
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
⊢ Multiset.recOn (C := C) 0 C_0 C_cons C_cons_heq = C_0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.recOn, Multiset.ofList, Multiset.rec, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
a : α
m : Multiset α
⊢ (a ::ₘ m).recOn (C := fun (x : Multiset α) ↦ C x) C_0 C_cons C_cons_heq =
    C_cons a m (m.recOn (C := fun (x : Multiset α) ↦ C x) C_0 C_cons C_cons_heq)

Tactic:
Quotient.inductionOn m fun _ => rfl

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
s : Multiset α
⊢ a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s

Tactic:
Quot.inductionOn s fun _ => List.mem_cons

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
s : Multiset α
h : a ∈ s
⊢ a ∈ b ::ₘ s

Tactic:
mem_cons.2 <| Or.inr h

Premises used: Iff.mpr, Multiset.mem_cons, Or.inr
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ a ∈ a ::ₘ s

Tactic:
mem_cons.2 (Or.inl rfl)

Premises used: Iff.mpr, Multiset.mem_cons, Or.inl, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : α → Prop
a : α
s : Multiset α
⊢ (∀ (x : α), x ∈ a ::ₘ s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x

Tactic:
Quotient.inductionOn' s fun _ => List.forall_mem_cons

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ a ∈ s → ∃ (t : Multiset α), s = a ::ₘ t

Tactic:
Quot.inductionOn s fun l (h : a ∈ l) =>
    let ⟨l₁, l₂, e⟩ := append_of_mem h
    e.symm ▸ ⟨(l₁ ++ l₂ : List α), Quot.sound perm_middle⟩

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ ¬Membership.mem (γ := Multiset α) 0 a

Tactic:
List.not_mem_nil

Premises used: Multiset.Mem, List.not_mem_nil
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x
rw : Eq.{u_1 + 1} (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) []) 0
⊢ Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) 0

Tactic:
rw [eq_nil_iff_forall_not_mem.mpr H]

Premises used: Iff.mpr, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) x
⊢ Eq.{u_1 + 1} (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) []) 0

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s = 0 ↔ ∀ (a : α), ¬a ∈ s

Tactic:
⟨fun h => h.symm ▸ fun _ => notMem_zero _, eq_zero_of_forall_notMem⟩

Premises used: Multiset.notMem_zero, Eq.rec, Iff.intro, Multiset.eq_zero_of_forall_notMem, Eq.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
l_1 : List α
hl : Ne (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l_1) 0
a : α
l : List α
h : Ne (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (a :: l)) 0
⊢ Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) (a :: l)) a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s = 0 ∨ ∃ (a : α), a ∈ s

Tactic:
or_iff_not_imp_left.mpr Multiset.exists_mem_of_ne_zero

Premises used: Iff.mpr, Classical.or_iff_not_imp_left, Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
m : Multiset α
⊢ 0 ≠ a ::ₘ m

Tactic:
fun h =>
  have : a ∈ (0 : Multiset α) := h.symm ▸ mem_cons_self _ _
  notMem_zero _ this

Premises used: Multiset.notMem_zero, Eq.rec, Multiset.mem_cons_self, Eq.symm, Not
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
m : Multiset α
⊢ a ::ₘ m ≠ 0

Tactic:
zero_ne_cons.symm

Premises used: Ne.symm, Multiset.zero_ne_cons