Theorem: double_split (Pdl/MultisetOrder.lean)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P Q : Multiset α), M + N = P + Q → N = N ∩ Q + (P - M)
Tactic:
intros M N P Q h
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N = N ∩ Q + (P - M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N = N ∩ Q + (P - M)
Tactic:
ext x
State after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q + (P - M))

State before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q + (P - M))
Tactic:
rw [Multiset.count_add]
State after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q) + Multiset.count x (P - M)

State before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q) + Multiset.count x (P - M)
Tactic:
rw [Multiset.count_inter]
State after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + Multiset.count x (P - M)

State before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + Multiset.count x (P - M)
Tactic:
rw [Multiset.count_sub]
State after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)

State before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q := by
  rw [Multiset.ext] at h
  simp_all only [Multiset.mem_add, Multiset.count_add]
State after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Tactic:
rw [Multiset.ext] at h
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), Multiset.count a (M + N) = Multiset.count a (P + Q)
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), Multiset.count a (M + N) = Multiset.count a (P + Q)
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Tactic:
simp_all only [Multiset.mem_add, Multiset.count_add]
State after:
no goals

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have : Multiset.count x N ≥ Multiset.count x Q := by linarith
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x N ≥ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x N ≥ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
simp_all only [ge_iff_le, min_eq_right]
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x N = Multiset.count x Q + (Multiset.count x P - Multiset.count x M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x N = Multiset.count x Q + (Multiset.count x P - Multiset.count x M)
Tactic:
apply le_eq_sub (Multiset.count x M) (Multiset.count x N) (Multiset.count x P) (Multiset.count x Q)
State after:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M ≤ Multiset.count x P

case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
⊢ Multiset.count x N ≥ Multiset.count x Q
Tactic:
linarith
State after:
no goals

State before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M ≤ Multiset.count x P
Tactic:
simp_all
State after:
no goals

State before:
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
Tactic:
exact H0
State after:
no goals

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : ¬Multiset.count x M ≤ Multiset.count x P
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
simp_all only [not_le, gt_iff_lt]
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have : Multiset.count x N ≤ Multiset.count x Q := by linarith
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this : Multiset.count x N ≤ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this : Multiset.count x N ≤ Multiset.count x Q
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
have:= le_of_lt l_u
State after:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this✝ : Multiset.count x N ≤ Multiset.count x Q
this : Multiset.count x P ≤ Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
this✝ : Multiset.count x N ≤ Multiset.count x Q
this : Multiset.count x P ≤ Multiset.count x M
⊢ Multiset.count x N = min (Multiset.count x N) (Multiset.count x Q) + (Multiset.count x P - Multiset.count x M)
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x P < Multiset.count x M
⊢ Multiset.count x N ≤ Multiset.count x Q
Tactic:
linarith
State after:
no goals