Theorem: in_notin_diff (Pdl/MultisetOrder.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (X Y : Multiset α), x ∈ X → x ∉ Y → x ∈ X - Y
Tactic:
intros x X Y x_in_X x_notin_Y
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ x ∈ X - Y

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ x ∈ X - Y
Tactic:
have : Multiset.count x X ≥ 1 := by
  rw [← Multiset.one_le_count_iff_mem] at x_in_X
  exact x_in_X
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∈ X - Y

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∈ X - Y
Tactic:
have : Multiset.count x Y = 0 := by apply Multiset.count_eq_zero_of_not_mem; exact x_notin_Y
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ x ∈ X - Y

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ x ∈ X - Y
Tactic:
rw [← Multiset.one_le_count_iff_mem]
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x (X - Y)

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x (X - Y)
Tactic:
rw [Multiset.count_sub]
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x X - Multiset.count x Y

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ 1 ≤ Multiset.count x X - Multiset.count x Y
Tactic:
aesop
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1
Tactic:
rw [← Multiset.one_le_count_iff_mem] at x_in_X
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : 1 ≤ Multiset.count x X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : 1 ≤ Multiset.count x X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1
Tactic:
exact x_in_X
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ Multiset.count x Y = 0
Tactic:
apply Multiset.count_eq_zero_of_not_mem
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∉ Y

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∉ Y
Tactic:
exact x_notin_Y
State after:
no goals