awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ ¬x ∈ ys ∧ xs.Disjoint ys

Tactic:
rw [disjoint_cons_left] at h

Premises used: List.disjoint_cons_left
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
pos : ∀ (hx : x ∈ xs), List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
neg : ∀ (hx : ¬x ∈ xs), List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
by_cases hx : x ∈ xs
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
pos : List.insert x (xs ∪ ys) = xs.dedup ++ ys
pos₁ : xs ∪ ys = xs.dedup ++ ys
pos₂ pos₃ : xs.dedup ++ ys = xs.dedup ++ ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]

Premises used: List.insert_of_mem, List.mem_union_left, And.right, List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
neg : ¬x ∈ xs ∪ ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]

Premises used: List.dedup_cons_of_notMem, And.right, List.cons_append, List.insert_of_not_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
neg : ¬x ∈ xs ∧ ¬x ∈ ys
⊢ ¬x ∈ xs ∪ ys

Tactic:
rw [mem_union_iff, not_or]

Premises used: List.mem_union_iff, not_or
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∧ ¬x ∈ ys

Tactic:
⟨hx, h.1⟩

Premises used: And.left, And.intro
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ ¬x ∈ xs ∧ ¬x ∈ ys

Tactic:
exact ⟨hx, h.1⟩
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
nil : ∀ (h : Disjoint [] ys), [] ∪ ys = dedup [] ++ ys
cons :
  ∀ (x : α) (xs : List α) (ih : ∀ (h : xs.Disjoint ys), xs ∪ ys = xs.dedup ++ ys) (h : (x :: xs).Disjoint ys),
    x :: xs ∪ ys = (x :: xs).dedup ++ ys
⊢ xs ∪ ys = xs.dedup ++ ys

Tactic:
induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union]
    rw [disjoint_cons_left] at h
    by_cases hx : x ∈ xs
    · rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
    · rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩

Premises used: List.mem_union_iff, List.cons_union, not_or, List.cons, List.cons_append, List.disjoint_cons_left, List.insert_of_not_mem, List.nil
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
rw : xs.Disjoint ys.dedup
⊢ (xs ++ ys).dedup = xs.dedup ++ ys.dedup

Tactic:
rw [List.dedup_append, Disjoint.union_eq]

Premises used: List.dedup_append, List.Disjoint.union_eq
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
hy : a ∈ ys.dedup
⊢ False

Tactic:
h hx (mem_dedup.mp hy)

Premises used: List.mem_dedup, Iff.mp
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
hy : a ∈ ys.dedup
⊢ False

Tactic:
exact h hx (mem_dedup.mp hy)

Premises used: List.mem_dedup, Iff.mp
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
x : α
n : ℕ
h : n + 2 ≠ 0
rw : (x :: replicate (n + 1) x).dedup = [x]
rw₁ : (replicate n.succ x).dedup = [x]
rw₂ rw₃ : [x] = [x]
⊢ (replicate (n + 2) x).dedup = [x]

Tactic:
rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]

Premises used: Iff.mpr, List.replicate_succ, Nat.succ_ne_zero, And.intro, List.mem_replicate, List.dedup_cons_of_mem, rfl
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
simp_rw : Eq (α := ℕ) (if a ∈ l.dedup then 1 else 0) (if a ∈ l then 1 else 0)
⊢ count a l.dedup = if a ∈ l then 1 else 0

Tactic:
simp_rw [List.Nodup.count <| nodup_dedup l, mem_dedup]

Premises used: List.Nodup.count, List.nodup_dedup, List.mem_dedup
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
simp [h, nodup_dedup, p.subset h]

Premises used: List.nodup_dedup, List.Perm.subset
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : ¬a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
simp [h, count_eq_zero_of_not_mem, mt p.mem_iff.2]

Premises used: Iff.mpr, mt, List.count_eq_zero_of_not_mem, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
inst : Inhabited α
⊢ Eq.{u_1 + 1} (α := α) (headI []) default

Tactic:
rfl

Premises used: List.headI, rfl
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
inst : Inhabited α
h : α
t : List α
⊢ (h :: t).headI = h

