-- Mathlib/Data/List/Destutter.lean
theorem length_destutter'_cotrans_ge [i : IsTrans α Rᶜ] :
    ∀ {a} {l : List α}, ¬R b a → (l.destutter' R b).length ≤ (l.destutter' R a).length
  | a, [], hba => by simp
  | a, c :: l, hba => by
    by_cases hbc : R b c
    case pos =>
      have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)
      simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
    case neg =>
      simp only [destutter', if_neg hbc]
      by_cases hac : R a c
      case pos =>
        simp only [if_pos hac, length_cons]
        exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
      case neg =>
        simp only [if_neg hac]
        exact length_destutter'_cotrans_ge hba

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
by_cases hbc : R b c

Result:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
simp only [destutter', if_neg hbc]

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

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

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Proof state:
case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
case neg =>
  simp only [if_neg hac]
  exact length_destutter'_cotrans_ge hba

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]

Result:
no goals

Proof state:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
case pos =>
  have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)
  simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]

Result:
case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
simp only [if_neg hac]

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (destutter' R a l).length

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (destutter' R a l).length

Tactic:
exact length_destutter'_cotrans_ge hba

Result:
no goals

Proof state:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
case pos =>
  simp only [if_pos hac, length_cons]
  exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)

Result:
case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Proof state:
case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
case neg =>
  simp only [destutter', if_neg hbc]
  by_cases hac : R a c
  case pos =>
    simp only [if_pos hac, length_cons]
    exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
  case neg =>
    simp only [if_neg hac]
    exact length_destutter'_cotrans_ge hba

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
simp only [if_pos hac, length_cons]

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (destutter' R c l).length + 1

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (destutter' R c l).length + 1

Tactic:
exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
by_cases hac : R a c

Result:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length

case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
hac : ¬R a c
⊢ (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length