awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
simp_rw :
  map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))

Tactic:
simp_rw [map_cons, destutter_cons_cons, ← this]

Premises used: List.map_cons, List.destutter_cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
pos :
  ∀ (hr : R a b),
    map f (if R a b then a :: destutter' R b l else destutter' R a l) =
      if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
neg :
  ∀ (hr : ¬R a b),
    map f (if R a b then a :: destutter' R b l else destutter' R a l) =
      if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

Tactic:
by_cases hr : R a b
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

Tactic:
simp [hr, ← destutter_cons', map_destutter fun c hc d hd ↦ hl _ (cons_subset_cons _
        (subset_cons_self _ _) hc) _ (cons_subset_cons _ (subset_cons_self _ _) hd),
        map_destutter fun c hc d hd ↦ hl _ (subset_cons_self _ _ hc) _ (subset_cons_self _ _ hd)]

Premises used: List.cons_subset_cons, List.cons, List.destutter_cons', List.subset_cons_self
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : ¬R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

Tactic:
simp [hr, ← destutter_cons', map_destutter fun c hc d hd ↦ hl _ (cons_subset_cons _
        (subset_cons_self _ _) hc) _ (cons_subset_cons _ (subset_cons_self _ _) hd),
        map_destutter fun c hc d hd ↦ hl _ (subset_cons_self _ _ hc) _ (subset_cons_self _ _ hd)]

Premises used: List.cons_subset_cons, List.cons, List.destutter_cons', List.subset_cons_self
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
h : Injective f
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ map f (destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) l) = destutter (fun (x1 x2 : β) ↦ x1 ≠ x2) (map f l)

Tactic:
map_destutter fun _ _ _ _ ↦ h.ne_iff.symm

