awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = (a ::ₘ s).erase a

Tactic:
exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
h : a ∈ t
⊢ a ::ₘ t.erase a = t

Tactic:
cons_erase h

Premises used: Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
h : a ∈ t
⊢ a ::ₘ t.erase a = t

Tactic:
exact cons_erase h

Premises used: Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ a ∈ s → (s + t).erase a = s.erase a + t

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

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
rw : (t + s).erase a = s + t.erase a
rw₁ : t.erase a + s = s + t.erase a
rw₂ rw₃ : s + t.erase a = s + t.erase a
⊢ (s + t).erase a = s + t.erase a

Tactic:
rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm]

Premises used: Multiset.add_comm, Multiset.erase_add_left_pos
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ ¬a ∈ s → (s + t).erase a = s + t.erase a

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

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
rw : (t + s).erase a = s.erase a + t
rw₁ : t + s.erase a = s.erase a + t
rw₂ rw₃ : s.erase a + t = s.erase a + t
⊢ (s + t).erase a = s.erase a + t

Tactic:
rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]

Premises used: Multiset.add_comm, Multiset.erase_add_right_neg
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ s.erase a ≤ s

Tactic:
Quot.inductionOn s fun _ => erase_sublist.subperm

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.erase a < s

Tactic:
simpa [h] using lt_cons_self (s.erase a) a

Premises used: Multiset.lt_cons_self, Multiset.erase
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ s.erase a ⊆ s

Tactic:
subset_of_le (erase_le a s)

Premises used: Multiset.subset_of_le, Multiset.erase_le
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
ab : a ≠ b
⊢ a ∈ s.erase b ↔ a ∈ s

Tactic:
Quot.inductionOn s fun _l => List.mem_erase_of_ne ab

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
⊢ a ∈ s.erase b → a ∈ s

Tactic:
mem_of_subset (erase_subset _ _)

Premises used: Multiset.erase_subset, Multiset.mem_of_subset
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a b : α
⊢ (s.erase a).erase b = (s.erase b).erase a

Tactic:
Quot.inductionOn s fun l => congr_arg _ <| l.erase_comm a b

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
γ : Type u_2
inst : DecidableEq α
s t : Multiset α
a b : α
⊢ RightCommutative.{u_1 + 1, u_1 + 1} (α := α) erase

Tactic:
⟨erase_comm⟩

Premises used: RightCommutative.mk, Multiset.erase_comm
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : s ≤ t
⊢ s.erase a ≤ t.erase a

Tactic:
leInductionOn h fun h => (h.erase _).subperm

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ a ::ₘ s.erase a ≤ a ::ₘ t

Tactic:
rw [← cons_erase m] at h

Premises used: Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
h₁ : a ::ₘ s.erase a ≤ a ::ₘ t
⊢ a ∈ s

Tactic:
rw [← cons_erase m] at h

Premises used: Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
(cons_le_cons_iff _).1 h

Premises used: Iff.mp, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
exact (cons_le_cons_iff _).1 h

Premises used: Iff.mp, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s → (s.erase a).card = s.card.pred

Tactic:
Quot.inductionOn s fun _l => length_erase_of_mem

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s → (s.erase a).card + 1 = s.card

Tactic:
Quot.inductionOn s fun _l => length_erase_add_one

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s → (s.erase a).card < s.card

Tactic:
fun h => card_lt_card (erase_lt.mpr h)

Premises used: Iff.mpr, Multiset.erase_lt, Multiset.card_lt_card
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ (s.erase a).card ≤ s.card

Tactic:
card_le_card (erase_le a s)

Premises used: Multiset.card_le_card, Multiset.erase_le
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
pos : ∀ (h : a ∈ s), (s.erase a).card = if a ∈ s then s.card.pred else s.card
neg : ∀ (h : ¬a ∈ s), (s.erase a).card = if a ∈ s then s.card.pred else s.card
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
pos : s.card.pred = if a ∈ s then s.card.pred else s.card
pos₁ : s.card.pred = s.card.pred
pos₂ : a ∈ s
pos₃ : s.card.pred = s.card.pred
pos₄ pos₅ pos₆ : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
rwa [card_erase_of_mem h, if_pos]

