-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_append_diff_self_of_count_le {l₁ l₂ : List α}
    (h : ∀ x ∈ l₁, count x l₁ ≤ count x l₂) : l₁ ++ l₂.diff l₁ ~ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
⊢ 0 < count hd l₂

Tactic:
exact Nat.lt_of_lt_of_le (count_pos_iff.mpr (.head _)) (h hd (.head _))

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
⊢ tl ++ (l₂.erase hd).diff tl ~ l₂.erase hd

Tactic:
refine IH fun x hx => ?_

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx : x ∈ tl
⊢ count x tl ≤ count x (l₂.erase hd)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ l₂

Tactic:
have : hd ∈ l₂ := by
  rw [← count_pos_iff]
  exact Nat.lt_of_lt_of_le (count_pos_iff.mpr (.head _)) (h hd (.head _))

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this : hd ∈ l₂
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ l₂

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx : x ∈ tl
h : count x (hd :: tl) ≤ count x (hd :: l₂.erase hd)
⊢ count x tl ≤ count x (l₂.erase hd)

Tactic:
if hx : x = hd then subst hd; simpa [Nat.succ_le_succ_iff] using h
else simpa [hx] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
x : α
hx : x ∈ tl
this✝ : x ∈ l₂
this : l₂ ~ x :: l₂.erase x
h : count x (x :: tl) ≤ count x (x :: l₂.erase x)
⊢ count x tl ≤ count x (l₂.erase x)

Tactic:
simpa [Nat.succ_le_succ_iff] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx✝ : x ∈ tl
h : count x (hd :: tl) ≤ count x (hd :: l₂.erase hd)
hx : ¬x = hd
⊢ count x tl ≤ count x (l₂.erase hd)

Tactic:
simpa [hx] using h

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ l₂

Tactic:
refine Perm.trans ?_ this.symm

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ hd :: l₂.erase hd

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ ++ l₂.diff l₁ ~ l₂

Tactic:
induction l₁ generalizing l₂ with
| nil => simp
| cons hd tl IH =>
  have : hd ∈ l₂ := by
    rw [← count_pos_iff]
    exact Nat.lt_of_lt_of_le (count_pos_iff.mpr (.head _)) (h hd (.head _))
  have := perm_cons_erase this
  refine Perm.trans ?_ this.symm
  rw [cons_append, diff_cons, perm_cons]
  refine IH fun x hx => ?_
  specialize h x (.tail _ hx)
  rw [perm_iff_count.mp this] at h
  if hx : x = hd then subst hd; simpa [Nat.succ_le_succ_iff] using h
  else simpa [hx] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx✝ : x ∈ tl
h : count x (hd :: tl) ≤ count x (hd :: l₂.erase hd)
hx : x = hd
⊢ count x tl ≤ count x (l₂.erase hd)

Tactic:
subst hd

Result:
α : Type u_1
inst✝ : DecidableEq α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
x : α
hx : x ∈ tl
this✝ : x ∈ l₂
this : l₂ ~ x :: l₂.erase x
h : count x (x :: tl) ≤ count x (x :: l₂.erase x)
⊢ count x tl ≤ count x (l₂.erase x)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ hd :: l₂.erase hd

Tactic:
rw [cons_append, diff_cons, perm_cons]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
⊢ tl ++ (l₂.erase hd).diff tl ~ l₂.erase hd

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx : x ∈ tl
h : count x (hd :: tl) ≤ count x l₂
⊢ count x tl ≤ count x (l₂.erase hd)

Tactic:
rw [perm_iff_count.mp this] at h

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx : x ∈ tl
h : count x (hd :: tl) ≤ count x (hd :: l₂.erase hd)
⊢ count x tl ≤ count x (l₂.erase hd)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx : x ∈ tl
⊢ count x tl ≤ count x (l₂.erase hd)

Tactic:
specialize h x (.tail _ hx)

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
x : α
hx : x ∈ tl
h : count x (hd :: tl) ≤ count x l₂
⊢ count x tl ≤ count x (l₂.erase hd)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this : hd ∈ l₂
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ l₂

Tactic:
have := perm_cons_erase this

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
this✝ : hd ∈ l₂
this : l₂ ~ hd :: l₂.erase hd
⊢ hd :: tl ++ l₂.diff (hd :: tl) ~ l₂