awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
haveI :
  ∀ (this : DecidableEq α),
    a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
haveI : DecidableEq α := Classical.decEq α
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
mp : a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
mpr : (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
pos : ∀ (h : a = b), a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
neg : ∀ (h : ¬a = b), a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
by_cases h : a = b
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : a = b
pos : ∀ (eq : a ::ₘ as = a ::ₘ bs), a = a ∧ as = bs ∨ a ≠ a ∧ ∃ (cs : Multiset α), as = a ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
subst h
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = a ::ₘ bs
⊢ a = a ∧ as = bs ∨ a ≠ a ∧ ∃ (cs : Multiset α), as = a ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a ∈ b ::ₘ bs

Tactic:
have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a ∈ bs

Tactic:
simpa [h]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a ∈ bs

Tactic:
have : a ∈ bs := by simpa [h]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
neg :
  ∀ (cs : Multiset α) (hcs : bs = a ::ₘ cs),
    a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
rcases exists_cons_of_mem this with ⟨cs, hcs⟩

Premises used: Multiset.exists_cons_of_mem
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
neg : as = b ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
simp only [h, hcs, false_and, ne_eq, not_false_eq_true, cons_inj_right, exists_eq_right',
        true_and, false_or]

Premises used: exists_eq_right', false_and, false_or, ne_eq, Multiset.cons_inj_right, not_false_eq_true, true_and
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs

Tactic:
simp [eq, hcs]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs

Tactic:
have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this_3 : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this rwa rwa₁ rwa₂ rwa₃ : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = a ::ₘ b ::ₘ cs

Tactic:
rwa [cons_swap]

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this_3 : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = a ::ₘ b ::ₘ cs

Tactic:
have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this_1 : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this_2 : a ∈ b ::ₘ bs
this_3 : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this_4 : a ::ₘ as = b ::ₘ a ::ₘ cs
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs

Tactic:
simpa using this
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ (cs : Multiset α), as = b ::ₘ cs ∧ bs = a ::ₘ cs
mpr : ∀ (eq₁ : a = b) (eq₂ : as = bs), a ::ₘ as = b ::ₘ bs
mpr₁ : a ≠ b → ∀ (cs : Multiset α) (eq₁ : as = b ::ₘ cs) (eq₂ : bs = a ::ₘ cs), a ::ₘ as = b ::ₘ bs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq₁ : a = b
eq₂ : as = bs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
left : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
simp [*, cons_swap a b]

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
γ : Type u_2
⊢ LawfulSingleton α (Multiset α)

Tactic:
⟨fun _ => rfl⟩

Premises used: LawfulSingleton.mk, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ a ::ₘ 0 = {a}

Tactic:
rfl

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

Tactic:
rfl

Premises used: Multiset.cons, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
⊢ Membership.mem (γ := Multiset α) {a} b ↔ b = a

Tactic:
simp only [← cons_zero, mem_cons, iff_self, or_false, notMem_zero]

Premises used: Multiset.notMem_zero, iff_self, Multiset.mem_cons, or_false, Multiset.cons_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0

Tactic:
mem_cons_self _ _

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0

Tactic:
exact mem_cons_self _ _

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b

Tactic:
cons_inj_left _

Premises used: Multiset.cons_inj_left
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b

Tactic:
exact cons_inj_left _

Premises used: Multiset.cons_inj_left
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
l : List α
a : α
rw : (↑l : Multiset α) = (↑[a] : Multiset α) ↔ l = [a]
rw₁ : l ~ [a] ↔ l = [a]
rw₂ rw₃ : l = [a] ↔ l = [a]
⊢ (↑l : Multiset α) = {a} ↔ l = [a]

Tactic:
rw [← coe_singleton, coe_eq_coe, List.perm_singleton]

Premises used: List.perm_singleton, Multiset.coe_eq_coe, Multiset.coe_singleton
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
m : Multiset α
rw : (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ (cs : Multiset α), 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0

Tactic:
rw [← cons_zero, cons_eq_cons]

Premises used: Multiset.cons_eq_cons, Multiset.cons_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ (cs : Multiset α), 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
x y : α
⊢ Eq (α := Multiset α) {x, y} {y, x}

Tactic:
cons_swap x y 0

Premises used: Multiset.cons_swap, OfNat.ofNat
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ 0 ⊆ s

Tactic:
fun _ => not_mem_nil.elim

Premises used: Multiset.Mem, Not.elim, Multiset.Subset, List.not_mem_nil
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s ⊆ a ::ₘ s

Tactic:
fun _ => mem_cons_of_mem

Premises used: Multiset.mem_cons_of_mem, Multiset.Subset
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
ha : ¬a ∈ s
⊢ s ⊂ a ::ₘ s

Tactic:
⟨subset_cons _ _, fun h => ha <| h <| mem_cons_self _ _⟩

Premises used: Multiset.subset_cons, And.intro, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
simp [subset_iff, or_imp, forall_and]

Premises used: or_imp, Multiset.subset_iff, forall_and
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ s ⊆ t → a ::ₘ s ⊆ a ::ₘ t

Tactic:
Quotient.inductionOn₂ s t fun _ _ => List.cons_subset_cons _

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
h : s ⊆ 0
⊢ s = 0

Tactic:
eq_zero_of_forall_notMem fun _ hx ↦ notMem_zero _ (h hx)

Premises used: Multiset.notMem_zero, Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s ⊆ 0 ↔ s = 0

Tactic:
⟨eq_zero_of_subset_zero, fun xeq => xeq.symm ▸ Subset.refl 0⟩

Premises used: Multiset.eq_zero_of_subset_zero, Eq.rec, Multiset.Subset.refl, Iff.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ 0 ⊂ s ↔ s ≠ 0

Tactic:
simp [ssubset_iff_subset_not_subset]

Premises used: ssubset_iff_subset_not_subset
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ {a} ⊆ s ↔ a ∈ s

Tactic:
simp [subset_iff]

Premises used: Multiset.subset_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
p : Multiset α → Prop
S : Multiset α
h₁ : p 0
h₂ : ∀ {a : α} {s : Multiset α}, a ∈ S → s ⊆ S → p s → p (insert a s)
⊢ p S

Tactic:
@Multiset.induction_on α (fun T => T ⊆ S → p T) S (fun _ => h₁)
    (fun _ _ hps hs =>
      let ⟨hS, sS⟩ := cons_subset.1 hs
      h₂ hS sS (hps sS))
    (Subset.refl S)

Premises used: _private.0.Multiset.induction_on'.match_1, Multiset.cons_subset, Multiset.cons, Multiset.induction_on, Multiset.Subset.refl, Iff.mp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ 0 ≤ s

Tactic:
Quot.inductionOn s fun l => (nil_sublist l).subperm

Premises used: Quot.inductionOn
-- 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
s : Multiset α
⊢ s ≤ 0 ↔ s = 0

Tactic:
le_bot_iff

Premises used: le_bot_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
l : List α
this : l <+~ a :: l ∧ ¬l ~ a :: l
⊢ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l < a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l

Tactic:
simpa [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s ≤ a ::ₘ s

Tactic:
le_of_lt <| lt_cons_self _ _

Premises used: le_of_lt, Multiset.lt_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
⊢ a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
Quotient.inductionOn₂ s t fun _ _ => subperm_cons a

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

Tactic:
(cons_le_cons_iff a).2

Premises used: Iff.mpr, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
⊢ a ::ₘ s < a ::ₘ t ↔ s < t

Tactic:
lt_iff_lt_of_le_iff_le' (cons_le_cons_iff _) (cons_le_cons_iff _)

Premises used: lt_iff_lt_of_le_iff_le', Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
h : s < t
⊢ a ::ₘ s < a ::ₘ t

Tactic:
cons_lt_cons_iff.2 h

Premises used: Iff.mpr, Multiset.cons_lt_cons_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
⟨?_, fun h => le_trans h <| le_cons_self _ _⟩

Premises used: Iff.intro, Multiset.le_cons_self, le_trans
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
refine : s ≤ a ::ₘ t → s ≤ t
⊢ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))

Premises used: Iff.mp, Multiset.mem_cons_self, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))

