α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ <+~ l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
refine' ⟨fun h x _ => Subperm.count_le h x, fun h => _⟩
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ <+~ List.diff l₂ l₁ ++ l₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ <+~ l₂
suffices l₁ <+~ l₂.diff l₁ ++ l₁ by
  refine' this.trans (Perm.subperm _)
  exact perm_append_comm.trans (subperm_append_diff_self_of_count_le h)
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ <+~ List.diff l₂ l₁ ++ l₁
exact (subperm_append_right l₁).mpr nil_subperm
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ List.diff l₂ l₁ ++ l₁
⊢ List.diff l₂ l₁ ++ l₁ ~ l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ List.diff l₂ l₁ ++ l₁
⊢ l₁ <+~ l₂
refine' this.trans (Perm.subperm _)
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ List.diff l₂ l₁ ++ l₁
⊢ List.diff l₂ l₁ ++ l₁ ~ l₂
exact perm_append_comm.trans (subperm_append_diff_self_of_count_le h)