awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : ℕ
h : i + 1 < (a :: l).length
⊢ (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (i + 1) h) =
    (a :: l).eraseIdx (i + 1)

Tactic:
grind
-- 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
i : ℕ
h : i < (a :: l).length
cons :
  ∀ (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
cons₁ :
  ∀ (i : ℕ) (h : i + 1 < (a :: l).length),
    (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (i + 1) h) =
      (a :: l).eraseIdx (i + 1)
⊢ (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) i h) = (a :: l).eraseIdx i

Tactic:
cases i with
    | zero => simp
    | succ i => grind
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l.Nodup
i : ℕ
h : i < l.length
nil :
  ∀ (hl : Nodup.{u} (α := α) []) (i : ℕ) (h : i < length.{u} (α := α) []),
    List.erase [] (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i h) = List.eraseIdx [] i
cons :
  ∀ (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) (i : ℕ) (h : i < (a :: l).length),
    (a :: l).erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) i h) = (a :: l).eraseIdx i
⊢ l.erase (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h) = l.eraseIdx i

Tactic:
induction l generalizing i with
  | nil => simp
  | cons a l IH =>
    cases i with
    | zero => simp
    | succ i => grind

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l.Nodup
i : Fin l.length
⊢ l.erase (l.get i) = l.eraseIdx (↑i : ℕ)

Tactic:
simp [erase_getElem, hl]

Premises used: List.Nodup.erase_getElem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
⊢ l₁.Nodup → (l₁.diff l₂).Nodup

Tactic:
Nodup.sublist <| diff_sublist _ _

Premises used: List.diff_sublist, List.Nodup.sublist
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
L : List (List α)
⊢ L.flatten.Nodup ↔ (∀ (l : List α), l ∈ L → l.Nodup) ∧ Pairwise Disjoint L

Tactic:
simp only [Nodup, pairwise_flatten, disjoint_left.symm, forall_mem_ne]

Premises used: List.disjoint_left, List.Nodup, List.forall_mem_ne, List.pairwise_flatten, Iff.symm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
f : α → List β
simp :
  (Pairwise (fun (a b : α) ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup
⊢ (flatMap f l₁).Nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).Nodup) ∧ Pairwise (Disjoint on f) l₁

Tactic:
simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, mem_map,
    exists_imp, and_imp]

Premises used: and_imp, List.nodup_flatten, List.pairwise_map, and_comm, exists_imp, List.mem_map, List.flatMap
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
f : α → List β
rw rw₁ :
  (Pairwise (fun (a b : α) ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup
⊢ (Pairwise (fun (a b : α) ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup

Tactic:
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
      from forall_comm.trans <| forall_congr' fun _ => forall_eq']

Premises used: forall_comm, forall_eq', forall_congr', Iff.trans
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) x
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) x
rcases :
  ∀ (b₁ : β),
    b₁ ∈ l₂ →
      ∀ (h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁))
        (h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) (a₁, b₁)), False
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩

Premises used: Iff.mp, List.mem_map, rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left : b₁ ∈ l₂
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) (a₁, b₁)
⊢ a₁ ≠ a₁

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left : b₁ ∈ l₂
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) (a₁, b₁)
n₁ : a₁ ≠ a₁
⊢ Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left : b₁ ∈ l₂
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₂) (a₁, b₁)
n₁ : a₁ ≠ a₁
h₃ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
⊢ b₁ ∈ l₂

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ : α
b₁ : β
left : b₁ ∈ l₂
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
n : a₁ ≠ a₁
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
mb₂ : b₁ ∈ l₂
⊢ False

Tactic:
n rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ : α
b₁ : β
left : b₁ ∈ l₂
h₁ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
n : a₁ ≠ a₁
h₂ : Membership.mem (γ := List (α × β)) ((fun (a : α) ↦ map (Prod.mk a) l₂) a₁) (a₁, b₁)
mb₂ : b₁ ∈ l₂
⊢ False

Tactic:
exact n rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a : α
h_1 : a ∈ l₁
b b' : σ a
h : Sigma.mk (β := fun (a : α) ↦ σ a) a b = Sigma.mk (β := fun (a : α) ↦ σ a) a b'
⊢ b = b'