Premises used: Iff.mp, Multiset.mem_cons_self, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
suffices : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
suffices ∀ {t'}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t' by
    exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
revert : ∀ (m : ¬a ∈ s), a ∈ t' → a ::ₘ s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'

Tactic:
revert m
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ (m : ¬a ∈ s), a ∈ t' → a ::ₘ s ≤ t'

Tactic:
leInductionOn h ?_

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
refine :
  ∀ {l₁ l₂ : List α},
    l₁ <+ l₂ → ∀ (m : ¬a ∈ (↑l₁ : Multiset α)), a ∈ (↑l₂ : Multiset α) → a ::ₘ (↑l₁ : Multiset α) ≤ (↑l₂ : Multiset α)
⊢ ∀ (m : ¬a ∈ s), a ∈ t' → a ::ₘ s ≤ t'

Tactic:
refine leInductionOn h ?_
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
t' : Multiset α
h : s_1 ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ (↑l₁ : Multiset α)
m₂ : a ∈ (↑l₂ : Multiset α)
rcases :
  ∀ (r₁ r₂ : List α) (s : l₁ <+ r₁ ++ a :: r₂) (m₂ : a ∈ (↑(r₁ ++ a :: r₂) : Multiset α)),
    a ::ₘ (↑l₁ : Multiset α) ≤ (↑(r₁ ++ a :: r₂) : Multiset α)
⊢ a ::ₘ (↑l₁ : Multiset α) ≤ (↑l₂ : Multiset α)

Tactic:
rcases append_of_mem m₂ with ⟨r₁, r₂, rfl⟩

Premises used: List.append_of_mem, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
t' : Multiset α
h : s_1 ≤ t'
l₁ : List α
m₁ : ¬a ∈ (↑l₁ : Multiset α)
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ (↑(r₁ ++ a :: r₂) : Multiset α)
⊢ a ::ₘ (↑l₁ : Multiset α) ≤ (↑(r₁ ++ a :: r₂) : Multiset α)

Tactic:
perm_middle.subperm_left.2
      ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

Premises used: Iff.mpr, List.sublist_or_mem_of_sublist, Multiset.Le, List.Subperm, List.subperm_cons, List.perm_middle, Or.resolve_right, List.Sublist.subperm, List.Perm.subperm_left
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
t' : Multiset α
h : s_1 ≤ t'
l₁ : List α
m₁ : ¬a ∈ (↑l₁ : Multiset α)
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ (↑(r₁ ++ a :: r₂) : Multiset α)
⊢ a ::ₘ (↑l₁ : Multiset α) ≤ (↑(r₁ ++ a :: r₂) : Multiset α)

Tactic:
exact
    perm_middle.subperm_left.2
      ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

Premises used: Iff.mpr, List.sublist_or_mem_of_sublist, List.subperm_cons, List.perm_middle, Or.resolve_right, List.Sublist.subperm, List.Perm.subperm_left
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
apply : a ∈ t ∧ s ≤ t → a ::ₘ s ≤ t
⊢ a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

Tactic:
apply Iff.intro (fun h ↦ ⟨subset_of_le h (mem_cons_self a s), le_trans (le_cons_self s a) h⟩)

Premises used: Iff.intro
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
rcases : ∀ (w : Multiset α) (h₁ : a ∈ a ::ₘ w) (h₂ : s ≤ a ::ₘ w), a ::ₘ s ≤ a ::ₘ w
⊢ a ::ₘ s ≤ t

Tactic:
rcases exists_cons_of_mem h₁ with ⟨_, rfl⟩

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
hs : ¬a ∈ s
w : Multiset α
h₁ : a ∈ a ::ₘ w
h₂ : s ≤ a ::ₘ w
⊢ a ::ₘ s ≤ a ::ₘ w

Tactic:
cons_le_cons _ ((le_cons_of_notMem hs).mp h₂)

Premises used: Iff.mp, Multiset.le_cons_of_notMem, Multiset.cons_le_cons
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
hs : ¬a ∈ s
w : Multiset α
h₁ : a ∈ a ::ₘ w
h₂ : s ≤ a ::ₘ w
⊢ a ::ₘ s ≤ a ::ₘ w

Tactic:
exact cons_le_cons _ ((le_cons_of_notMem hs).mp h₂)

Premises used: Iff.mp, Multiset.le_cons_of_notMem, Multiset.cons_le_cons
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ Ne (α := Multiset α) {a} 0

Tactic:
ne_of_gt (lt_cons_self _ _)

Premises used: ne_of_gt, Multiset.lt_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ Ne (α := Multiset α) 0 {a}

Tactic:
singleton_ne_zero _ |>.symm

Premises used: Ne.symm, Multiset.singleton_ne_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ {a} ≤ s ↔ a ∈ s

Tactic:
⟨fun h => mem_of_le h (mem_singleton_self _), fun h =>
    let ⟨_t, e⟩ := exists_cons_of_mem h
    e.symm ▸ cons_le_cons _ (zero_le _)⟩

Premises used: Multiset.exists_cons_of_mem, Eq.rec, LE.le, Multiset.mem_of_le, Iff.intro, _private.0.Multiset.singleton_le.match_1, Multiset.mem_singleton_self, Multiset.zero_le, Singleton.singleton, Eq.symm, Multiset.cons_le_cons
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
l : List α
⊢ LE.le (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) {a} ↔
    Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) 0 ∨
      Eq (α := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) {a}

