case nil
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
l₂ : List α
H : ∀ (a : α), count a [] = count a l₂
⊢ [] ~ l₂

case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
⊢ a :: l₁ ~ l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
H : ∀ (a : α), count a l₁ = count a l₂
⊢ l₁ ~ l₂
induction' l₁ with a l₁ IH generalizing l₂
case nil.nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂
H : ∀ (a : α), count a [] = count a []
⊢ [] ~ []

case nil.cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
b : α
l₂ : List α
H : ∀ (a : α), count a [] = count a (b :: l₂)
⊢ [] ~ b :: l₂
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
l₂ : List α
H : ∀ (a : α), count a [] = count a l₂
⊢ [] ~ l₂
cases' l₂ with b l₂
case nil.cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
b : α
l₂ : List α
H : count b [] = count b (b :: l₂)
⊢ [] ~ b :: l₂
case nil.cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
b : α
l₂ : List α
H : ∀ (a : α), count a [] = count a (b :: l₂)
⊢ [] ~ b :: l₂
specialize H b
case nil.cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
b : α
l₂ : List α
H : 0 = count b l₂ + 1
⊢ [] ~ b :: l₂
case nil.cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
b : α
l₂ : List α
H : count b [] = count b (b :: l₂)
⊢ [] ~ b :: l₂
simp at H
no goals
case nil.cons
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂✝
b : α
l₂ : List α
H : 0 = count b l₂ + 1
⊢ [] ~ b :: l₂
contradiction
no goals
case nil.nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
H✝ : ∀ (a : α), count a l₁ = count a l₂
H : ∀ (a : α), count a [] = count a []
⊢ [] ~ []
rfl
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
this : a ∈ l₂
⊢ a :: l₁ ~ l₂
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
⊢ a :: l₁ ~ l₂
have : a ∈ l₂ := count_pos.1 (by rw [← H]; simp)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
this : a ∈ l₂
b : α
⊢ count b l₁ = count b (List.erase l₂ a)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
this : a ∈ l₂
⊢ a :: l₁ ~ l₂
refine' ((IH fun b => _).cons a).trans (perm_cons_erase this).symm
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
this : a ∈ l₂
b : α
H : count b (a :: l₁) = count b l₂
⊢ count b l₁ = count b (List.erase l₂ a)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
this : a ∈ l₂
b : α
⊢ count b l₁ = count b (List.erase l₂ a)
specialize H b
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
this : a ∈ l₂
b : α
H : count b (a :: l₁) = count b (a :: List.erase l₂ a)
⊢ count b l₁ = count b (List.erase l₂ a)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
this : a ∈ l₂
b : α
H : count b (a :: l₁) = count b l₂
⊢ count b l₁ = count b (List.erase l₂ a)
rw [(perm_cons_erase this).count_eq] at H
no goals
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
this : a ∈ l₂
b : α
H : count b (a :: l₁) = count b (a :: List.erase l₂ a)
⊢ count b l₁ = count b (List.erase l₂ a)
by_cases h : b = a <;> simpa [h] using H
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
⊢ 0 < count a (a :: l₁)
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
⊢ 0 < count a l₂
rw [← H]
no goals
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : ∀ (a : α), count a l₁✝ = count a l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, (∀ (a : α), count a l₁ = count a l₂) → l₁ ~ l₂
l₂ : List α
H : ∀ (a_1 : α), count a_1 (a :: l₁) = count a_1 l₂
⊢ 0 < count a (a :: l₁)
simp