Theorem: cons_erase (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
⊢ M = X + {a0} - {a}
Tactic:
if hyp : a = a0 then
  simp [mul_cons_trivial, mul_erase_trivial] at *
  aesop
else
  have a0_a: a0 ≠ a := by rw [eq_comm] at hyp; exact hyp
  ext b
  simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
  have H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0}) := by aesop
  if ba : b = a then
    rw [ba]
    rw [ba] at H
    have : a ∈ X + {a0} := by
      by_contra h
      have absurd3 : Multiset.count a (a ::ₘ M) > 0 := by simp
      aesop
    have : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1 := by simp
    have : Multiset.count a (a0 ::ₘ X) = Multiset.count a (Multiset.erase (a0 ::ₘ X) a) + 1 := by simp ; aesop
    aesop
  else if ba0 : b = a0 then
    rw [ba0]
    rw [ba0] at H
    have : Multiset.count a0 (Multiset.erase (a ::ₘ M) a) = Multiset.count a0 (Multiset.erase (a ::ₘ M) a) := by
      simp
    have : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1 := by subst_eqs; rw [mul_cons_trivial] at H; simp_all
    have : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M) := by
      have : a0 ≠ a := by simp_all
      rw [Multiset.count_cons_of_ne this M]
    simp_all
    else
    have : Multiset.count b M = Multiset.count b (a ::ₘ M) := by
      have : b ≠ a := by simp_all
      rw [Multiset.count_cons_of_ne this M]
    rw [this ]
    have : Multiset.count b (X + {a0}) = Multiset.count b (Multiset.erase (a0 ::ₘ X) a) := by
      simp
      simp_all
    simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : a = a0
⊢ M = X + {a0} - {a}
Tactic:
simp [mul_cons_trivial, mul_erase_trivial] at *
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
hyp : a = a0
H : a ::ₘ M = a0 ::ₘ X
⊢ M = (a0 ::ₘ X).erase a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
hyp : a = a0
H : a ::ₘ M = a0 ::ₘ X
⊢ M = (a0 ::ₘ X).erase a
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
⊢ M = X + {a0} - {a}
Tactic:
have a0_a: a0 ≠ a := by rw [eq_comm] at hyp; exact hyp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
⊢ M = X + {a0} - {a}

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
⊢ M = X + {a0} - {a}
Tactic:
ext b
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
⊢ Multiset.count b M = Multiset.count b (X + {a0} - {a})

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
⊢ Multiset.count b M = Multiset.count b (X + {a0} - {a})
Tactic:
simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
have H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0}) := by aesop
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
if ba : b = a then
  rw [ba]
  rw [ba] at H
  have : a ∈ X + {a0} := by
    by_contra h
    have absurd3 : Multiset.count a (a ::ₘ M) > 0 := by simp
    aesop
  have : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1 := by simp
  have : Multiset.count a (a0 ::ₘ X) = Multiset.count a (Multiset.erase (a0 ::ₘ X) a) + 1 := by simp ; aesop
  aesop
else if ba0 : b = a0 then
  rw [ba0]
  rw [ba0] at H
  have : Multiset.count a0 (Multiset.erase (a ::ₘ M) a) = Multiset.count a0 (Multiset.erase (a ::ₘ M) a) := by
    simp
  have : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1 := by subst_eqs; rw [mul_cons_trivial] at H; simp_all
  have : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M) := by
    have : a0 ≠ a := by simp_all
    rw [Multiset.count_cons_of_ne this M]
  simp_all
  else
  have : Multiset.count b M = Multiset.count b (a ::ₘ M) := by
    have : b ≠ a := by simp_all
    rw [Multiset.count_cons_of_ne this M]
  rw [this ]
  have : Multiset.count b (X + {a0}) = Multiset.count b (Multiset.erase (a0 ::ₘ X) a) := by
    simp
    simp_all
  simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