Tactic:
simp only [← coe_singleton, quot_mk_to_coe'', coe_le,
    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]

Premises used: Multiset.coe_le, Multiset.coe_eq_zero, List.perm_singleton, Multiset.coe_eq_coe, Multiset.coe_singleton, List.subperm_singleton_iff, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
simp : s = 0 → ¬s = {a}
⊢ s < {a} ↔ s = 0

Tactic:
simp only [lt_iff_le_and_ne, le_singleton, or_and_right, Ne, and_not_self, or_false,
    and_iff_left_iff_imp]

Premises used: lt_iff_le_and_ne, Multiset.le_singleton, Ne, and_not_self, or_false, or_and_right, and_iff_left_iff_imp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ ¬Eq (α := Multiset α) 0 {a}

Tactic:
(singleton_ne_zero _).symm

Premises used: Ne.symm, Multiset.singleton_ne_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ ¬Eq (α := Multiset α) 0 {a}

Tactic:
exact (singleton_ne_zero _).symm

Premises used: Ne.symm, Multiset.singleton_ne_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s ⊂ {a} ↔ s = 0

Tactic:
⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩

Premises used: False.elim, Multiset.eq_zero_of_subset_zero, And.right, Iff.intro
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
refine_1 : ∀ (hs : s ⊂ {a}) (b : α) (hb : b ∈ s), {a} ⊆ s
refine_2 : s = 0 → s ⊂ {a}
⊢ s ⊂ {a} ↔ s = 0