Premises used: Function.Injective.ne_iff, List.map_destutter, Iff.symm
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
by_cases : ∀ (hbc : R b c), (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
by_cases₁ : ∀ (hbc : ¬R b c), (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
by_cases hbc : R b c
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
⊢ ¬Rᶜ a c

Tactic:
have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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
simp_rw :
  (if R b c then b :: destutter' R c l else destutter' R b l).length ≤
    (if R a c then a :: destutter' R c l else destutter' R a l).length
simp_rw₁ : (if R b c then b :: destutter' R c l else destutter' R b l).length ≤ (a :: destutter' R c l).length
simp_rw₂ : (b :: destutter' R c l).length ≤ (a :: destutter' R c l).length
simp_rw₃ : (destutter' R c l).length + 1 ≤ (destutter' R c l).length + 1
⊢ (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]

Premises used: le_refl, Classical.not_not, List.length_cons, List.destutter', if_pos, Iff.mp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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]

Premises used: le_refl, List.length_cons, List.destutter', if_pos
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
simp : (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
simp only [destutter', if_neg hbc]

Premises used: List.destutter', if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
by_cases :
  ∀ (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
by_cases₁ :
  ∀ (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
⊢ (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
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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
simp : (destutter' R b l).length ≤ (destutter' R c l).length + 1
⊢ (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]

Premises used: List.length_cons, if_pos
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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:
Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)

Premises used: Nat.le_succ_of_le
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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)

Premises used: Nat.le_succ_of_le
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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)

Premises used: List.length_cons, if_pos, Nat.le_succ_of_le
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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
simp : (destutter' R b l).length ≤ (destutter' R a l).length
⊢ (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]

Premises used: if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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:
length_destutter'_cotrans_ge hba
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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
-- Module: Mathlib.Data.List.Destutter
Goal:
α : 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
case : (destutter' R b l).length ≤ (destutter' R a l).length
⊢ (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

Premises used: if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : ¬R b c
case : (destutter' R b l).length ≤ (if R a c then a :: destutter' R c l else destutter' R a l).length
case₁ : ∀ (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₂ case₃ :
  ∀ (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
⊢ (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

Premises used: List.length_cons, List.destutter', Nat.le_succ_of_le, if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
hab : ¬R a b
⊢ (destutter' R a l).length = (destutter' R b l).length

Tactic:
(length_destutter'_cotrans_ge hab).antisymm <| length_destutter'_cotrans_ge (symm hab : Rᶜ b a)

Premises used: List.length_destutter'_cotrans_ge, LE.le.antisymm, symm
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
pos : ∀ (hab : R a b), (destutter' R b []).length ≤ (destutter' R a [b]).length
neg : ∀ (hab : ¬R a b), (destutter' R b []).length ≤ (destutter' R a [b]).length
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

Tactic:
by_cases hab : (R a b)
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
hab : R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

Tactic:
simp_all [Nat.le_succ]

Premises used: Nat.le_succ
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
hab : ¬R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

Tactic:
simp_all [Nat.le_succ]

Premises used: Nat.le_succ
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
by_cases : ∀ (hab : R a b), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
neg : ∀ (hab : ¬R a b), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
by_cases hab : R a b
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : 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]

Premises used: Nat.le_succ, List.destutter', if_pos
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : 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]

Premises used: Nat.le_succ, List.destutter', if_pos
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
⊢ R a c ∨ Rᶜ a c

Tactic:
em _

Premises used: em
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
neg : ∀ (hac : R a c), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
neg₁ : ∀ (hac : Rᶜ a c), (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

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

Premises used: Compl.compl, em
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ ¬Rᶜ b c

Tactic:
have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : 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]

Premises used: Classical.not_not, List.destutter', if_pos, Iff.mp, if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ ¬R b c

Tactic:
have hbc : ¬R b c := trans (symm hab) hac
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
hbc : ¬R b c
neg : (destutter' R b cs).length ≤ (destutter' R a cs).length
⊢ (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]

Premises used: List.destutter', if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : 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:
(length_destutter'_congr cs hab).ge

Premises used: Eq.ge, List.length_destutter'_congr
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
inst_1 : 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

Premises used: Eq.ge, List.length_destutter'_congr
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a : α
inst_1 : IsEquiv α Rᶜ
⊢ (destutter R []).length ≤ (destutter R [a]).length

Tactic:
simp [destutter]

Premises used: List.destutter
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
a : α
inst : DecidableEq α
⊢ (destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) l).length ≤ (destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l)).length

Tactic:
length_destutter_le_length_destutter_cons

Premises used: List.length_destutter_le_length_destutter_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
h : Sublist.{u_1} (α := α) [] []
h_1 : IsChain R []
⊢ length.{u_1} (α := α) [] ≤ (destutter R []).length

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
l₁ : List α
a : α
hl : [] <+ l₁
hl₁ : IsChain R [a]
⊢ [a].length ≤ (destutter R (a :: l₁)).length

Tactic:
simp [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
pos : ∀ (hab : R a b), (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
neg : ∀ (hab : ¬R a b), (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
by_cases hab : R a b
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain 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 _)

Premises used: List.IsChain.tail, List.Sublist.cons, List.destutter_cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain 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_cons _)

Premises used: List.Sublist.cons_cons, List.destutter_cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
inst_1 : IsEquiv α Rᶜ
b : α
l₁ l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: b :: l₁)
⊢ (a :: b :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

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

Premises used: List.Sublist.cons_cons, List.IsChain.tail, List.rel_of_isChain_cons_cons, List.destutter_cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
hl : l₁ <+ l₂
hl₁ : IsChain (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁
⊢ l₁.length ≤ (destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) l₂).length

Tactic:
hl₁.length_le_length_destutter hl

Premises used: List.IsChain.length_le_length_destutter
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
h : Pairwise r []
⊢ Eq.{u_1 + 1} (α := List α) (destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) []) (dedup [])

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x : α
h : Pairwise r [x]
⊢ destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) [x] = [x].dedup

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : Pairwise r (x :: y :: xs)
⊢ (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)

Tactic:
rw [pairwise_cons] at h

Premises used: List.pairwise_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
rw : (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
⊢ destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup

Tactic:
rw [destutter_cons_cons, ← destutter_cons', ← destutter_cons', h.2.destutter_eq_dedup]

Premises used: And.right, List.destutter_cons', List.destutter_cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
inl :
  ∀ (h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)),
    (if x ≠ x then x :: (x :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup
inr :
  ∀ (hxy : x ≠ y),
    (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
obtain rfl | hxy := eq_or_ne x y

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x : α
xs : List α
h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)
⊢ (if x ≠ x then x :: (x :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup

Tactic:
simpa using h.2.destutter_eq_dedup

Premises used: And.right
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs

Tactic:
simp only [mem_cons, forall_eq_or_imp, pairwise_cons] at h

Premises used: forall_eq_or_imp, List.pairwise_cons, List.mem_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
⊢ ¬x ∈ xs

Tactic:
have : x ∉ xs := fun hx ↦ hxy (antisymm h.1.1 (h.2.1 x hx))
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ ¬x ∈ y :: xs

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
inst_1 : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
inr : x :: (y :: xs).dedup = (x :: y :: xs).dedup
inr₁ inr₂ : x :: (y :: xs).dedup = x :: (y :: xs).dedup
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun (x1 x2 : α) ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
rw [if_pos hxy, dedup_cons_of_notMem (a := x) (by simp [*])]

Premises used: List.dedup_cons_of_notMem, if_pos
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := List α) (rdrop [] n) []

Tactic:
simp [rdrop]

Premises used: List.rdrop
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
⊢ l.rdrop 0 = l

Tactic:
simp [rdrop]

Premises used: List.rdrop
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := List α) (take (length.{u_1} (α := α) [] - n) []) (reverse (drop n (reverse [])))

Tactic:
simp
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
append_singleton : take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse
append_singleton₁ :
  ∀ (n : ℕ), take ((xs ++ [x]).length - (n + 1)) (xs ++ [x]) = (drop (n + 1) (xs ++ [x]).reverse).reverse
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse

Tactic:
cases n