-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
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 :: l₂.erase a)
⊢ count b l₁ = count b (l₂.erase a)

Tactic:
by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj'] using H

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
H : ∀ (a : α), count a [] = count a l₂
⊢ [] ~ l₂

Tactic:
match l₂ with
| nil => rfl
| cons b l₂ =>
  specialize H b
  simp at H

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₂✝ : List α
b : α
l₂ : List α
H : count b [] = count b (b :: l₂)
⊢ [] ~ b :: l₂

Tactic:
simp at H

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁ ~ l₂ ↔ ∀ (a : α), count a l₁ = count a l₂

Tactic:
refine ⟨Perm.count_eq, fun H => ?_⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
H : ∀ (a : α), count a l₁ = count a l₂
⊢ l₁ ~ l₂

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
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₂

Tactic:
have : a ∈ l₂ := count_pos_iff.mp (by rw [← H]; simp)

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
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₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
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₁)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
H : ∀ (a : α), count a [] = count a []
⊢ [] ~ []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
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₂

Tactic:
rw [← H]

Result:
α : Type u_1
inst✝ : DecidableEq α
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₁)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
H : ∀ (a : α), count a l₁ = count a l₂
⊢ l₁ ~ l₂

Tactic:
induction l₁ generalizing l₂ with
| nil =>
  match l₂ with
  | nil => rfl
  | cons b l₂ =>
    specialize H b
    simp at H
| cons a l₁ IH =>
  have : a ∈ l₂ := count_pos_iff.mp (by rw [← H]; simp)
  refine ((IH fun b => ?_).cons a).trans (perm_cons_erase this).symm
  specialize H b
  rw [(perm_cons_erase this).count_eq] at H
  by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj'] using H

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
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 (l₂.erase a)

Tactic:
rw [(perm_cons_erase this).count_eq] at H

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
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 :: l₂.erase a)
⊢ count b l₁ = count b (l₂.erase a)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
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 (l₂.erase a)

Tactic:
specialize H b

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
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 (l₂.erase a)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
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₂

Tactic:
refine ((IH fun b => ?_).cons a).trans (perm_cons_erase this).symm

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
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 (l₂.erase a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₂✝ : List α
b : α
l₂ : List α
H : ∀ (a : α), count a [] = count a (b :: l₂)
⊢ [] ~ b :: l₂

Tactic:
specialize H b

Result:
α : Type u_1
inst✝ : DecidableEq α
l₂✝ : List α
b : α
l₂ : List α
H : count b [] = count b (b :: l₂)
⊢ [] ~ b :: l₂