awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨i, hi⟩)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) ⟨j, hj⟩)
hji : j < i
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩

Tactic:
exact (h j i hj hi hji hg.symm).elim

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
⊢ l.Nodup ↔ Injective l.get

Tactic:
nodup_iff_injective_getElem

Premises used: List.nodup_iff_injective_getElem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : l.Nodup
⊢ Injective l.get

Tactic:
nodup_iff_injective_get.mp h

Premises used: Iff.mp, List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : Injective l.get
⊢ l.Nodup

Tactic:
nodup_iff_injective_get.mpr h

Premises used: Iff.mpr, List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : l.Nodup
i j : Fin l.length
⊢ l.get i = l.get j ↔ i = j

Tactic:
(nodup_iff_injective_get.1 h).eq_iff

Premises used: Function.Injective.eq_iff, Iff.mp, List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ l.get (⟨i, hi⟩ : Fin l.length) = l.get (⟨j, hj⟩ : Fin l.length) ↔ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩

Tactic:
have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
this : l.get (⟨i, hi⟩ : Fin l.length) = l.get (⟨j, hj⟩ : Fin l.length) ↔ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj ↔
    i = j

Tactic:
simpa
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
⊢ l.Nodup ↔
    ∀ (i j : ℕ),
      i < j →
        j < l.length →
          getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ≠
            getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j

Tactic:
grind [List.pairwise_iff_getElem]

