-- Mathlib/Data/List/Dedup.lean
theorem dedup_eq_cons (l : List α) (a : α) (l' : List α) :
    l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self _ _), fun ha => ?_, by rw [h, tail_cons]⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
⊢ False

Tactic:
have := count_pos_iff.2 ha

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this : 0 < count a l'
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'

Tactic:
have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
⊢ l.dedup = a :: l'

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l' + 1 ≤ 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l.dedup.tail = l'

Tactic:
rw [h, tail_cons]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
⊢ l.dedup = a :: l'

Tactic:
have hal : a ∈ l.dedup := mem_dedup.2 h.1

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup
⊢ l.dedup = a :: l'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'

case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this : 0 < count a l'
⊢ False

Tactic:
have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l.dedup ≤ 1
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∉ l.dedup.tail → a = l.dedup.head!
⊢ l.dedup = a :: l'

Tactic:
exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup
⊢ l.dedup = a :: l'

Tactic:
rw [← this, mem_cons, or_iff_not_imp_right] at hal

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∉ l.dedup.tail → a = l.dedup.head!
⊢ l.dedup = a :: l'

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l.dedup ≤ 1
⊢ False

Tactic:
rw [h, count_cons_self] at this

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l' + 1 ≤ 1
⊢ False