Theorem: le_sub_add (Pdl/MultisetOrder.lean)

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
State after:
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P = M + P - N

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]
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

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]
State after:
no goals

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]
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

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]
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

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]
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

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]
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

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]
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

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]
State after:
no goals

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)
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

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]
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

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)
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

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]
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)

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
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)

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]
State after:
no goals

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)
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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 ≤ M + P
Tactic:
simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
State after:
no goals

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 = M
Tactic:
have : M = M - N + N := by
  apply mem_leq_diff
  exact h
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 = M - N + N
⊢ M - N + N = M

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 = M - N + N
⊢ M - N + N = M
Tactic:
rw [← this]
State after:
no goals

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 = M - N + N
Tactic:
apply mem_leq_diff
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 ≤ M

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 ≤ M
Tactic:
exact h
State after:
no goals