⊢ a0 ≠ a
Tactic:
rw [eq_comm] at hyp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a0 = a
⊢ a0 ≠ a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a0 = a
⊢ a0 ≠ a
Tactic:
exact hyp
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
⊢ Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : b = a
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
rw [ba]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : b = a
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : b = a
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0
Tactic:
rw [ba] at H
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0
Tactic:
have : a ∈ X + {a0} := by
  by_contra h
  have absurd3 : Multiset.count a (a ::ₘ M) > 0 := by simp
  aesop
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this : a ∈ X + {a0}
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this : a ∈ X + {a0}
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0
Tactic:
have : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1 := by simp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝ : a ∈ X + {a0}
this : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝ : a ∈ X + {a0}
this : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0
Tactic:
have : Multiset.count a (a0 ::ₘ X) = Multiset.count a (Multiset.erase (a0 ::ₘ X) a) + 1 := by simp ; aesop
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝¹ : a ∈ X + {a0}
this✝ : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
this : Multiset.count a (a0 ::ₘ X) = Multiset.count a ((a0 ::ₘ X).erase a) + 1
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝¹ : a ∈ X + {a0}
this✝ : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
this : Multiset.count a (a0 ::ₘ X) = Multiset.count a ((a0 ::ₘ X).erase a) + 1
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = a then 1 else 0
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
⊢ a ∈ X + {a0}
Tactic:
by_contra h
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
h : a ∉ X + {a0}
⊢ False

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
h : a ∉ X + {a0}
⊢ False
Tactic:
have absurd3 : Multiset.count a (a ::ₘ M) > 0 := by simp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
h : a ∉ X + {a0}
absurd3 : Multiset.count a (a ::ₘ M) > 0
⊢ False

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
h : a ∉ X + {a0}
absurd3 : Multiset.count a (a ::ₘ M) > 0
⊢ False
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
h : a ∉ X + {a0}
⊢ Multiset.count a (a ::ₘ M) > 0
Tactic:
simp
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this : a ∈ X + {a0}
⊢ Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
Tactic:
simp
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝ : a ∈ X + {a0}
this : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
⊢ Multiset.count a (a0 ::ₘ X) = Multiset.count a ((a0 ::ₘ X).erase a) + 1
Tactic:
simp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝ : a ∈ X + {a0}
this : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
⊢ Multiset.count a (a0 ::ₘ X) = Multiset.count a (a0 ::ₘ X) - 1 + 1

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a (a ::ₘ M) = Multiset.count a (X + {a0})
ba : b = a
this✝ : a ∈ X + {a0}
this : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1
⊢ Multiset.count a (a0 ::ₘ X) = Multiset.count a (a0 ::ₘ X) - 1 + 1
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
if ba0 : b = a0 then
rw [ba0]
rw [ba0] at H
have : Multiset.count a0 (Multiset.erase (a ::ₘ M) a) = Multiset.count a0 (Multiset.erase (a ::ₘ M) a) := by
simp
have : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1 := by subst_eqs; rw [mul_cons_trivial] at H; simp_all
have : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M) := by
have : a0 ≠ a := by simp_all
rw [Multiset.count_cons_of_ne this M]
simp_all
else
have : Multiset.count b M = Multiset.count b (a ::ₘ M) := by
have : b ≠ a := by simp_all
rw [Multiset.count_cons_of_ne this M]
rw [this ]
have : Multiset.count b (X + {a0}) = Multiset.count b (Multiset.erase (a0 ::ₘ X) a) := by
simp
simp_all
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : b = a0
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
rw [ba0]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : b = a0
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : b = a0
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0
Tactic:
rw [ba0] at H
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0
Tactic:
have : Multiset.count a0 (Multiset.erase (a ::ₘ M) a) = Multiset.count a0 (Multiset.erase (a ::ₘ M) a) := by
  simp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0
Tactic:
have : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1 := by subst_eqs; rw [mul_cons_trivial] at H; simp_all
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0
Tactic:
have : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M) := by
  have : a0 ≠ a := by simp_all
  rw [Multiset.count_cons_of_ne this M]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝¹ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this✝ : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
this : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M)
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝¹ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this✝ : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
this : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M)
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
⊢ Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
Tactic:
simp
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
⊢ Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
Tactic:
subst_eqs
State after:
case refl.refl
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬a0 = a
⊢ Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1

State before:
case refl.refl
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬a0 = a
⊢ Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
Tactic:
rw [mul_cons_trivial] at H
State after:
case refl.refl
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (a0 ::ₘ X)
ba : ¬a0 = a
⊢ Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1

State before:
case refl.refl
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (a0 ::ₘ X)
ba : ¬a0 = a
⊢ Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
⊢ Multiset.count a0 M = Multiset.count a0 (a ::ₘ M)
Tactic:
have : a0 ≠ a := by simp_all
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝¹ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this✝ : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
this : a0 ≠ a
⊢ Multiset.count a0 M = Multiset.count a0 (a ::ₘ M)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝¹ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this✝ : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
this : a0 ≠ a
⊢ Multiset.count a0 M = Multiset.count a0 (a ::ₘ M)
Tactic:
rw [Multiset.count_cons_of_ne this M]
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 (X + {a0})
ba : ¬b = a
ba0 : b = a0
this✝ : Multiset.count a0 ((a ::ₘ M).erase a) = Multiset.count a0 ((a ::ₘ M).erase a)
this : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1
⊢ a0 ≠ a
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
have : Multiset.count b M = Multiset.count b (a ::ₘ M) := by
  have : b ≠ a := by simp_all
  rw [Multiset.count_cons_of_ne this M]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
rw [this ]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b (a ::ₘ M) = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b (a ::ₘ M) = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
have : Multiset.count b (X + {a0}) = Multiset.count b (Multiset.erase (a0 ::ₘ X) a) := by
  simp
  simp_all
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this✝ : Multiset.count b M = Multiset.count b (a ::ₘ M)
this : Multiset.count b (X + {a0}) = Multiset.count b ((a0 ::ₘ X).erase a)
⊢ Multiset.count b (a ::ₘ M) = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this✝ : Multiset.count b M = Multiset.count b (a ::ₘ M)
this : Multiset.count b (X + {a0}) = Multiset.count b ((a0 ::ₘ X).erase a)
⊢ Multiset.count b (a ::ₘ M) = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
⊢ Multiset.count b M = Multiset.count b (a ::ₘ M)
Tactic:
have : b ≠ a := by simp_all
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : b ≠ a
⊢ Multiset.count b M = Multiset.count b (a ::ₘ M)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : b ≠ a
⊢ Multiset.count b M = Multiset.count b (a ::ₘ M)
Tactic:
rw [Multiset.count_cons_of_ne this M]
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
⊢ b ≠ a
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b (X + {a0}) = Multiset.count b ((a0 ::ₘ X).erase a)
Tactic:
simp
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b X + Multiset.count b {a0} = Multiset.count b ((a0 ::ₘ X).erase a)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b X + Multiset.count b {a0} = Multiset.count b ((a0 ::ₘ X).erase a)
Tactic:
simp_all
State after:
no goals