internlm/Lean-Github huggingface dataset:
Theorem: mord_wf_3
Proof state before:
case intro
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ AccM_1 (x ::ₘ M)
Tactic:
apply @mord_wf_2 α _ _ _ _ _ accM1
Proof state after:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ ∀ (b : α) (M : Multiset α), b < x → AccM_1 M → AccM_1 (b ::ₘ M)
Theorem: mord_wf_3
Proof state before:
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
w x : α
h✝ : ∀ y < x, Acc LT.lt y
ih : ∀ y < x, ∀ (M : Multiset α), AccM_1 M → AccM_1 (y ::ₘ M)
M : Multiset α
accM1 : AccM_1 M
⊢ ∀ (b : α) (M : Multiset α), b < x → AccM_1 M → AccM_1 (b ::ₘ M)
Tactic:
simp_all
Proof state after:
no goals
Theorem: mred_acc
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (M : Multiset α), (∀ x ∈ M, Acc LT.lt x) → AccM_1 M
Tactic:
intros M wf_el
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M : Multiset α
wf_el : ∀ x ∈ M, Acc LT.lt x
⊢ AccM_1 M
Theorem: mred_acc
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M : Multiset α
wf_el : ∀ x ∈ M, Acc LT.lt x
⊢ AccM_1 M
Tactic:
induction M using Multiset.induction_on with | empty =>
  constructor
  intro y y_lt
  absurd y_lt
  apply not_MultisetRedLt_0
| cons _ _ ih =>
  apply mord_wf_3
  . assumption
  . apply wf_el
    simp_all
  . apply ih
    intros
    apply wf_el
    simp_all
Proof state after:
no goals
Theorem: mred_acc
Proof state before:
case empty
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ AccM_1 0
Tactic:
constructor
Proof state after:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), MultisetRedLt y 0 → Acc MultisetRedLt y
Theorem: mred_acc
Proof state before:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), MultisetRedLt y 0 → Acc MultisetRedLt y
Tactic:
intro y y_lt
Proof state after:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ Acc MultisetRedLt y
Theorem: mred_acc
Proof state before:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ Acc MultisetRedLt y
Tactic:
absurd y_lt
Proof state after:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ ¬MultisetRedLt y 0
Theorem: mred_acc
Proof state before:
case empty.h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_el : ∀ x ∈ 0, Acc LT.lt x
y : Multiset α
y_lt : MultisetRedLt y 0
⊢ ¬MultisetRedLt y 0
Tactic:
apply not_MultisetRedLt_0
Proof state after:
no goals
Theorem: mred_acc
Proof state before:
case cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 (a✝ ::ₘ s✝)
Tactic:
apply mord_wf_3
Proof state after:
case cons.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Multiset α

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Theorem: mred_acc
Proof state before:
case cons.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Multiset α

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
. assumption
Proof state after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Theorem: mred_acc
Proof state before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝

case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
. apply wf_el
  simp_all
Proof state after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Theorem: mred_acc
Proof state before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
. apply ih
  intros
  apply wf_el
  simp_all