Premises used: List.pairwise_iff_getElem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x : α
h : Nodup.{u} (α := α) []
⊢ [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
hl : ∀ (h : tl.Nodup), tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
⊢ tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x

Tactic:
specialize hl h.of_cons

Premises used: List.Nodup.of_cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
pos : ∀ (hx : tl = [x]), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
neg : ∀ (hx : ¬tl = [x]), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
by_cases hx : tl = [x]
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
simpa [hx, and_comm, and_or_left] using h

Premises used: and_or_left, and_comm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
hx : ¬tl = [x]
⊢ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x

Tactic:
rw [← Ne, hl] at hx

Premises used: Ne
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
hx : tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
neg :
  ∀ (h : [hd].Nodup)
    (hl : [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x),
    [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ (y : α), y ∈ [hd] ∧ y ≠ x
neg₁ : ∀ (y : α) (hy : y ∈ tl) (hx : y ≠ x), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
rcases hx with (rfl | ⟨y, hy, hx⟩)

Premises used: rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
h : [hd].Nodup
hl : [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ (y : α), y ∈ [hd] ∧ y ≠ x

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
this : ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
simpa [ne_nil_of_mem hy]

Premises used: List.ne_nil_of_mem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
neg : ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
⟨y, mem_cons_of_mem _ hy, hx⟩

Premises used: List.mem_cons_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x

Tactic:
exact ⟨y, mem_cons_of_mem _ hy, hx⟩
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : l.Nodup
x : α
nil :
  ∀ (h : Nodup.{u} (α := α) []),
    [] ≠ [x] ↔ Eq.{u + 1} (α := List α) [] [] ∨ ∃ (y : α), Membership.mem (γ := List α) [] y ∧ y ≠ x
cons :
  ∀ (hd : α) (tl : List α) (hl : ∀ (h : tl.Nodup), tl ≠ [x] ↔ tl = [] ∨ ∃ (y : α), y ∈ tl ∧ y ≠ x)
    (h : (hd :: tl).Nodup), hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ (y : α), y ∈ hd :: tl ∧ y ≠ x
⊢ l ≠ [x] ↔ l = [] ∨ ∃ (y : α), y ∈ l ∧ y ≠ x

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl =>
    specialize hl h.of_cons
    by_cases hx : tl = [x]
    · simpa [hx, and_comm, and_or_left] using h
    · rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩

Premises used: and_or_left, Ne, and_comm, List.cons, rfl, List.nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
rw : ¬Injective xs.get
⊢ ¬xs.Nodup

Tactic:
rw [nodup_iff_injective_get]

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get

Tactic:
fun hinj => hne (hinj h)

Premises used: Not
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get

Tactic:
exact fun hinj => hne (hinj h)
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ idxOf (l.get i) l = (↑i : ℕ)

Tactic:
simp [H]
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
⊢ l.Nodup ↔ ∀ (a : α), count a l ≤ 1

Tactic:
nodup_iff_sublist.trans <|
    forall_congr' fun a =>
      have : replicate 2 a <+ l ↔ 1 < count a l := replicate_sublist_iff ..
      (not_congr this).trans Nat.not_lt

Premises used: Nat.not_lt, List.nodup_iff_sublist, List.replicate_sublist_iff, forall_congr', Iff.trans, not_congr
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
inst : BEq α
inst_1 : LawfulBEq α
x : α
rw : count x l ≤ 1 ↔ 0 < count x l → count x l = 1
⊢ count x l ≤ 1 ↔ x ∈ l → count x l = 1

Tactic:
rw [← count_pos_iff]

Premises used: List.count_pos_iff
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
inst : BEq α
inst_1 : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1

Tactic:
grind
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
inst : BEq α
inst_1 : LawfulBEq α
h : ∀ (a : α), count a l = 1
a : α
⊢ 1 ≤ count a l

Tactic:
grind
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
inst : BEq α
inst_1 : LawfulBEq α
⊢ (Bijective.{1, u + 1} (β := α) fun (n : Fin l.length) ↦
      getElem (valid := fun (xs : List α) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l n ⋯) ↔
    ∀ (a : α), count a l = 1

Tactic:
get_bijective_iff

Premises used: List.get_bijective_iff
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
d : l.Nodup
h : a ∈ l
⊢ count a l = 1

Tactic:
nodup_iff_count_eq_one.mp d a h

Premises used: List.nodup_iff_count_eq_one, Iff.mp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup → l₁.Nodup

Tactic:
Nodup.sublist (sublist_append_left l₁ l₂)

Premises used: List.Nodup.sublist, List.sublist_append_left
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup → l₂.Nodup

Tactic:
Nodup.sublist (sublist_append_right l₁ l₂)

Premises used: List.Nodup.sublist, List.sublist_append_right
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂

Tactic:
simp only [Nodup, pairwise_append, disjoint_iff_ne]

Premises used: List.disjoint_iff_ne, List.pairwise_append, List.Nodup
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
d : (l₁ ++ l₂).Nodup
⊢ l₁.Disjoint l₂

Tactic:
(nodup_append'.1 d).2.2

Premises used: And.right, Iff.mp, List.nodup_append'
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
d₁ : l₁.Nodup
d₂ : l₂.Nodup
dj : l₁.Disjoint l₂
⊢ (l₁ ++ l₂).Nodup

Tactic:
nodup_append'.2 ⟨d₁, d₂, dj⟩

Premises used: Iff.mpr, And.intro, List.nodup_append'
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ (l₂ ++ l₁).Nodup

Tactic:
simp only [nodup_append', and_left_comm, disjoint_comm]

Premises used: and_left_comm, List.disjoint_comm, List.nodup_append'
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l₁ l₂ : List α
⊢ (l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup

Tactic:
simp only [nodup_append', not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
    disjoint_cons_right]

Premises used: and_left_comm, not_or, List.nodup_cons, List.mem_append, and_assoc, List.nodup_append', List.disjoint_cons_right
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
l : List α
⊢ (map f l).Nodup → l.Nodup

Tactic:
(Pairwise.of_map f) fun _ _ => mt <| congr_arg f

Premises used: List.Pairwise.of_map, mt, List.Nodup, congr_arg
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l : List α
f : α → β
H : ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y
d : l.Nodup
⊢ (map f l).Nodup

Tactic:
Pairwise.map _ (fun a b ⟨ma, mb, n⟩ e => n (H a ma b mb e)) (Pairwise.and_mem.1 d)

Premises used: List.Pairwise.and_mem, List.Nodup, List.Pairwise.map, Iff.mp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
d : (map f []).Nodup
⊢ ∀ ⦃x : α⦄, Membership.mem (γ := List α) [] x → ∀ ⦃y : α⦄, Membership.mem (γ := List α) [] y → f x = f y → x = y

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (map f (hd :: tl)).Nodup
⊢ (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup

Tactic:
simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d

Premises used: List.map, not_exists, Ne.eq_def, List.nodup_cons, List.mem_map, not_and
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
cons : ∀ ⦃x : α⦄, x = hd ∨ x ∈ tl → ∀ ⦃y : α⦄, y = hd ∨ y ∈ tl → f x = f y → x = y
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y

Tactic:
simp only [mem_cons]

Premises used: List.mem_cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y) ∧ (map f tl).Nodup
h₃ : f y = f y
⊢ y = y

Tactic:
rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x : α
d : (∀ (x_1 : α), x_1 ∈ tl → f x_1 ≠ f x) ∧ (map f tl).Nodup
y : α
h₂ : y ∈ tl
h₃ : f x = f y
⊢ x = y

Tactic:
apply (d.1 _ h₂ h₃.symm).elim

Premises used: False.elim, And.left, Eq.symm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x : α
h₁ : x ∈ tl
y : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y) ∧ (map f tl).Nodup
h₃ : f x = f y
⊢ x = y

Tactic:
apply (d.1 _ h₁ h₃).elim

Premises used: False.elim, And.left
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x : α
h₁ : x ∈ tl
y : α
h₂ : y ∈ tl
h₃ : f x = f y
⊢ x = y

Tactic:
apply ih d.2 h₁ h₂ h₃

Premises used: And.right
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
l : List α
d : (map f l).Nodup
nil :
  ∀ (d : (map f []).Nodup) ⦃x : α⦄,
    Membership.mem (γ := List α) [] x → ∀ ⦃y : α⦄, Membership.mem (γ := List α) [] y → f x = f y → x = y
cons :
  ∀ (hd : α) (tl : List α) (ih : ∀ (d : (map f tl).Nodup) ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y)
    (d : (map f (hd :: tl)).Nodup) ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y

Tactic:
induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
    simp only [mem_cons]
    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
    · rfl
    · apply (d.1 _ h₂ h₃.symm).elim
    · apply (d.1 _ h₁ h₃).elim
    · apply ih d.2 h₁ h₂ h₃

Premises used: List.map, not_exists, Ne.eq_def, List.cons, List.nodup_cons, List.mem_cons, List.mem_map, not_and, rfl, List.nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
l : List α
d : l.Nodup
⊢ (map f l).Nodup ↔ ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y

Tactic:
⟨inj_on_of_nodup_map, fun h => d.map_on h⟩

Premises used: List.Nodup.map_on, List.inj_on_of_nodup_map, Iff.intro
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l : List α
f : α → β
hf : Injective f
⊢ l.Nodup → (map f l).Nodup

Tactic:
Nodup.map_on fun _ _ _ _ h => hf h

Premises used: List.Nodup.map_on
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
f : α → β
l : List α
hf : Injective f
⊢ (map f l).Nodup ↔ l.Nodup

Tactic:
⟨Nodup.of_map _, Nodup.map hf⟩

Premises used: List.Nodup.map, Iff.intro, List.Nodup.of_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
⊢ l.attach.Nodup ↔ l.Nodup

Tactic:
⟨fun h => attach_map_subtype_val l ▸ h.map fun _ _ => Subtype.ext, fun h =>
    Nodup.of_map Subtype.val ((attach_map_subtype_val l).symm ▸ h)⟩

Premises used: Eq.rec, List.Nodup.map, Iff.intro, List.Nodup.of_map, Eq.symm, Subtype.val, List.attach_map_subtype_val, Subtype.ext
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : l.Nodup
⊢ (List.pmap (P := p) f l H).Nodup

Tactic:
grind
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
p : α → Bool
l : List α
⊢ l.Nodup → (List.filter p l).Nodup

Tactic:
simpa using Pairwise.filter p

Premises used: List.Pairwise.filter
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
⊢ Pairwise (fun (a b : α) ↦ b ≠ a) l ↔ l.Nodup

Tactic:
simp only [Nodup, Ne, eq_comm]

Premises used: Ne, eq_comm, List.Nodup
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
u : α
rw : (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup
⊢ (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
rw [← nodup_reverse]

Premises used: List.nodup_reverse
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
u : α
⊢ (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = getLast? []
⊢ Nodup.{u} (α := α) (tail (reverse [])) ↔ Nodup.{u} (α := α) (tail [])

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.reverse.tail.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
pos : ∀ (hl : l = []), (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
neg : ∀ (hl : ¬l = []), (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
by_cases hl : l = []
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.reverse.tail.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
hl : l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
simp_all
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.reverse.tail.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
hl : ¬l = []
neg :
  ∀
    (ih :
      ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
        l.dropLast.Nodup ↔ l.tail.Nodup)
    (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?) (hl : ¬l = []),
    (a :: l.dropLast).Nodup ↔ l.Nodup
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]

Premises used: List.nodup_reverse, List.tail_reverse, List.tail_cons, List.dropLast_cons_of_ne_nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
hl : ¬l = []
⊢ l.length ≠ 0

Tactic:
aesop
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?
hl : ¬l = []
⊢ a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯

Tactic:
simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h

Premises used: Nat.add_one_sub_one, List.length_cons, Nat.zero_lt_succ, Option.some.injEq, reduceDIte, List.getElem_cons, Nat.lt_add_one, List.getElem?_eq_getElem, List.getLast?_eq_getElem?
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
hl : ¬l = []
h : a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯
⊢ l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup

Tactic:
simp [List.dropLast_eq_take]

Premises used: List.dropLast_eq_take
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
hl : ¬l = []
h : a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯
neg :
  (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯ :: l.dropLast).Nodup ↔
    ([l.getLast hl] ++ l.dropLast).Nodup
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup

Tactic:
rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]

Premises used: List.nodup_append_comm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
ih :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
    l.dropLast.Nodup ↔ l.tail.Nodup
hl : ¬l = []
h : a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯
⊢ (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (l.length - 1) ⋯ :: l.dropLast).Nodup ↔
    ([l.getLast hl] ++ l.dropLast).Nodup

Tactic:
simp [List.getLast_eq_getElem]

Premises used: List.getLast_eq_getElem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?
nil :
  ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 = getLast? []),
    Nodup.{u} (α := α) (tail (reverse [])) ↔ Nodup.{u} (α := α) (tail [])
cons :
  ∀ (a : α) (l : List α)
    (ih :
      ∀ (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 = l.getLast?),
        l.reverse.tail.Nodup ↔ l.tail.Nodup)
    (h : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 = (a :: l).getLast?),
    (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
⊢ l.reverse.tail.Nodup ↔ l.tail.Nodup

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    · simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]

Premises used: Nat.add_one_sub_one, List.nodup_reverse, List.length_cons, Nat.zero_lt_succ, List.tail_reverse, Option.some.injEq, reduceDIte, List.nodup_append_comm, List.getElem_cons, Nat.lt_add_one, List.tail_cons, List.cons, List.getElem?_eq_getElem, List.getLast?_eq_getElem?, List.getLast_eq_getElem, List.nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
hl : Nodup.{u} (α := α) []
i : ℕ
h : i < length.{u} (α := α) []
⊢ List.erase [] (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i h) = List.eraseIdx [] i

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
IH :
  ∀ (hl : l.Nodup) (i : ℕ) (h : i < l.length),
    l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i
hl : (a :: l).Nodup
h : 0 < (a :: l).length
⊢ (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 h) = (a :: l).eraseIdx 0

Tactic:
simp