-- Mathlib/Data/List/Destutter.lean
/-- `destutter` of relations like `≠`, whose negation is an equivalence relation,
gives a list of maximal length over any chain.

In other words, `l.destutter R` is an `R`-chain sublist of `l`, and is at least as long as any other
`R`-chain sublist. -/
lemma Chain'.length_le_length_destutter [IsEquiv α Rᶜ] :
    ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → l₁.Chain' R → l₁.length ≤ (l₂.destutter R).length
  -- `l₁ := []`, `l₂ := []`
  | [], [], _, _ => by simp
  -- `l₁ := l₁`, `l₂ := a :: l₂`
  | l₁, _, .cons (l₂ := l₂) a hl, hl₁ =>
    (hl₁.length_le_length_destutter hl).trans length_destutter_le_length_destutter_cons
  -- `l₁ := [a]`, `l₂ := a :: l₂`
  | _, _, .cons₂ (l₁ := []) (l₂ := l₁) a hl, hl₁ => by simp [Nat.one_le_iff_ne_zero]
  -- `l₁ := a :: l₁`, `l₂ := a :: b :: l₂`
  | _, _, .cons₂ a <| .cons (l₁ := l₁) (l₂ := l₂) b hl, hl₁ => by
    by_cases hab : R a b
    · simpa [destutter_cons_cons, hab] using hl₁.tail.length_le_length_destutter (hl.cons _)
    · simpa [destutter_cons_cons, hab] using hl₁.length_le_length_destutter (hl.cons₂ _)
  -- `l₁ := a :: b :: l₁`, `l₂ := a :: b :: l₂`
  | _, _, .cons₂ a <| .cons₂ (l₁ := l₁) (l₂ := l₂) b hl, hl₁ => by
    simpa [destutter_cons_cons, rel_of_chain_cons hl₁]
      using hl₁.tail.length_le_length_destutter (hl.cons₂ _)

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : Chain' R (a :: l₁)
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
by_cases hab : R a b

Result:
case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : Chain' R (a :: l₁)
hab : R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : Chain' R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Proof state:
case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : Chain' R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
simpa [destutter_cons_cons, hab] using hl₁.length_le_length_destutter (hl.cons₂ _)

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
b : α
l₁ l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : Chain' R (a :: b :: l₁)
⊢ (a :: b :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
simpa [destutter_cons_cons, rel_of_chain_cons hl₁]
  using hl₁.tail.length_le_length_destutter (hl.cons₂ _)

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
x✝¹ : [] <+ []
x✝ : Chain' R []
⊢ [].length ≤ (destutter R []).length

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : Chain' R (a :: l₁)
hab : R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
simpa [destutter_cons_cons, hab] using hl₁.tail.length_le_length_destutter (hl.cons _)

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
a : α
hl : [] <+ l₁
hl₁ : Chain' R [a]
⊢ [a].length ≤ (destutter R (a :: l₁)).length

Tactic:
simp [Nat.one_le_iff_ne_zero]

Result:
no goals