internlm/Lean-Github huggingface dataset:
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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]
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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]
Proof 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
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof 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)
Theorem: cons_erase
Proof 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]
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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]
Proof 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
Theorem: cons_erase
Proof 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 ]
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof 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)
Theorem: cons_erase
Proof 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]
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: cons_erase
Proof 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
Proof 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)
Theorem: cons_erase
Proof 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
Proof state after:
no goals
Theorem: red_insert
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N : Multiset α
H : MultisetRedLt N (a ::ₘ M)
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
Tactic:
rcases H with ⟨X, Y, a0, H1, H0, H2⟩
Proof state after:
case RedLt
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
Theorem: red_insert
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
Tactic:
exists Y
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = a ::ₘ Y ∧ MultisetRedLt Y M ∨ N = M + Y ∧ ∀ x ∈ Y, x < a
Theorem: red_insert
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = a ::ₘ Y ∧ MultisetRedLt Y M ∨ N = M + Y ∧ ∀ x ∈ Y, x < a
Tactic:
right
Proof state after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y ∧ ∀ x ∈ Y, x < a
Theorem: red_insert
Proof state before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y ∧ ∀ x ∈ Y, x < a
Tactic:
apply And.intro
Proof state after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y

case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Theorem: red_insert
Proof state before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y

case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Tactic:
. rw [H1]
  rw [add_left_inj]
  rw [mul_cons_trivial] at H0
  simp_all
Proof state after:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Theorem: red_insert
Proof state before:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Tactic:
. simp_all
Proof state after:
no goals
Theorem: red_insert
Proof state before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y
Tactic:
rw [H1]
Proof state after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X + Y = M + Y
Theorem: red_insert
Proof state before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X + Y = M + Y
Tactic:
rw [add_left_inj]
Proof state after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M
Theorem: red_insert
Proof state before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M
Tactic:
rw [mul_cons_trivial] at H0
Proof state after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = a0 ::ₘ X
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M