Tactic:
rfl

Premises used: List.headI, rfl
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (ts.length + (is.length + 1), ts.length)
    (ts.length + 1 + is.length, ts.length + 1)

Tactic:
omega
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
t : α
ts is : List α
simp_wf :
  Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (is.length, is.length)
    (ts.length + 1 + is.length, ts.length + 1)
⊢ Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (is.length + length.{u_1} (α := α) [], is.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
simp_wf
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (is.length, is.length)
    (ts.length + 1 + is.length, ts.length + 1)

Tactic:
omega
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
zero : ∀ (a : α) (l : List α), iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0
succ :
  ∀ (n : ℕ),
    (∀ (a : α) (l : List α), iterateTR.loop f a n l = l.reverse ++ iterate f a n) →
      ∀ (a : α) (l : List α), iterateTR.loop f a (n + 1) l = l.reverse ++ iterate f a (n + 1)
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n

Tactic:
induction n generalizing a l
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
f : α → α
a : α
l : List α
⊢ iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_1
f : α → α
n : ℕ
h : ∀ (a : α) (l : List α), iterateTR.loop f a n l = l.reverse ++ iterate f a n
a : α
l : List α
⊢ iterateTR.loop f a (n + 1) l = l.reverse ++ iterate f a (n + 1)

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Defs
Goal:
h : ∀ (α : Type u_7) (f : α → α) (a : α) (n : ℕ), iterate f a n = iterateTR f a n
⊢ @iterate = @iterateTR

Tactic:
funext α f a n
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_7
f : α → α
a : α
n : ℕ
⊢ iterate f a n = iterateTR f a n

Tactic:
Eq.symm <| iterateTR_loop_eq f a n []

Premises used: List.iterateTR_loop_eq, Eq.symm, List.nil
-- Module: Mathlib.Data.List.Defs
Goal:
α : Type u_7
f : α → α
a : α
n : ℕ
⊢ iterate f a n = iterateTR f a n

Tactic:
exact Eq.symm <| iterateTR_loop_eq f a n []

Premises used: List.iterateTR_loop_eq, Eq.symm, List.nil
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ destutter' R a [] = [a]

Tactic:
rfl

Premises used: List.destutter', rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
⊢ destutter' R a (b :: l) = if R a b then a :: destutter' R b l else destutter' R a l

Tactic:
rfl

Premises used: List.destutter', rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
h : R b a
rw : (if R b a then b :: destutter' R a l else destutter' R b l) = b :: destutter' R a l
rw₁ rw₂ : b :: destutter' R a l = b :: destutter' R a l
⊢ destutter' R b (a :: l) = b :: destutter' R a l

Tactic:
rw [destutter', if_pos h]

Premises used: List.destutter', if_pos
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
h : ¬R b a
rw : (if R b a then b :: destutter' R a l else destutter' R b l) = destutter' R b l
rw₁ rw₂ : destutter' R b l = destutter' R b l
⊢ destutter' R b (a :: l) = destutter' R b l

Tactic:
rw [destutter', if_neg h]

Premises used: List.destutter', if_neg
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
pos : ∀ (h : R a b), destutter' R a [b] = [a, b]
neg : ∀ (h : ¬R a b), destutter' R a [b] = [a]
⊢ destutter' R a [b] = if R a b then [a, b] else [a]

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
h : R a b
⊢ destutter' R a [b] = [a, b]

Tactic:
simp! [h]
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
h : ¬R a b
⊢ destutter' R a [b] = [a]

Tactic:
simp! [h]
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ destutter' R a [] <+ [a]

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
pos : R a b → a :: destutter' R b l <+ a :: b :: l
neg : ¬R a b → destutter' R a l <+ a :: b :: l
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l

Tactic:
split_ifs
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

Tactic:
Sublist.cons_cons a (hl b)

Premises used: List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

Tactic:
exact Sublist.cons_cons a (hl b)

Premises used: List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Tactic:
(hl a).trans ((l.sublist_cons_self b).cons_cons a)

Premises used: List.Sublist.cons_cons, List.Sublist.trans, List.sublist_cons_self
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Tactic:
exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)

Premises used: List.Sublist.cons_cons, List.Sublist.trans, List.sublist_cons_self
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
nil : ∀ (a : α), destutter' R a [] <+ [a]
cons :
  ∀ (b : α) (l : List α) (hl : ∀ (a : α), destutter' R a l <+ a :: l) (a : α), destutter' R a (b :: l) <+ a :: b :: l
⊢ destutter' R a l <+ a :: l

Tactic:
induction l generalizing a with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · exact Sublist.cons_cons a (hl b)
    · exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)

Premises used: List.destutter', List.cons, List.nil
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ a ∈ destutter' R a []

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
pos : R a b → a ∈ a :: destutter' R b l
neg : ¬R a b → a ∈ destutter' R a l
⊢ a ∈ if R a b then a :: destutter' R b l else destutter' R a l

Tactic:
split_ifs
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h : R a b
⊢ a ∈ a :: destutter' R b l

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l_1 : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h : ¬R a b
⊢ a ∈ destutter' R a l

Tactic:
assumption
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
nil : a ∈ destutter' R a []
cons : ∀ (b : α) (l : List α) (hl : a ∈ destutter' R a l), a ∈ destutter' R a (b :: l)
⊢ a ∈ destutter' R a l

Tactic:
induction l with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · simp
    · assumption

Premises used: List.destutter', List.cons, List.nil
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ IsChain R (destutter' R a [])

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
x a : α
⊢ IsChain R (destutter' R a [x])

Tactic:
simp [apply_ite]

Premises used: apply_ite
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
IH2 : ∀ (y a : α), IsChain R (destutter' R a (y :: l))
a : α
⊢ ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)

Tactic:
simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2

Premises used: apply_ite, List.IsChain, if_true_right, List.destutter'_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
cons_cons :
  (((R a b → R b c → R a b) ∧ (R a b → R b c → IsChain R (b :: destutter' R c l))) ∧
      (R a b → ¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))
⊢ IsChain R (destutter' R a (b :: c :: l))

Tactic:
simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]

Premises used: imp_and, apply_ite, List.IsChain, List.cons, List.isChain_cons_cons, ite_prop_iff_and, if_true_right, List.destutter'_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ (((R a b → R b c → R a b) ∧ (R a b → R b c → IsChain R (b :: destutter' R c l))) ∧
      (R a b → ¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))

Tactic:
⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩

Premises used: Function.swap, id, And.intro
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ (((R a b → R b c → R a b) ∧ (R a b → R b c → IsChain R (b :: destutter' R c l))) ∧
      (R a b → ¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))

Tactic:
exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
a : α
nil : ∀ (a : α), IsChain R (destutter' R a [])
singleton : ∀ (x a : α), IsChain R (destutter' R a [x])
cons_cons :
  ∀ (b c : α) (l : List α) (IH : ∀ (a : α), IsChain R (destutter' R a l))
    (IH2 : ∀ (y a : α), IsChain R (destutter' R a (y :: l))) (a : α), IsChain R (destutter' R a (b :: c :: l))
⊢ IsChain R (destutter' R a l)

Tactic:
induction l using twoStepInduction generalizing a with
  | nil => simp
  | singleton => simp [apply_ite]
  | cons_cons b c l IH IH2 =>
    simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
    simp_rw [destutter'_cons, apply_ite (IsChain R ·),
      apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
      if_true_right, ite_prop_iff_and, imp_and]
    exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩

Premises used: imp_and, apply_ite, List.IsChain, List.cons, List.isChain_cons_cons, ite_prop_iff_and, if_true_right, Singleton.singleton, List.destutter'_cons, List.nil
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
a b : α
hab : R a b
⊢ IsChain R (a :: destutter' R b l)

Tactic:
simpa [destutter'_cons, hab] using isChain_destutter' R (b :: l) a

Premises used: List.isChain_destutter', List.cons, List.destutter'_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a : α
h : IsChain R [a]
⊢ destutter' R a [] = [a]

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
⊢ R a b

Tactic:
obtain ⟨h, hc⟩ := isChain_cons_cons.mp h

Premises used: List.isChain_cons_cons, Iff.mp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
h₁ : R a b
⊢ IsChain R (b :: l)

Tactic:
obtain ⟨h, hc⟩ := isChain_cons_cons.mp h

Premises used: List.isChain_cons_cons, Iff.mp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
b : α
l : List α
hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l
a : α
h_1 : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
cons : a :: destutter' R b l = a :: b :: l
cons₁ cons₂ : a :: b :: l = a :: b :: l
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
rw [l.destutter'_cons_pos h, hb hc]

Premises used: List.destutter'_cons_pos
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : IsChain R (a :: l)
nil : ∀ {a : α} (h : IsChain R [a]), destutter' R a [] = [a]
cons :
  ∀ (b : α) (l : List α) (hb : ∀ {a : α} (h : IsChain R (a :: l)), destutter' R a l = a :: l) {a : α}
    (h : IsChain R (a :: b :: l)), destutter' R a (b :: l) = a :: b :: l
⊢ destutter' R a l = a :: l

Tactic:
induction l generalizing a with
  | nil => simp
  | cons b l hb =>
    obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
    rw [l.destutter'_cons_pos h, hb hc]

Premises used: List.cons, List.isChain_cons_cons, List.destutter'_cons_pos, Iff.mp, List.nil
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : destutter' R a l = a :: l
this : IsChain R (a :: l)
⊢ IsChain R (a :: l)

Tactic:
assumption
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : destutter' R a l = a :: l
rw : IsChain R (destutter' R a l)
⊢ IsChain R (a :: l)

Tactic:
rw [← h]
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (destutter' R a l)

Tactic:
l.isChain_destutter' R a

Premises used: List.isChain_destutter'
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (destutter' R a l)

Tactic:
exact l.isChain_destutter' R a

Premises used: List.isChain_destutter'
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ destutter' R a l ≠ []

Tactic:
ne_nil_of_mem <| l.mem_destutter' R a

Premises used: List.mem_destutter', List.ne_nil_of_mem
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
⊢ destutter R [] = []

Tactic:
rfl

Premises used: List.destutter, rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ destutter R (a :: l) = destutter' R a l

Tactic:
rfl

Premises used: List.destutter, rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
a b : α
⊢ destutter R (a :: b :: l) = if R a b then a :: destutter' R b l else destutter' R a l

Tactic:
rfl

Premises used: List.destutter, List.destutter', rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a : α
⊢ destutter R [a] = [a]

Tactic:
rfl

Premises used: List.destutter, List.destutter', rfl
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
a b : α
⊢ destutter R [a, b] = if R a b then [a, b] else [a]

Tactic:
destutter_cons_cons _ R

Premises used: List.destutter', List.destutter_cons_cons
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
⊢ destutter R [] = [] ↔ IsChain R []

Tactic:
simp
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
l : List α
R : α → α → Prop
inst : DecidableRel R
⊢ destutter R (destutter R l) = destutter R l

Tactic:
destutter_of_isChain R _ <| l.isChain_destutter R

Premises used: List.isChain_destutter, List.destutter_of_isChain
-- Module: Mathlib.Data.List.Destutter
Goal:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst : DecidableRel R
R₂ : β → β → Prop
inst_1 : DecidableRel R₂
f : α → β
hl :
  ∀ (a : α), Membership.mem (γ := List α) [] a → ∀ (b : α), Membership.mem (γ := List α) [] b → (R a b ↔ R₂ (f a) (f b))
⊢ map f (destutter R []) = destutter R₂ (map f [])

Tactic:
simp
-- 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 : α
hl : ∀ (a_1 : α), a_1 ∈ [a] → ∀ (b : α), b ∈ [a] → (R a_1 b ↔ R₂ (f a_1) (f b))
⊢ map f (destutter R [a]) = destutter R₂ (map f [a])

Tactic:
simp
-- 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))
⊢ a ∈ a :: b :: l

Tactic:
simp
-- 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))
⊢ b ∈ a :: b :: l

Tactic:
simp
-- 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))
⊢ R a b ↔ R₂ (f a) (f b)

Tactic:
have := hl a (by simp) b (by simp)