awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c

Tactic:
exact hs.1 c (Or.inl hc)

Premises used: And.left, Or.inl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

Tactic:
hs.2.2 b hb

Premises used: And.right
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

Tactic:
exact hs.2.2 b hb

Premises used: And.right
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
_root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))

Premises used: trans, And.right, And.left, Or.inl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))

Premises used: trans, And.right, And.left, Or.inl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
h : Chain r Cycle.nil
⊢ Eq.{u_1 + 1} (α := Cycle α) Cycle.nil Cycle.nil

Tactic:
rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
a : α
l : List α
h_1 : ∀ (h : Chain r (↑l : Cycle α)), (↑l : Cycle α) = Cycle.nil
h : Chain r (↑(a :: l) : Cycle α)
⊢ a ∈ a :: l

Tactic:
have ha : a ∈ a :: l := mem_cons_self
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
a : α
l : List α
h_1 : ∀ (h : Chain r (↑l : Cycle α)), (↑l : Cycle α) = Cycle.nil
h : Chain r (↑(a :: l) : Cycle α)
ha : a ∈ a :: l
⊢ (↑(a :: l) : Cycle α) = Cycle.nil

Tactic:
(irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

Premises used: False.elim, irrefl_of, Cycle.chain_iff_pairwise, Iff.mp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
a : α
l : List α
h_1 : ∀ (h : Chain r (↑l : Cycle α)), (↑l : Cycle α) = Cycle.nil
h : Chain r (↑(a :: l) : Cycle α)
ha : a ∈ a :: l
⊢ (↑(a :: l) : Cycle α) = Cycle.nil

Tactic:
exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

Premises used: False.elim, irrefl_of, Cycle.chain_iff_pairwise, Iff.mp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Irrefl r
h : Chain r s
nil : ∀ (h : Chain r Cycle.nil), Eq.{u_1 + 1} (α := Cycle α) Cycle.nil Cycle.nil
cons :
  ∀ (a : α) (l : List α) (h : ∀ (h : Chain r (↑l : Cycle α)), (↑l : Cycle α) = Cycle.nil)
    (h : Chain r (↑(a :: l) : Cycle α)), (↑(a :: l) : Cycle α) = Cycle.nil
⊢ s = Cycle.nil

Tactic:
induction s with
  | nil => rfl
  | cons a l h =>
    have ha : a ∈ a :: l := mem_cons_self
    exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

Premises used: Cycle.Chain.nil, List.cons
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsWellFounded α r
h : Chain r s
⊢ s = Cycle.nil

Tactic:
Chain.eq_nil_of_irrefl <| h.imp fun _ _ => Relation.TransGen.single

Premises used: Cycle.Chain.imp, Cycle.Chain.eq_nil_of_irrefl, Relation.TransGen.single
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Antisymm r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
rw : ∀ (hs : ∀ a ∈ s, ∀ b ∈ s, r a b) {a b : α} (ha : a ∈ s) (hb : b ∈ s), a = b
⊢ a = b

Tactic:
rw [chain_iff_pairwise] at hs

Premises used: Cycle.chain_iff_pairwise
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Antisymm r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
antisymm (hs a ha b hb) (hs b hb a ha)

Premises used: antisymm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
inst_1 : Std.Antisymm r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
exact antisymm (hs a ha b hb) (hs b hb a ha)

Premises used: antisymm
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List α) (dedup []) []

Tactic:
rfl

Premises used: List.dedup, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : a ∈ l.dedup
⊢ ¬∀ (b : α), b ∈ pwFilter (fun (x1 x2 : α) ↦ x1 ≠ x2) l → a ≠ b

Tactic:
simpa only [forall_mem_ne, not_not] using h

Premises used: Classical.not_not, List.forall_mem_ne
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : ¬a ∈ l.dedup
⊢ ∀ (b : α), b ∈ pwFilter (fun (x1 x2 : α) ↦ x1 ≠ x2) l → a ≠ b

Tactic:
simpa only [forall_mem_ne] using h