Proof state after:
no goals
Theorem: mred_acc
Proof state before:
case cons.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Multiset α
Tactic:
assumption
Proof state after:
no goals
Theorem: mred_acc
Proof state before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ Acc LT.lt a✝
Tactic:
apply wf_el
Proof state after:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ a✝ ∈ a✝ ::ₘ s✝
Theorem: mred_acc
Proof state before:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ a✝ ∈ a✝ ::ₘ s✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: mred_acc
Proof state before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ AccM_1 s✝
Tactic:
apply ih
Proof state after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ ∀ x ∈ s✝, Acc LT.lt x
Theorem: mred_acc
Proof state before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝ ::ₘ s✝, Acc LT.lt x
⊢ ∀ x ∈ s✝, Acc LT.lt x
Tactic:
intros
Proof state after:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ Acc LT.lt x✝
Theorem: mred_acc
Proof state before:
case cons.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ Acc LT.lt x✝
Tactic:
apply wf_el
Proof state after:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ x✝ ∈ a✝¹ ::ₘ s✝
Theorem: mred_acc
Proof state before:
case cons.a.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a✝¹ : α
s✝ : Multiset α
ih : (∀ x ∈ s✝, Acc LT.lt x) → AccM_1 s✝
wf_el : ∀ x ∈ a✝¹ ::ₘ s✝, Acc LT.lt x
x✝ : α
a✝ : x✝ ∈ s✝
⊢ x✝ ∈ a✝¹ ::ₘ s✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: RedLt_wf
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ WellFounded MultisetRedLt
Tactic:
constructor
Proof state after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ ∀ (a : Multiset α), Acc MultisetRedLt a
Theorem: RedLt_wf
Proof state before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
⊢ ∀ (a : Multiset α), Acc MultisetRedLt a
Tactic:
intros a
Proof state after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ Acc MultisetRedLt a
Theorem: RedLt_wf
Proof state before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ Acc MultisetRedLt a
Tactic:
apply mred_acc
Proof state after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ ∀ x ∈ a, Acc LT.lt x
Theorem: RedLt_wf
Proof state before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
⊢ ∀ x ∈ a, Acc LT.lt x
Tactic:
intros x _
Proof state after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ Acc LT.lt x
Theorem: RedLt_wf
Proof state before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ Acc LT.lt x
Tactic:
apply wf_lt.induction x
Proof state after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ ∀ (x : α), (∀ y < x, Acc LT.lt y) → Acc LT.lt x
Theorem: RedLt_wf
Proof state before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
⊢ ∀ (x : α), (∀ y < x, Acc LT.lt y) → Acc LT.lt x
Tactic:
intros y h
Proof state after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ Acc LT.lt y
Theorem: RedLt_wf
Proof state before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ Acc LT.lt y
Tactic:
apply Acc.intro y
Proof state after:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ ∀ y_1 < y, Acc LT.lt y_1
Theorem: RedLt_wf
Proof state before:
case h.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
wf_lt : WellFoundedLT α
a : Multiset α
x : α
a✝ : x ∈ a
y : α
h : ∀ y_1 < y, Acc LT.lt y_1
⊢ ∀ y_1 < y, Acc LT.lt y_1
Tactic:
assumption
Proof state after:
no goals
Theorem: Lt_wf
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded MultisetLt
Tactic:
unfold MultisetLt
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded (TC MultisetRedLt)
Theorem: Lt_wf
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded (TC MultisetRedLt)
Tactic:
apply TC.wf
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded MultisetRedLt
Theorem: Lt_wf
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
h : WellFounded MultisetRedLt
⊢ WellFounded MultisetRedLt
Tactic:
assumption
Proof state after:
no goals
Theorem: mul_geq_zero
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
⊢ ∀ (M : Multiset α), M ≥ 0
Tactic:
intro M
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
⊢ M ≥ 0
Theorem: mul_geq_zero
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
⊢ M ≥ 0
Tactic:
simp_all only [Multiset.quot_mk_to_coe'', ge_iff_le, zero_le]
Proof state after:
no goals
Theorem: mem_leq_diff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (M N : Multiset α), N ≤ M → M = M - N + N
Tactic:
intros M N h
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M - N + N
Theorem: mem_leq_diff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M - N + N
Tactic:
rw [← Multiset.union_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M ∪ N
Theorem: mem_leq_diff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M ∪ N
Tactic:
rw [Multiset.eq_union_left]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ N ≤ M
Theorem: mem_leq_diff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ N ≤ M
Tactic:
exact h
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P : Multiset α), N ≤ M → M - N + P = M + P - N
Tactic:
intro M N P h
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P = M + P - N
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P = M + P - N
Tactic:
have : M - N + P + N = M + P - N + N := by
  have : M - N + P + N = M - N + N + P := by
    have : M - N + P + N = M - N + (P + N) := by
      apply add_assoc (M - N)
    rw [this]
    have : M - N + N + P = M - N + (N + P) := by apply add_assoc (M - N)
    rw [this]
    have : P + N = N + P := by apply add_comm P N
    simp_all only [ge_iff_le]
  rw [this]
  have : M + P - N + N = M + P := by
    have : M + P - N + N = (M + P) ∪ N := by apply Eq.refl
    have : (M + P) ∪ N = M + P:= by
      apply Multiset.eq_union_left
      have : M ≤ M + P := by simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
      apply le_trans h this
    simp_all only [ge_iff_le]
  rw [this]
  have : M - N + N = M := by
    have : M = M - N + N := by
      apply mem_leq_diff
      exact h
    rw [← this]
  simp_all only [ge_iff_le]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M + P - N + N
