-- Mathlib/Data/List/Destutter.lean
theorem le_length_destutter'_cons [IsEquiv α Rᶜ] :
    ∀ {l : List α}, (l.destutter' R b).length ≤ ((b :: l).destutter' R a).length
  | [] => by by_cases hab : (R a b) <;> simp_all [Nat.le_succ]
  | c :: cs => by
    by_cases hab : R a b
    case pos => simp [destutter', if_pos hab, Nat.le_succ]
    obtain hac | hac : R a c ∨ Rᶜ a c := em _
    · have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
      simp [destutter', if_pos hac, if_pos (not_not.1 hbc), if_neg hab]
    · have hbc : ¬R b c := trans (symm hab) hac
      simp only [destutter', if_neg hbc, if_neg hac, if_neg hab]
      exact (length_destutter'_congr cs hab).ge

Proof state:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
have hbc : ¬R b c := trans (symm hab) hac

Result:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Proof state:
case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
obtain hac | hac : R a c ∨ Rᶜ a c := em _

Result:
case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Proof state:
case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
hbc : ¬Rᶜ b c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
simp [destutter', if_pos hac, if_pos (not_not.1 hbc), if_neg hab]

Result:
no goals

Proof state:
case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)

Result:
case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
hbc : ¬Rᶜ b c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
simp [destutter', if_pos hab, Nat.le_succ]

Result:
no goals

Proof state:
case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
case pos => simp [destutter', if_pos hab, Nat.le_succ]

Result:
case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

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

Tactic:
by_cases hab : (R a b) <;> simp_all [Nat.le_succ]

Result:
no goals

Proof state:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
simp only [destutter', if_neg hbc, if_neg hac, if_neg hab]

Result:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
⊢ (destutter' R b cs).length ≤ (destutter' R a cs).length

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
by_cases hab : R a b

Result:
case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Proof state:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
⊢ (destutter' R b cs).length ≤ (destutter' R a cs).length

Tactic:
exact (length_destutter'_congr cs hab).ge

Result:
no goals