Tactic:
refine ⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
refine_1 : ∀ (hs : s ⊂ {b}), {b} ⊆ s
⊢ {a} ⊆ s

Tactic:
obtain rfl := mem_singleton.1 (hs.1 hb)

Premises used: Multiset.mem_singleton, And.left, Iff.mp, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
refine_1 refine_1₁ refine_1₂ refine_1₃ : b ∈ s
⊢ {b} ⊆ s

Tactic:
rwa [singleton_subset]

Premises used: Multiset.singleton_subset
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ SSubset (α := Multiset α) 0 {a}

Tactic:
simp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
⊢ card.{u_1} (α := α) 0 = 0

Tactic:
rfl

Premises used: Multiset.card, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ (a ::ₘ s).card = s.card + 1

Tactic:
Quot.inductionOn s fun _l => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
⊢ card (α := α) {a} = 1

Tactic:
simp only [← cons_zero, card_zero, card_cons]

Premises used: Multiset.card_cons, Multiset.card_zero, Multiset.cons_zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a b : α
rw : (a ::ₘ {b}).card = 2
rw₁ : card (α := α) {b} + 1 = 2
rw₂ rw₃ : HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ card (α := α) {a, b} = 2

Tactic:
rw [insert_eq_cons, card_cons, card_singleton]

Premises used: Multiset.card_singleton, Multiset.card_cons, Multiset.insert_eq_cons
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s.card = 1 ↔ ∃ (a : α), s = {a}

Tactic:
⟨Quot.inductionOn s fun _l h => (List.length_eq_one_iff.1 h).imp fun _a => congr_arg _,
    fun ⟨_a, e⟩ => e.symm ▸ rfl⟩

Premises used: _private.0.Multiset.card_eq_one.match_1, Quot.inductionOn, Eq.rec, Iff.intro, Multiset.card, OfNat.ofNat, Eq.symm, Eq, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
⊢ s < t ↔ ∃ (a : α), a ::ₘ s ≤ t

Tactic:
⟨Quotient.inductionOn₂ s t fun _l₁ _l₂ h =>
      Subperm.exists_of_length_lt (le_of_lt h) (card_lt_card h),
    fun ⟨_a, h⟩ => lt_of_lt_of_le (lt_cons_self _ _) h⟩

Premises used: Multiset.lt_cons_self, Quotient.inductionOn₂, _private.0.Multiset.lt_iff_cons_le.match_1, LT.lt, Iff.intro, lt_of_lt_of_le
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
e : s = 0
⊢ s.card = 0

Tactic:
simp [e]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ 0 < s.card ↔ s ≠ 0

Tactic:
Nat.pos_iff_ne_zero.trans <| not_congr card_eq_zero

Premises used: Multiset.card_eq_zero, Nat.pos_iff_ne_zero, Iff.trans, not_congr
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ 0 < s.card ↔ ∃ (a : α), a ∈ s

Tactic:
Quot.inductionOn s fun _l => length_pos_iff_exists_mem

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s.card = 2 ↔ ∃ (x : α), ∃ (y : α), s = {x, y}

Tactic:
⟨Quot.inductionOn s fun _l h =>
      (List.length_eq_two.mp h).imp fun _a => Exists.imp fun _b => congr_arg _,
    fun ⟨_a, _b, e⟩ => e.symm ▸ rfl⟩

Premises used: Quot.inductionOn, Eq.rec, _private.0.Multiset.card_eq_two.match_1, Iff.intro, Multiset.card, OfNat.ofNat, Eq.symm, Eq, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s.card = 3 ↔ ∃ (x : α), ∃ (y : α), ∃ (z : α), s = {x, y, z}

Tactic:
⟨Quot.inductionOn s fun _l h =>
      (List.length_eq_three.mp h).imp fun _a =>
        Exists.imp fun _b => Exists.imp fun _c => congr_arg _,
    fun ⟨_a, _b, _c, e⟩ => e.symm ▸ rfl⟩

Premises used: _private.0.Multiset.card_eq_three.match_1, Quot.inductionOn, Eq.rec, Iff.intro, Multiset.card, OfNat.ofNat, Eq.symm, Eq, rfl