⊢ M - N + P = M + P - N
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M + P - N + N
⊢ M - N + P = M + P - N
Tactic:
simp_all only [ge_iff_le, add_left_inj]
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P + N = M + P - N + N
Tactic:
have : M - N + P + N = M - N + N + P := by
  have : M - N + P + N = M - N + (P + N) := by
    apply add_assoc (M - N)
  rw [this]
  have : M - N + N + P = M - N + (N + P) := by apply add_assoc (M - N)
  rw [this]
  have : P + N = N + P := by apply add_comm P N
  simp_all only [ge_iff_le]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M - N + P + N = M + P - N + N
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M - N + P + N = M + P - N + N
Tactic:
rw [this]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M - N + N + P = M + P - N + N
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M - N + N + P = M + P - N + N
Tactic:
have : M + P - N + N = M + P := by
  have : M + P - N + N = (M + P) ∪ N := by apply Eq.refl
  have : (M + P) ∪ N = M + P:= by
    apply Multiset.eq_union_left
    have : M ≤ M + P := by simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
    apply le_trans h this
  simp_all only [ge_iff_le]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M - N + N + P = M + P - N + N
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M - N + N + P = M + P - N + N
Tactic:
rw [this]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M - N + N + P = M + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M - N + N + P = M + P
Tactic:
have : M - N + N = M := by
  have : M = M - N + N := by
    apply mem_leq_diff
    exact h
  rw [← this]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P
this : M - N + N = M
⊢ M - N + N + P = M + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P
this : M - N + N = M
⊢ M - N + N + P = M + P
Tactic:
simp_all only [ge_iff_le]
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P + N = M - N + N + P
Tactic:
have : M - N + P + N = M - N + (P + N) := by
  apply add_assoc (M - N)
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + (P + N)
⊢ M - N + P + N = M - N + N + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + (P + N)
⊢ M - N + P + N = M - N + N + P
Tactic:
rw [this]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + (P + N)
⊢ M - N + (P + N) = M - N + N + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + (P + N)
⊢ M - N + (P + N) = M - N + N + P
Tactic:
have : M - N + N + P = M - N + (N + P) := by apply add_assoc (M - N)
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + (P + N)
this : M - N + N + P = M - N + (N + P)
⊢ M - N + (P + N) = M - N + N + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + (P + N)
this : M - N + N + P = M - N + (N + P)
⊢ M - N + (P + N) = M - N + N + P
Tactic:
rw [this]
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + (P + N)
this : M - N + N + P = M - N + (N + P)
⊢ M - N + (P + N) = M - N + (N + P)
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + (P + N)
this : M - N + N + P = M - N + (N + P)
⊢ M - N + (P + N) = M - N + (N + P)
Tactic:
have : P + N = N + P := by apply add_comm P N
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + (P + N)
this✝ : M - N + N + P = M - N + (N + P)
this : P + N = N + P
⊢ M - N + (P + N) = M - N + (N + P)
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + (P + N)
this✝ : M - N + N + P = M - N + (N + P)
this : P + N = N + P
⊢ M - N + (P + N) = M - N + (N + P)
Tactic:
simp_all only [ge_iff_le]
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P + N = M - N + (P + N)
Tactic:
apply add_assoc (M - N)
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + (P + N)
⊢ M - N + N + P = M - N + (N + P)
Tactic:
apply add_assoc (M - N)
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + (P + N)
this : M - N + N + P = M - N + (N + P)
⊢ P + N = N + P
Tactic:
apply add_comm P N
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M + P - N + N = M + P
Tactic:
have : M + P - N + N = (M + P) ∪ N := by apply Eq.refl
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ M + P - N + N = M + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ M + P - N + N = M + P
Tactic:
have : (M + P) ∪ N = M + P:= by
  apply Multiset.eq_union_left
  have : M ≤ M + P := by simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
  apply le_trans h this
Proof state after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P ∪ N
this : M + P ∪ N = M + P
⊢ M + P - N + N = M + P
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P ∪ N
this : M + P ∪ N = M + P
⊢ M + P - N + N = M + P
Tactic:
simp_all only [ge_iff_le]
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M + P - N + N = M + P ∪ N
Tactic:
apply Eq.refl
Proof state after:
no goals
Theorem: le_sub_add
Proof state before:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ M + P ∪ N = M + P
Tactic:
apply Multiset.eq_union_left
Proof state after:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ N ≤ M + P
Theorem: le_sub_add
Proof state before:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ N ≤ M + P
Tactic:
have : M ≤ M + P := by simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
Proof state after:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P ∪ N
this : M ≤ M + P
⊢ N ≤ M + P
Theorem: le_sub_add
Proof state before:
case a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P ∪ N
this : M ≤ M + P
⊢ N ≤ M + P
Tactic:
apply le_trans h this
Proof state after:
no goals