Premises used: if_pos, Multiset.card_erase_of_mem
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
neg : s.card = if a ∈ s then s.card.pred else s.card
neg₁ : s.card = s.card
neg₂ : ¬a ∈ s
neg₃ : s.card = s.card
neg₄ neg₅ neg₆ : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
rwa [erase_of_notMem h, if_neg]

Premises used: Multiset.erase_of_notMem, if_neg
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ List.count a (l.erase a) = List.count a l - 1

Tactic:
List.count_erase_self (a := a) (l := l)

Premises used: List.count_erase_self
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
h : count a (erase ⟦l⟧ a) = List.count a (l.erase a)
h₁ : count a ⟦l⟧ = List.count a l
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
convert! List.count_erase_self (a := a) (l := l)

Premises used: List.count_erase_self
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
h : count a (erase ⟦l⟧ a) = count a (↑(l.erase a) : Multiset α)
⊢ count a (erase ⟦l⟧ a) = List.count a (l.erase a)

Tactic:
rw [← coe_count]

Premises used: Multiset.coe_count
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
h : count a ⟦l⟧ = count a (↑l : Multiset α)
⊢ count a ⟦l⟧ = List.count a l

Tactic:
rw [← coe_count]

Premises used: Multiset.coe_count
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a (↑(l.erase a) : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a (↑l : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ List.count a (l.erase b) = List.count a l

Tactic:
List.count_erase_of_ne ab (l := l)

Premises used: List.count_erase_of_ne
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
h : count a (erase ⟦l⟧ b) = List.count a (l.erase b)
h₁ : count a ⟦l⟧ = List.count a l
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧

Tactic:
convert! List.count_erase_of_ne ab (l := l)

Premises used: List.count_erase_of_ne
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
h : count a (erase ⟦l⟧ b) = count a (↑(l.erase b) : Multiset α)
⊢ count a (erase ⟦l⟧ b) = List.count a (l.erase b)

Tactic:
rw [← coe_count]

Premises used: Multiset.coe_count
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
h : count a ⟦l⟧ = count a (↑l : Multiset α)
⊢ count a ⟦l⟧ = List.count a l

Tactic:
rw [← coe_count]

Premises used: Multiset.coe_count
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a (↑(l.erase b) : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a (↑l : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : List α
⊢ (↑s : Multiset α) - (↑t : Multiset α) = (↑(s.diff t) : Multiset α)

Tactic:
rfl

Premises used: Multiset.ofList, Multiset.sub, rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ s - 0 = s

Tactic:
Quot.inductionOn s fun _l => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ s - a ::ₘ t = s.erase a - t

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

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
ih : 0 - s = 0
⊢ 0 - a ::ₘ s = 0

Tactic:
simp [ih]
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ t ≤ s → ∀ (p : α → Prop) [inst_1 : DecidablePred p], countP p (s - t) = countP p s - countP p t

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ hl _ _ ↦ List.countP_diff hl _

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
⊢ ∀ (a_1 b : List α), count a (⟦a_1⟧ - ⟦b⟧) = count a ⟦a_1⟧ - count a ⟦b⟧

Tactic:
simp [List.count_diff]

Premises used: List.count_diff
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
u s : Multiset α
⊢ s - 0 ≤ u ↔ s ≤ u + 0

Tactic:
simp [Multiset.sub_zero]

Premises used: Multiset.sub_zero
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
u : Multiset α
a : α
s_1 : Multiset α
IH : ∀ {s : Multiset α}, s - s_1 ≤ u ↔ s ≤ u + s_1
s : Multiset α
⊢ s - a ::ₘ s_1 ≤ u ↔ s ≤ u + a ::ₘ s_1

Tactic:
simp [IH, erase_le_iff_le_cons]

Premises used: Multiset.erase_le_iff_le_cons
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
empty : ∀ {s : Multiset α}, s - 0 ≤ u ↔ s ≤ u + 0
cons :
  ∀ (a : α) (s : Multiset α) (IH : ∀ {s_1 : Multiset α}, s_1 - s ≤ u ↔ s_1 ≤ u + s) {s_1 : Multiset α},
    s_1 - a ::ₘ s ≤ u ↔ s_1 ≤ u + a ::ₘ s
⊢ s - t ≤ u ↔ s ≤ u + t

Tactic:
induction t using Multiset.induction_on generalizing s with
  | empty => simp [Multiset.sub_zero]
  | cons a s IH => simp [IH, erase_le_iff_le_cons]

Premises used: Multiset.cons, Multiset.erase_le_iff_le_cons, Multiset.sub_zero
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : s ≤ u + t ↔ s ≤ t + u
rw₁ rw₂ : s ≤ t + u ↔ s ≤ t + u
⊢ s - t ≤ u ↔ s ≤ t + u

Tactic:
rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]

Premises used: Multiset.add_comm, Multiset.sub_le_iff_le_add
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
rw : s ≤ s + t
⊢ s - t ≤ s

Tactic:
rw [Multiset.sub_le_iff_le_add]

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

Tactic:
le_add_right _ _

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

Tactic:
exact le_add_right _ _

Premises used: Multiset.le_add_right
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : ∀ (a : α), count a (s + t - u) = count a (s + (t - u))
⊢ s + t - u = s + (t - u)

Tactic:
ext a
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : α
⊢ count a (s + t - u) = count a (s + (t - u))

Tactic:
simp [Nat.add_sub_assoc <| count_le_of_le _ hut]

Premises used: Nat.add_sub_assoc, Multiset.count_le_of_le
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : ∀ (a : α), count a (s - t + t) = count a s
⊢ s - t + t = s

Tactic:
ext a
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s

Tactic:
simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

Premises used: Multiset.count_le_of_le, Nat.sub_add_cancel
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
a : ∀ (a : α), count a (s - (t + u)) = count a (s - t - u)
⊢ s - (t + u) = s - t - u

Tactic:
ext
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
a : α
⊢ count a (s - (t + u)) = count a (s - t - u)

Tactic:
simp [Nat.sub_add_eq]

Premises used: Nat.sub_add_eq
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ≤ s - t + t

Tactic:
Multiset.sub_le_iff_le_add.1 le_rfl

Premises used: le_rfl, Multiset.sub_le_iff_le_add, Iff.mp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ≤ t + (s - t)

Tactic:
Multiset.sub_le_iff_le_add'.1 le_rfl

Premises used: le_rfl, Multiset.sub_le_iff_le_add', Iff.mp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hst : s ≤ t
⊢ s - u ≤ t - u

Tactic:
Multiset.sub_le_iff_le_add'.mpr <| hst.trans Multiset.le_add_sub

Premises used: Iff.mpr, Multiset.sub_le_iff_le_add', Multiset.le_add_sub, LE.le.trans
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : ∀ (a : α), count a (s + t - t) = count a s
⊢ s + t - t = s

Tactic:
ext a
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hstu : s + t = u
rw : s = s + t - t
rw₁ rw₂ : s = s
⊢ s = u - t

Tactic:
rw [← hstu, Multiset.add_sub_cancel_right]

Premises used: Multiset.add_sub_cancel_right
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
rw : {a} + s - t = a ::ₘ (s - t)
rw₁ : {a} + s - t = {a} + (s - t)
rw₂ rw₃ : {a} + (s - t) = {a} + (s - t)
⊢ a ::ₘ s - t = a ::ₘ (s - t)

Tactic:
rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]

Premises used: Multiset.singleton_add, Multiset.add_sub_assoc
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : t ≤ s
rw : (s - t + t).card = s.card
rw₁ rw₂ : s.card = s.card
⊢ (s - t).card + t.card = s.card

Tactic:
rw [← card_add, Multiset.sub_add_cancel h]

Premises used: Multiset.card_add, Multiset.sub_add_cancel
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a₁ : ∀ (a_1 : α), count a_1 (s - {a}) = count a_1 (s.erase a)
⊢ s - {a} = s.erase a

Tactic:
ext
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
a₁ : (count a_1 s - if a_1 = a then 1 else 0) = count a_1 (s.erase a)
⊢ count a_1 (s - {a}) = count a_1 (s.erase a)

Tactic:
simp only [count_sub, count_singleton]

Premises used: Multiset.count_sub, Multiset.count_singleton
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
a₁ : a_1 = a → count a_1 s - 1 = count a_1 (s.erase a)
a₂ : ¬a_1 = a → count a_1 s - 0 = count a_1 (s.erase a)
⊢ (count a_1 s - if a_1 = a then 1 else 0) = count a_1 (s.erase a)

Tactic:
split
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
h : a_1 = a
⊢ count a_1 s - 1 = count a_1 (s.erase a)

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
a_1 : α
h : ¬a_1 = a
⊢ count a_1 s - 0 = count a_1 (s.erase a)

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Multiset α
rw : 0 < count a (s - t) ↔ count a t < count a s
rw₁ : 0 < count a s - count a t ↔ count a t < count a s
rw₂ rw₃ : count a t < count a s ↔ count a t < count a s
⊢ a ∈ s - t ↔ count a t < count a s

Tactic:
rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]

Premises used: Nat.sub_pos_iff_lt, Multiset.count_pos, Multiset.count_sub
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

Tactic:
simpa using huv
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a : α
b : β
as : Multiset α
bs : Multiset β
hab : r a b
hst : Rel r as bs
ih : Rel r (as + u) (bs + v)
⊢ Rel r (a ::ₘ as + u) (b ::ₘ bs + v)

Tactic:
simpa using ih.cons hab

Premises used: Multiset.Rel.cons
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
zero : Rel r (0 + u) (0 + v)
cons :
  ∀ {a : α} {b : β} {as : Multiset α} {bs : Multiset β} (hab : r a b) (hst : Rel r as bs)
    (ih : Rel r (as + u) (bs + v)), Rel r (a ::ₘ as + u) (b ::ₘ bs + v)
⊢ Rel r (s + u) (t + v)

Tactic:
induction hst with
  | zero => simpa using huv
  | cons hab hst ih => simpa using ih.cons hab

Premises used: Multiset.Rel.zero, Multiset.Rel.cons
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
⊢ ∀ {bs : Multiset β},
    Rel r (0 + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r 0 bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
simp
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
simp :
  (∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            bs = b ::ₘ bs') ↔
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
⊢ Rel r (a ::ₘ s + as₁) bs ↔
    ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
simp only [ih, cons_add, rel_cons_left]

Premises used: Multiset.rel_cons_left, Multiset.cons_add
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
mp :
  (∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            bs = b ::ₘ bs') →
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
mpr :
  (∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
⊢ (∃ (b : β),
      ∃ (bs' : Multiset β),
        r a b ∧
          (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧
            bs = b ::ₘ bs') ↔
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h :
  ∃ (b : β),
    ∃ (bs' : Multiset β),
      r a b ∧
        (∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
mp :
  ∀ (b : β) (bs' : Multiset β) (hab : r a b)
    (h : ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁),
    ∃ (bs₀ : Multiset β),
      ∃ (bs₁ : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ b ::ₘ bs' = bs₀ + bs₁
⊢ ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
rcases h with ⟨b, bs', hab, h, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
bs' : Multiset β
hab : r a b
h : ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁
mp :
  ∀ (bs₀ bs₁ : Multiset β) (h₀ : Rel r s bs₀) (h₁ : Rel r as₁ bs₁),
    ∃ (bs₀_1 : Multiset β),
      ∃ (bs₁_1 : Multiset β),
        (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀_1 = b ::ₘ bs') ∧
          Rel r as₁ bs₁_1 ∧ b ::ₘ (bs₀ + bs₁) = bs₀_1 + bs₁_1
⊢ ∃ (bs₀ : Multiset β),
    ∃ (bs₁ : Multiset β),
      (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ b ::ₘ bs' = bs₀ + bs₁

Tactic:
rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih :
  ∀ {bs : Multiset β},
    Rel r (s + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ b ::ₘ (bs₀ + bs₁) = b ::ₘ bs₀ + bs₁

Tactic:
simp