Premises used: List.forall_mem_ne
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
isTrue : a ∈ l.dedup → (a :: l).dedup = l.dedup
isFalse : ¬a ∈ l.dedup → (a :: l).dedup = a :: l.dedup
⊢ (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup

Tactic:
split
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : a ∈ l.dedup
⊢ (a :: l).dedup = l.dedup

Tactic:
simp [dedup_cons_of_mem', dedup_cons_of_notMem', *]

Premises used: List.dedup_cons_of_mem', List.dedup_cons_of_notMem'
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : ¬a ∈ l.dedup
⊢ (a :: l).dedup = a :: l.dedup

Tactic:
simp [dedup_cons_of_mem', dedup_cons_of_notMem', *]

Premises used: List.dedup_cons_of_mem', List.dedup_cons_of_notMem'
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
refine_2 :
  ∀ (this : (¬∀ (b : α), b ∈ pwFilter (fun (x1 x2 : α) ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b),
    a ∈ l.dedup ↔ a ∈ l
refine_1 :
  ∀ {x y z : α}, (fun (x1 x2 : α) ↦ x1 ≠ x2) x z → (fun (x1 x2 : α) ↦ x1 ≠ x2) x y ∨ (fun (x1 x2 : α) ↦ x1 ≠ x2) y z
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun (x1 x2 : α) ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
simpa only [dedup, forall_mem_ne, not_not] using this

Premises used: Classical.not_not, List.dedup, List.forall_mem_ne
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun (x1 x2 : α) ↦ x1 ≠ x2) x y ∨ (fun (x1 x2 : α) ↦ x1 ≠ x2) y z

Tactic:
not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

Premises used: mt, And.right, And.left, not_and_or, Iff.mp, Eq.trans
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun (x1 x2 : α) ↦ x1 ≠ x2) x y ∨ (fun (x1 x2 : α) ↦ x1 ≠ x2) y z

Tactic:
exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

Premises used: mt, not_and_or, Iff.mp
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ (a :: l).dedup = l.dedup

Tactic:
dedup_cons_of_mem' <| mem_dedup.2 h

Premises used: Iff.mpr, List.dedup_cons_of_mem', List.mem_dedup
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ (a :: l).dedup = a :: l.dedup

Tactic:
dedup_cons_of_notMem' <| mt mem_dedup.1 h

Premises used: mt, List.mem_dedup, List.dedup_cons_of_notMem', Iff.mp
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup

Tactic:
simpa using dedup_cons' a l

Premises used: List.dedup_cons'
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ ∀ (l : List α), l.dedup <+ l

Tactic:
pwFilter_sublist

Premises used: List.dedup, List.pwFilter_sublist
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ ∀ (l : List α), l.dedup ⊆ l

Tactic:
pwFilter_subset

Premises used: List.pwFilter_subset, List.dedup
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l ⊆ l.dedup

Tactic:
fun _ => mem_dedup.2

Premises used: Iff.mpr, List.Subset, List.mem_dedup
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ ∀ (l : List α), l.dedup.Nodup

Tactic:
pairwise_pwFilter

Premises used: List.dedup, List.pairwise_pwFilter, List.Nodup
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
pos :
  ∀ (ha : a ∈ l),
    (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
neg :
  ∀ (ha : ¬a ∈ l),
    (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
by_cases ha : a ∈ l
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
simp [ha, List.dedup_cons_of_mem]

Premises used: List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
simp [ha, List.dedup_cons_of_mem]

Premises used: List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
pos :
  ∀ (ha : a ∈ l),
    (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
neg :
  ∀ (ha : ¬a ∈ l),
    (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
by_cases ha : a ∈ l
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
simp [ha, List.dedup_cons_of_mem]

Premises used: List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Inhabited α
l_1 : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
simp [ha, List.dedup_cons_of_mem]

Premises used: List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.dedup = l ↔ l.Nodup

Tactic:
pwFilter_eq_self

Premises used: List.dedup, List.Nodup, List.pwFilter_eq_self
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
refine_1 : ∀ (h : l.dedup = a :: l'), a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
refine_2 : ∀ (h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'), l.dedup = a :: l'
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
rw : (a :: l').tail = l'
rw₁ rw₂ : l' = l'
⊢ l.dedup.tail = l'

Tactic:
rw [h, tail_cons]

Premises used: List.tail_cons
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
refine_1 : ∀ (ha : a ∈ l'), False
⊢ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
⊢ 0 < count a l'

Tactic:
have := count_pos_iff.2 ha
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this : 0 < count a l'
⊢ count a l.dedup ≤ 1

Tactic:
have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this_1 : 0 < count a l'
this : count a l.dedup ≤ 1
⊢ count a l' + 1 ≤ 1

Tactic:
rw [h, count_cons_self] at this

Premises used: List.count_cons_self
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this_1 : 0 < count a l'
this : count a l' + 1 ≤ 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup.head! :: l.dedup.tail = l.dedup

Tactic:
have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
⊢ a ∈ l.dedup

Tactic:
have hal : a ∈ l.dedup := mem_dedup.2 h.1
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup
⊢ ¬a ∈ l.dedup.tail → a = l.dedup.head!

Tactic:
rw [← this, mem_cons, or_iff_not_imp_right] at hal

Premises used: Classical.or_iff_not_imp_right, List.mem_cons
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : ¬a ∈ l.dedup.tail → a = l.dedup.head!
⊢ l.dedup = a :: l'

Tactic:
this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩

Premises used: Iff.mpr, Eq.rec, And.right, And.left, And.intro, List.cons_eq_cons, Eq.symm, rfl
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : ¬a ∈ l.dedup.tail → a = l.dedup.head!
⊢ l.dedup = a :: l'

Tactic:
exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List α) (dedup []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
Iff.rfl

Premises used: Iff.rfl, List.dedup, List.pwFilter, List.foldr
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List α) (dedup []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
pos : ∀ (h : a ∈ l), (a :: l).dedup = [] ↔ a :: l = []
neg : ∀ (h : ¬a ∈ l), (a :: l).dedup = [] ↔ a :: l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
by_cases h : a ∈ l
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]

Premises used: reduceCtorEq, List.ne_nil_of_mem, List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : ¬a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]

Premises used: List.dedup_cons_of_notMem, List.cons_ne_nil
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) (dedup []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []
cons : ∀ (a : α) (l : List α) (hl : l.dedup = [] ↔ l = []), (a :: l).dedup = [] ↔ a :: l = []
⊢ l.dedup = [] ↔ l = []

Tactic:
induction l with
  | nil => exact Iff.rfl
  | cons a l hl =>
    by_cases h : a ∈ l
    · simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]
    · simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]

Premises used: reduceCtorEq, Iff.rfl, List.cons, List.cons_ne_nil, List.nil
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ l.dedup = l

Tactic:
List.dedup_eq_self.2 h

Premises used: Iff.mpr, List.dedup_eq_self
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ l.dedup.dedup = l.dedup

Tactic:
pwFilter_idem

Premises used: List.pwFilter_idem, List.dedup
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
⊢ ([] ++ l₂).dedup = [] ∪ l₂.dedup

Tactic:
rfl
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup

Tactic:
?_
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
cons : ∀ (a : α) (l₁ : List α) (IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup), (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
⊢ (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup

Tactic:
induction l₁ with | nil => rfl | cons a l₁ IH => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
cons : (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup

Tactic:
simp only [cons_union] at *

Premises used: List.cons_union
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
cons : (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)

Tactic:
rw [← IH, cons_append]

Premises used: List.cons_append
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
pos : ∀ (h : a ∈ (l₁ ++ l₂).dedup), (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
neg : ∀ (h : ¬a ∈ (l₁ ++ l₂).dedup), (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
by_cases h : a ∈ dedup (l₁ ++ l₂)

Premises used: List.dedup, HAppend.hAppend
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
pos : (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
pos₁ pos₂ : (l₁ ++ l₂).dedup = (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
rw [dedup_cons_of_mem' h, insert_of_mem h]

Premises used: List.dedup_cons_of_mem', List.insert_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
neg : a :: (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
neg₁ neg₂ : a :: (l₁ ++ l₂).dedup = a :: (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
rw [dedup_cons_of_notMem' h, insert_of_not_mem h]

Premises used: List.dedup_cons_of_notMem', List.insert_of_not_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
⊢ (map f []).dedup = map f (dedup [])

Tactic:
simp
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
pos : ∀ (h : x ∈ xs), (f x :: map f xs).dedup = map f (x :: xs).dedup
neg : ∀ (h : ¬x ∈ xs), (f x :: map f xs).dedup = map f (x :: xs).dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
by_cases h : x ∈ xs
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
pos : (f x :: map f xs).dedup = map f xs.dedup
pos₁ : (map f xs).dedup = map f xs.dedup
pos₂ pos₃ : map f xs.dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]

Premises used: List.dedup_cons_of_mem, List.mem_map_of_mem
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
neg : (f x :: map f xs).dedup = map f (x :: xs.dedup)
neg₁ : f x :: (map f xs).dedup = map f (x :: xs.dedup)
neg₂ : f x :: map f xs.dedup = map f (x :: xs.dedup)
neg₃ neg₄ : f x :: map f xs.dedup = f x :: map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]

Premises used: Iff.mpr, List.map_cons, List.dedup_cons_of_notMem, Iff.not, List.mem_map_of_injective
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Function.Injective f
xs : List α
nil : (map f []).dedup = map f (dedup [])
cons : ∀ (x : α) (xs : List α) (ih : (map f xs).dedup = map f xs.dedup), (map f (x :: xs)).dedup = map f (x :: xs).dedup
⊢ (map f xs).dedup = map f xs.dedup

Tactic:
induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [map_cons]
    by_cases h : x ∈ xs
    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
    · rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]

Premises used: List.map_cons, List.dedup_cons_of_notMem, List.cons, List.nil
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
rw : xs ∪ ys.dedup = ys.dedup
rw₁ rw₂ : ys.dedup = ys.dedup
⊢ (xs ++ ys).dedup = ys.dedup

Tactic:
rw [List.dedup_append, Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)]

Premises used: List.Subset.union_eq_right, List.Subset.trans, List.subset_dedup, List.dedup_append
-- Module: Mathlib.Data.List.Dedup
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
h : Disjoint [] ys
⊢ [] ∪ ys = dedup [] ++ ys

Tactic:
simp
-- 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
cons : List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
⊢ x :: xs ∪ ys = (x :: xs).dedup ++ ys

Tactic:
rw [cons_union]

Premises used: List.cons_union