Tactic:
injection h with _ h
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁) x
h₂ : Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂) x
rcases :
  ∀ (b₁ : σ a₁),
    b₁ ∈ l₂ a₁ →
      ∀
        (h₁ :
          Membership.mem (γ := List ((a : α) × σ a))
            ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
            (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁))
        (h₂ :
          Membership.mem (γ := List ((a : α) × σ a))
            ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂)
            (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)),
        False
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩

Premises used: Iff.mp, List.mem_map, rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left : b₁ ∈ l₂ a₁
h₁ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
h₂ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
⊢ a₁ ≠ a₁

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left : b₁ ∈ l₂ a₁
h₁ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
h₂ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
n₁ : a₁ ≠ a₁
⊢ Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left : b₁ ∈ l₂ a₁
h₁ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
h₂ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₂)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
n₁ : a₁ ≠ a₁
h₃ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
⊢ b₁ ∈ l₂ a₁

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ : α
b₁ : σ a₁
left : b₁ ∈ l₂ a₁
h₁ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
n : a₁ ≠ a₁
h₂ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
mb₂ : b₁ ∈ l₂ a₁
⊢ False

Tactic:
n rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ : α
b₁ : σ a₁
left : b₁ ∈ l₂ a₁
h₁ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
n : a₁ ≠ a₁
h₂ :
  Membership.mem (γ := List ((a : α) × σ a)) ((fun (a : α) ↦ map (Sigma.mk (β := fun (a : α) ↦ σ a) a) (l₂ a)) a₁)
    (Sigma.mk (β := fun (a : α) ↦ σ a) a₁ b₁)
mb₂ : b₁ ∈ l₂ a₁
⊢ False

Tactic:
exact n rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
rw : b ∈ f a
⊢ b' ∈ f a

Tactic:
rw [← e]
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a

Tactic:
bm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a

Tactic:
exact bm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
rw : (l ++ [a]).Nodup
⊢ (l.concat a).Nodup

Tactic:
rw [concat_eq_append]

Premises used: List.concat_eq_append
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup

Tactic:
h'.append (nodup_singleton _) (disjoint_singleton.2 h)

Premises used: Iff.mpr, List.nodup_singleton, List.Nodup.append, List.disjoint_singleton
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup

Tactic:
exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)

Premises used: Iff.mpr, List.nodup_singleton, List.Nodup.append, List.disjoint_singleton
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : a ∈ l
rw : l.Nodup
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_mem h']

Premises used: List.insert_of_mem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Tactic:
h
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Tactic:
exact h
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
rw : ¬a ∈ l ∧ l.Nodup
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_not_mem h', nodup_cons]

Premises used: List.nodup_cons, List.insert_of_not_mem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' left : ¬a ∈ l
right : l.Nodup
⊢ ¬a ∈ l ∧ l.Nodup

Tactic:
constructor
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ ¬a ∈ l

Tactic:
assumption
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ l.Nodup

Tactic:
assumption
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l₂ : List α
h : l₂.Nodup
⊢ ([] ∪ l₂).Nodup

Tactic:
h

Premises used: List.foldr
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l₂ : List α
h : l₂.Nodup
⊢ ([] ∪ l₂).Nodup

Tactic:
exact h
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α} (h : l₂.Nodup), (l₁ ∪ l₂).Nodup
l₂ : List α
h : l₂.Nodup
⊢ (a :: l₁ ∪ l₂).Nodup

Tactic:
(ih h).insert

Premises used: List.Nodup.insert, List.foldr, ite
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α} (h : l₂.Nodup), (l₁ ∪ l₂).Nodup
l₂ : List α
h : l₂.Nodup
⊢ (a :: l₁ ∪ l₂).Nodup

Tactic:
exact (ih h).insert

Premises used: List.Nodup.insert
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
h : l₂.Nodup
nil : ∀ {l₂ : List α} (h : l₂.Nodup), ([] ∪ l₂).Nodup
cons :
  ∀ (a : α) (l₁ : List α) (ih : ∀ {l₂ : List α} (h : l₂.Nodup), (l₁ ∪ l₂).Nodup) {l₂ : List α} (h : l₂.Nodup),
    (a :: l₁ ∪ l₂).Nodup
⊢ (l₁ ∪ l₂).Nodup

Tactic:
induction l₁ generalizing l₂ with
  | nil => exact h
  | cons a l₁ ih => exact (ih h).insert

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ : List α
inst : BEq α
l₂ : List α
⊢ l₁.Nodup → (l₁ ∩ l₂).Nodup

