internlm/Lean-Github huggingface dataset:
Theorem: mapCon_mapForall
Proof state before:
case h.left
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ X ∧ Con (g (a_1, b_1) φ) = Con (g (a, b) φ)
Tactic:
use a, b
Proof state after:
no goals
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ evaluate M w (Con (g (a, b) φ))
Tactic:
rw [conEval]
Proof state after:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f
Tactic:
intro f
Proof state after:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
f : Formula
⊢ f ∈ g (a, b) φ → evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
f : Formula
⊢ f ∈ g (a, b) φ → evaluate M w f
Tactic:
tauto
Proof state after:
no goals
Theorem: undag_boxes
Proof state before:
ps : List Program
df : DagFormula
⊢ undagDagFormula (⌈⌈ps⌉⌉df) = ⌈⌈ps⌉⌉undag df
Tactic:
cases ps
Proof state after:
case nil
df : DagFormula
⊢ undagDagFormula (⌈⌈[]⌉⌉df) = ⌈⌈[]⌉⌉undag df

case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df
Theorem: undag_boxes
Proof state before:
case nil
df : DagFormula
⊢ undagDagFormula (⌈⌈[]⌉⌉df) = ⌈⌈[]⌉⌉undag df

case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df
Tactic:
simp
Proof state after:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df
Theorem: undag_boxes
Proof state before:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈head✝ :: tail✝⌉⌉df) = ⌈⌈head✝ :: tail✝⌉⌉undag df
Tactic:
simp
Proof state after:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈tail✝⌉⌉df) = ⌈⌈tail✝⌉⌉undagDagFormula df
Theorem: undag_boxes
Proof state before:
case cons
df : DagFormula
head✝ : Program
tail✝ : List Program
⊢ undagDagFormula (⌈⌈tail✝⌉⌉df) = ⌈⌈tail✝⌉⌉undagDagFormula df
Tactic:
apply undag_boxes
Proof state after:
no goals
Theorem: undag_inject
Proof state before:
ps : List Program
α : Program
φ : Formula
⊢ undag (inject ps α φ) = ⌈⌈ps⌉⌉⌈∗α⌉φ
Tactic:
simp
Proof state after:
no goals
Theorem: ProgramSequenceNotSelfContaining
Proof state before:
⊢ ∀ (p q : Program), ¬p = (p;'q)
Tactic:
intro p q hyp
Proof state after:
p q : Program
hyp : p = (p;'q)
⊢ False
Theorem: ProgramSequenceNotSelfContaining
Proof state before:
p q : Program
hyp : p = (p;'q)
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramUnionNotSelfContainingLeft
Proof state before:
⊢ ∀ (p q : Program), ¬p = (p⋓q)
Tactic:
intro p q hyp
Proof state after:
p q : Program
hyp : p = (p⋓q)
⊢ False
Theorem: ProgramUnionNotSelfContainingLeft
Proof state before:
p q : Program
hyp : p = (p⋓q)
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramUnionNotSelfContainingLeft'
Proof state before:
⊢ ∀ (p q : Program), ¬(p⋓q) = p
Tactic:
intro p q hyp
Proof state after:
p q : Program
hyp : (p⋓q) = p
⊢ False
Theorem: ProgramUnionNotSelfContainingLeft'
Proof state before:
p q : Program
hyp : (p⋓q) = p
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramUnionNotSelfContainingRight
Proof state before:
⊢ ∀ (p q : Program), ¬q = (p⋓q)
Tactic:
intro p q hyp
Proof state after:
p q : Program
hyp : q = (p⋓q)
⊢ False
Theorem: ProgramUnionNotSelfContainingRight
Proof state before:
p q : Program
hyp : q = (p⋓q)
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramUnionNotSelfContainingRight'
Proof state before:
⊢ ∀ (p q : Program), ¬(p⋓q) = q
Tactic:
intro p q hyp
Proof state after:
p q : Program
hyp : (p⋓q) = q
⊢ False
Theorem: ProgramUnionNotSelfContainingRight'
Proof state before:
p q : Program
hyp : (p⋓q) = q
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramTestNotSelfContain
Proof state before:
ψ : DagFormula
φ : Formula
⊢ ¬ψ = ⌈?'φ⌉ψ
Tactic:
intro hyp
Proof state after:
ψ : DagFormula
φ : Formula
hyp : ψ = ⌈?'φ⌉ψ
⊢ False
Theorem: ProgramTestNotSelfContain
Proof state before:
ψ : DagFormula
φ : Formula
hyp : ψ = ⌈?'φ⌉ψ
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramStarNotSelfContain
Proof state before:
α : Program
⊢ ¬(∗α) = α
Tactic:
intro hyp
Proof state after:
α : Program
hyp : (∗α) = α
⊢ False
Theorem: ProgramStarNotSelfContain
Proof state before:
α : Program
hyp : (∗α) = α
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: ProgramBoxStarNotSelfContain
Proof state before:
α : Program
ψ : DagFormula
⊢ ¬(⌈∗α⌉ψ) = ψ
Tactic:
intro hyp
Proof state after:
α : Program
ψ : DagFormula
hyp : (⌈∗α⌉ψ) = ψ
⊢ False
Theorem: ProgramBoxStarNotSelfContain
Proof state before:
α : Program
ψ : DagFormula
hyp : (⌈∗α⌉ψ) = ψ
⊢ False
Tactic:
cases hyp
Proof state after:
no goals
Theorem: not_MultisetRedLt_0
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
⊢ ¬MultisetRedLt M 0
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
h : MultisetRedLt M 0
⊢ False
Theorem: not_MultisetRedLt_0
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
h : MultisetRedLt M 0
⊢ False
Tactic:
cases h with
| RedLt X Y a M nonsense _ =>
  have contra : a ∈ (0 : Multiset α):= by
    rw [nonsense]
    simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
  contradiction
Proof state after:
no goals
Theorem: not_MultisetRedLt_0
Proof state before:
case RedLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ False
Tactic:
have contra : a ∈ (0 : Multiset α):= by
  rw [nonsense]
  simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
Proof state after:
case RedLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
contra : a ∈ 0
⊢ False
Theorem: not_MultisetRedLt_0
Proof state before:
case RedLt
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
contra : a ∈ 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: not_MultisetRedLt_0
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ 0
Tactic:
rw [nonsense]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ X + {a}
Theorem: not_MultisetRedLt_0
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ X + {a}
Tactic:
simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
Proof state after:
no goals
Theorem: meq_union_meq_reverse
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N P : Multiset α
x✝ : M = N
⊢ M + P = N + P
Tactic:
simp_all only
Proof state after:
no goals
Theorem: mul_cons_trivial
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
⊢ M + {a} = a ::ₘ M
Tactic:
ext
Proof state after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M + {a}) = Multiset.count a✝ (a ::ₘ M)
Theorem: mul_cons_trivial
Proof state before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M + {a}) = Multiset.count a✝ (a ::ₘ M)
Tactic:
simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
Proof state after:
no goals
Theorem: mul_erase_trivial
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
⊢ M - {a} = M.erase a
Tactic:
ext
Proof state after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M - {a}) = Multiset.count a✝ (M.erase a)
Theorem: mul_erase_trivial
Proof state before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M - {a}) = Multiset.count a✝ (M.erase a)
Tactic:
simp [Multiset.erase_singleton]
Proof state after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ M - Multiset.count a✝ {a} = Multiset.count a✝ (M.erase a)
Theorem: mul_erase_trivial
Proof state before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ M - Multiset.count a✝ {a} = Multiset.count a✝ (M.erase a)
Tactic:
simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
Proof state after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ (Multiset.count a✝ M - if a✝ = a then 1 else 0) = Multiset.count a✝ (M.erase a)
Theorem: mul_erase_trivial
Proof state before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ (Multiset.count a✝ M - if a✝ = a then 1 else 0) = Multiset.count a✝ (M.erase a)
Tactic:
aesop
Proof state after:
no goals
Theorem: mul_mem_not_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ M
Tactic:
rw [H]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ (a0 ::ₘ X).erase a
Theorem: mul_mem_not_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ (a0 ::ₘ X).erase a
Tactic:
have : a0 ∈ Multiset.erase (a0 ::ₘ X) a ↔ a0 ∈ (a0 ::ₘ X) := by
  apply Multiset.mem_erase_of_ne
  aesop
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ (a0 ::ₘ X).erase a
Theorem: mul_mem_not_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ (a0 ::ₘ X).erase a
Tactic:
rw [this]
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ a0 ::ₘ X
Theorem: mul_mem_not_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ a0 ::ₘ X
Tactic:
aesop
Proof state after:
no goals
Theorem: mul_mem_not_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
Tactic:
apply Multiset.mem_erase_of_ne
Proof state after:
case ab
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ≠ a
Theorem: mul_mem_not_erase
Proof state before:
case ab
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ≠ a
Tactic:
aesop
Proof state after:
no goals
Theorem: mem_erase_cons
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a0 : α
M : Multiset α
x✝ : a0 ∈ M
⊢ M = M - {a0} + {a0}
Tactic:
simp_all [mul_cons_trivial, mul_erase_trivial, Multiset.cons_erase]
Proof state after:
no goals
Theorem: neq_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
⊢ Multiset.count a0 (M.erase a) = Multiset.count a0 M
Tactic:
have : Multiset.count a0 (a ::ₘ (Multiset.erase M a)) = Multiset.count a0 (a ::ₘ M) := by simp_all
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
this : Multiset.count a0 (a ::ₘ M.erase a) = Multiset.count a0 (a ::ₘ M)
⊢ Multiset.count a0 (M.erase a) = Multiset.count a0 M
Theorem: neq_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
this : Multiset.count a0 (a ::ₘ M.erase a) = Multiset.count a0 (a ::ₘ M)
⊢ Multiset.count a0 (M.erase a) = Multiset.count a0 M
Tactic:
simp_all
Proof state after:
no goals
Theorem: neq_erase
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
⊢ Multiset.count a0 (a ::ₘ M.erase a) = Multiset.count a0 (a ::ₘ M)
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}
⊢ 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
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
⊢ M = X + {a0} - {a}
Tactic:
simp [mul_cons_trivial, mul_erase_trivial] at *
Proof 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
Theorem: cons_erase
Proof 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
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
⊢ M = X + {a0} - {a}
Tactic:
have a0_a: a0 ≠ a := by rw [eq_comm] at hyp; exact hyp
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
⊢ M = X + {a0} - {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
⊢ M = X + {a0} - {a}
Tactic:
ext b
Proof 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})
Theorem: cons_erase
Proof 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]
Proof 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
Theorem: cons_erase
Proof 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
Proof 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
Theorem: cons_erase
Proof 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
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
Tactic:
rw [eq_comm] at hyp
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a0 = a
⊢ a0 ≠ a
Theorem: cons_erase
Proof 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
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 : α
⊢ Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
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:
rw [ba]
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
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = 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
⊢ 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
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
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = 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 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
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}
⊢ Multiset.count a M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = 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 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
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 M = (Multiset.count a X + if a = a0 then 1 else 0) - if a = 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 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
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
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