Tactic:
Nodup.filter _

Premises used: List.Nodup.filter
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
h : l₁.Nodup
⊢ l₁.diff [] = List.filter (fun (x : α) ↦ decide ¬Membership.mem (γ := List α) [] x) l₁

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
rw : List.filter (fun (a_1 : α) ↦ decide ¬a_1 ∈ l₂ && a_1 != a) l₁ = List.filter (fun (x : α) ↦ decide ¬x ∈ a :: l₂) l₁
⊢ l₁.diff (a :: l₂) = List.filter (fun (x : α) ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]

Premises used: List.Nodup.erase, List.diff_cons, List.filter_filter, List.Nodup.erase_eq_filter
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun (a_1 : α) ↦ decide ¬a_1 ∈ l₂ && a_1 != a) l₁ = List.filter (fun (x : α) ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
simp only [decide_not, bne, Bool.and_comm, decide_mem_cons, Bool.not_or]

Premises used: Bool.not_or, bne, List.decide_mem_cons, decide_not, Bool.and_comm
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l₁ l₂ : List α
a : α
inst : BEq α
inst_1 : LawfulBEq α
hl₁ : l₁.Nodup
rw : a ∈ List.filter (fun (x : α) ↦ decide ¬x ∈ l₂) l₁ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
rw₁ : a ∈ l₁ ∧ (decide ¬a ∈ l₂) = true ↔ a ∈ l₁ ∧ ¬a ∈ l₂
rw₂ rw₃ : a ∈ l₁ ∧ ¬a ∈ l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Tactic:
rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]

Premises used: List.Nodup.diff_eq_filter, List.mem_filter, decide_eq_true_iff
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hl : Nodup.{u} (α := α) []
⊢ map (update (β := fun (a : α) ↦ β) f x y) [] =
    if Membership.mem (γ := List α) [] x then (map f []).set (idxOf x []) y else map f []

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update (β := fun (a : α) ↦ β) f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
?_
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
l : List α
hl : l.Nodup
f : α → β
x : α
y : β
cons :
  ∀ (hd : α) (tl : List α)
    (ihl :
      ∀ (hl : tl.Nodup),
        map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl)
    (hl : (hd :: tl).Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) (hd :: tl) =
      if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)
⊢ map (update (β := fun (a : α) ↦ β) f x y) l = if x ∈ l then (map f l).set (idxOf x l) y else map f l

Tactic:
induction l with | nil => simp | cons hd tl ihl => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ ¬hd ∈ tl ∧ tl.Nodup

Tactic:
rw [nodup_cons] at hl

Premises used: List.nodup_cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
cons :
  (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
⊢ map (update (β := fun (a : α) ↦ β) f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
simp only [mem_cons, map, ihl hl.2]

Premises used: List.map, And.right, List.mem_cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
pos :
  ∀ (H : hd = x),
    (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
      if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
neg :
  ∀ (H : ¬hd = x),
    (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
      if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
⊢ (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
by_cases H : hd = x
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
H : hd = x
pos :
  ∀ (hl : ¬x ∈ tl ∧ tl.Nodup),
    (update (β := fun (a : α) ↦ β) f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
      if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl
⊢ (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
subst hd
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬x ∈ tl ∧ tl.Nodup
⊢ (update (β := fun (a : α) ↦ β) f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl

Tactic:
simp [hl.1]

Premises used: And.left
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
inst : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl :
  ∀ (hl : tl.Nodup),
    map (update (β := fun (a : α) ↦ β) f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
H : ¬hd = x
⊢ (update (β := fun (a : α) ↦ β) f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
simp [Ne.symm H, H, ← apply_ite (cons (f hd))]

Premises used: apply_ite, Ne.symm, List.cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l

Tactic:
grind [List.pairwise_iff_forall_sublist]

Premises used: List.pairwise_iff_forall_sublist
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
n : ℕ
h : Nodup.{u} (α := α) []
⊢ Eq.{u + 1} (α := List α) (take n []) (List.filter (fun (a : α) ↦ elem a (take n [])) [])

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
h : (b :: l).Nodup
⊢ take 0 (b :: l) = List.filter (fun (a : α) ↦ elem a (take 0 (b :: l))) (b :: l)

Tactic:
simp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ elem b (b :: List.filter (fun (a : α) ↦ elem a (take n l)) l) = true

Tactic:
simp