awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ (r.push hd).toListAppend (go f (tl ++ [a]) #[]) =
    r.toListAppend ((Array.push #[] hd).toListAppend (go f (tl ++ [a]) #[]))

Tactic:
simp only [Array.toListAppend_eq, Array.toList_push, nil_append,
      append_assoc]

Premises used: Array.toList_push, Array.toListAppend_eq, List.append_assoc, List.nil_append
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
nil : go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])
cons : ∀ (hd : α) (tl : List α), go f (hd :: tl ++ [a]) r = r.toListAppend (go f (hd :: tl ++ [a]) #[])
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])

Tactic:
cases tl with
  | nil =>
    simp only [nil_append, modifyLast.go]; rfl
  | cons hd tl =>
    simp only [cons_append]
    rw [modifyLast.go, modifyLast.go]
    case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]
    simp only [Array.toListAppend_eq, Array.toList_push, nil_append,
      append_assoc]

Premises used: Array.toList_push, Array.toListAppend_eq, List.append_assoc, List.modifyLast.go, List.cons, List.cons_ne_nil, List.nil_append, List.cons_append, List.append_ne_nil_of_right_ne_nil, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
⊢ modifyLast f ([] ++ [a]) = [] ++ [f a]

Tactic:
simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq]

Premises used: Array.toListAppend_eq, List.modifyLast, List.modifyLast.go, List.nil_append
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
cons : modifyLast.go f (tl ++ [a]) (Array.push #[] head) = head :: (tl ++ [f a])
rw : tl ++ [a] = [] → False
⊢ modifyLast.go f (head :: (tl ++ [a])) #[] = head :: (tl ++ [f a])

Tactic:
rw [modifyLast.go]

Premises used: List.modifyLast.go
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Premises used: List.cons_ne_nil, Not, List.append_ne_nil_of_right_ne_nil, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Premises used: List.cons_ne_nil, List.append_ne_nil_of_right_ne_nil, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Premises used: List.cons_ne_nil, List.append_ne_nil_of_right_ne_nil, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
cons : modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
⊢ modifyLast.go f (tl ++ [a]) (Array.push #[] head) = head :: (tl ++ [f a])

Tactic:
rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray,
      nil_append, cons_append, nil_append, cons_inj_right]

Premises used: Array.toList_push, Array.toListAppend_eq, List.cons_inj_right, List.toList_toArray, List.nil_append, List.cons_append, _private.0.List.modifyLast.go_concat
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]

Tactic:
modifyLast_concat _ _ tl
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]

Tactic:
exact modifyLast_concat _ _ tl
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
a : α
l : List α
nil : modifyLast f ([] ++ [a]) = [] ++ [f a]
cons : ∀ (head : α) (tl : List α), modifyLast f (head :: tl ++ [a]) = head :: tl ++ [f a]
⊢ modifyLast f (l ++ [a]) = l ++ [f a]

Tactic:
cases l with
  | nil =>
    simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq]
  | cons _ tl =>
    simp only [cons_append, modifyLast]
    rw [modifyLast.go]
    case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray,
      nil_append, cons_append, nil_append, cons_inj_right]
    exact modifyLast_concat _ _ tl

Premises used: Array.toList_push, Array.toListAppend_eq, List.modifyLast, List.modifyLast.go, List.cons_inj_right, List.cons, List.toList_toArray, List.nil_append, List.cons_append, _private.0.List.modifyLast.go_concat, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
h : Ne.{u_1 + 1} (α := List α) [] []
⊢ modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []

Tactic:
contradiction
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd : α
h : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]

Tactic:
modifyLast_concat _ hd _

Premises used: List.modifyLast.go, dite, Array.foldrM, List.modifyLast_concat, ite
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd : α
h : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]

Tactic:
exact modifyLast_concat _ hd _

Premises used: List.modifyLast_concat
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
h : hd :: hd' :: tl' ≠ []
rw rw₁ : hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ hd :: hd' :: tl') = l₁ ++ modifyLast f (hd :: hd' :: tl')

Tactic:
rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]

Premises used: List.append_assoc, List.cons, List.nil_append, List.append_cons, HAppend.hAppend, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
h : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
cons_ne_nil _ _

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
h : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
exact cons_ne_nil _ _

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
h : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

Tactic:
{ exact cons_ne_nil _ _ }

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
h : hd :: tl ≠ []
cons : [hd] ≠ [] → modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]
cons₁ :
  ∀ (hd' : α) (tl' : List α),
    hd :: hd' :: tl' ≠ [] → modifyLast f (l₁ ++ hd :: hd' :: tl') = l₁ ++ modifyLast f (hd :: hd' :: tl')
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)

Tactic:
cases tl with
    | nil => exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }

Premises used: List.append_assoc, List.cons, List.cons_ne_nil, List.nil_append, List.append_cons, List.modifyLast_concat, List.nil
-- Module: Mathlib.Data.List.ModifyLast
Goal:
α : Type u_1
f : α → α
l₁ l₂ : List α
h : l₂ ≠ []
nil : Ne.{u_1 + 1} (α := List α) [] [] → modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []
cons : ∀ (hd : α) (tl : List α), hd :: tl ≠ [] → modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Tactic:
cases l₂ with
  | nil => contradiction
  | cons hd tl =>
    cases tl with
    | nil => exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }

Premises used: List.append_assoc, List.cons, List.cons_ne_nil, List.nil_append, List.append_cons, List.nil
-- Module: Mathlib.Data.List.Monad
Goal:
α : Type u
a : α
⊢ pure a = [a]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Monad
Goal:
α : Type u
⊢ LawfulMonad List

Tactic:
LawfulMonad.mk'
  (id_map := map_id)
  (pure_bind := fun _ _ => List.append_nil _)
  (bind_assoc := fun _ _ _ => List.flatMap_assoc)
  (bind_pure_comp := fun _ _ => map_eq_flatMap.symm)

Premises used: List.map_id, List.map_eq_flatMap, LawfulMonad.mk', List.append_nil, List.flatMap_assoc, Eq.symm
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
x : ℕ × ℕ
rcases : ∀ (x y : ℕ), (x, y) ∈ antidiagonal n ↔ (x, y).fst + (x, y).snd = n
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n

Tactic:
rcases x with ⟨x, y⟩
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n x y : ℕ
simp : x < n + 1 ∧ n - x = y ↔ x + y = n
⊢ (x, y) ∈ antidiagonal n ↔ (x, y).fst + (x, y).snd = n

Tactic:
simp [antidiagonal]

Premises used: List.Nat.antidiagonal
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n x y : ℕ
⊢ x < n + 1 ∧ n - x = y ↔ x + y = n

Tactic:
grind
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
rw : length (α := ℕ × ℕ) (map (fun (i : ℕ) ↦ (i, n - i)) (range (n + 1))) = n + 1
rw₁ : (range (n + 1)).length = n + 1
rw₂ rw₃ : n + 1 = n + 1
⊢ (antidiagonal n).length = n + 1

Tactic:
rw [antidiagonal, length_map, length_range]

Premises used: List.length_range, List.length_map, List.Nat.antidiagonal
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
⊢ antidiagonal 0 = [(0, 0)]

Tactic:
rfl

Premises used: List.map, rfl, List.Nat.antidiagonal
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
⊢ (antidiagonal n).Nodup

Tactic:
nodup_range.map ((@LeftInverse.injective ℕ (ℕ × ℕ) Prod.fst fun i ↦ (i, n - i)) fun _ ↦ rfl)

Premises used: Function.LeftInverse.injective, List.Nodup.map, List.nodup_range, rfl, List.Nat.antidiagonal
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
simp :
  (0, n + 1) :: (Nat.succ 0, n) :: map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    (0, n + 1) :: (Nat.succ 0, n) :: map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)

Tactic:
simp only [antidiagonal, range_succ_eq_map, map_cons, Nat.add_succ_sub_one,
    Nat.add_zero, id, Nat.sub_zero, map_map, Prod.map_apply]

Premises used: List.map_cons, id, List.map_map, List.range_succ_eq_map, Nat.add_succ_sub_one, Prod.map_apply, Nat.sub_zero, Nat.add_zero, List.Nat.antidiagonal
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
apply :
  Eq (α := List (ℕ × ℕ)) (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))
    (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n))
⊢ (0, n + 1) :: (Nat.succ 0, n) :: map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    (0, n + 1) :: (Nat.succ 0, n) :: map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)

Tactic:
apply congr rfl (congr rfl _)

Premises used: congr, rfl
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
h :
  ∀ (i : ℕ) (a : ℕ × ℕ),
    getElem? (valid := fun (as : List (ℕ × ℕ)) (i : ℕ) ↦ i < as.length)
          (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n)) i =
        some a ↔
      getElem? (valid := fun (as : List (ℕ × ℕ)) (i : ℕ) ↦ i < as.length)
          (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)) i =
        some a
⊢ Eq (α := List (ℕ × ℕ)) (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))
    (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n))

Tactic:
ext
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n i : ℕ
a : ℕ × ℕ
⊢ getElem? (valid := fun (as : List (ℕ × ℕ)) (i : ℕ) ↦ i < as.length)
        (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n)) i =
      some a ↔
    getElem? (valid := fun (as : List (ℕ × ℕ)) (i : ℕ) ↦ i < as.length)
        (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)) i =
      some a

Tactic:
simp
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
⊢ antidiagonal (n + 1) = map (Prod.map id Nat.succ) (antidiagonal n) ++ [(n + 1, 0)]

Tactic:
simp +contextual [antidiagonal, range_succ, Nat.le_of_lt, Nat.sub_add_comm]

Premises used: Nat.sub_add_comm, Nat.le_of_lt, List.Nat.antidiagonal, List.range_succ
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
rw :
  map (Prod.map id Nat.succ) ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
rw [antidiagonal_succ', antidiagonal_succ]

Premises used: List.Nat.antidiagonal_succ, List.Nat.antidiagonal_succ'
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
⊢ map (Prod.map id Nat.succ) ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
simp
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
rw :
  Eq (α := List (ℕ × ℕ)) (map (Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) (range (n + 1)))
    (map ((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))
⊢ map Prod.swap (antidiagonal n) = (antidiagonal n).reverse

Tactic:
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
    range_eq_range', map_map]

Premises used: List.map_map, List.map_reverse, List.range_eq_range', List.reverse_range', List.Nat.antidiagonal
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
h :
  ∀ (a : ℕ),
    a ∈ range (n + 1) →
      Eq (α := ℕ × ℕ) ((Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) a)
        (((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) a)
⊢ Eq (α := List (ℕ × ℕ)) (map (Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) (range (n + 1)))
    (map ((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))

Tactic:
apply map_congr_left

Premises used: List.map_congr_left
-- Module: Mathlib.Data.List.NatAntidiagonal
Goal:
n : ℕ
⊢ ∀ (a : ℕ),
    a ∈ range (n + 1) →
      Eq (α := ℕ × ℕ) ((Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) a)
        (((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) a)

Tactic:
simp +contextual [Nat.sub_sub_self, Nat.lt_succ_iff]

Premises used: Nat.sub_sub_self, Nat.lt_succ_iff
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
r : α → α → Prop
inst : Std.Irrefl r
h : Pairwise r l
⊢ l.Nodup

Tactic:
h.imp ne_of_irrefl

Premises used: ne_of_irrefl, List.Nodup, List.Pairwise.imp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
⊢ (fun (x1 x2 : Prop) ↦ x1 ↔ x2) (Nodup.{u} (α := α) []) (Nodup.{v} (α := β) [])

Tactic:
simp only [nodup_nil]

Premises used: List.nodup_nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
a : α
b : β
l₁ : List α
l₂ : List β
hab : r a b
h : Forall₂ r l₁ l₂
⊢ (fun (x1 x2 : Prop) ↦ x1 ↔ x2) (a :: l₁).Nodup (b :: l₂).Nodup

Tactic:
simpa only [nodup_cons] using
      Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)

Premises used: Relator.rel_not, List.nodup_cons, List.rel_mem, Relator.rel_and
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
ha : ¬a ∈ l
hl : l.Nodup
⊢ (a :: l).Nodup

Tactic:
nodup_cons.2 ⟨ha, hl⟩

Premises used: Iff.mpr, List.nodup_cons, And.intro
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
⊢ [a].Nodup

Tactic:
pairwise_singleton _ _

Premises used: List.Nodup, List.pairwise_singleton
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
h : (a :: l).Nodup
⊢ l.Nodup

Tactic:
(nodup_cons.1 h).2

Premises used: List.nodup_cons, And.right, Iff.mp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
h : (a :: l).Nodup
⊢ ¬a ∈ l

Tactic:
(nodup_cons.1 h).1

Premises used: List.nodup_cons, And.left, Iff.mp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
a : α
⊢ a ∈ l → ¬(a :: l).Nodup

Tactic:
imp_not_comm.1 Nodup.notMem

Premises used: imp_not_comm, List.Nodup.notMem, Iff.mp
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
⊢ ¬[a, a].Nodup

Tactic:
not_nodup_cons_of_mem <| mem_singleton_self _

Premises used: List.mem_singleton_self, List.not_nodup_cons_of_mem
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
nil : (∀ (a : α), ¬[a, a] <+ []) → Nodup.{u} (α := α) []
cons :
  ∀ (head : α) (tail : List α),
    ((∀ (a : α), ¬[a, a] <+ tail) → tail.Nodup) → (∀ (a : α), ¬[a, a] <+ head :: tail) → (head :: tail).Nodup
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup

Tactic:
induction l
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ Nodup.{u} (α := α) []

Tactic:
nodup_nil

Premises used: List.nodup_nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ Nodup.{u} (α := α) []

Tactic:
exact nodup_nil

Premises used: List.nodup_nil
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ (a :: l).Nodup

Tactic:
(IH fun a s => h a <| sublist_cons_of_sublist _ s).cons
          fun al => h a <| (singleton_sublist.2 al).cons_cons _

Premises used: Iff.mpr, List.sublist_cons_of_sublist, List.Sublist.cons_cons, List.singleton_sublist, List.Nodup.cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ (a :: l).Nodup

Tactic:
exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons
          fun al => h a <| (singleton_sublist.2 al).cons_cons _

Premises used: Iff.mpr, List.sublist_cons_of_sublist, List.Sublist.cons_cons, List.singleton_sublist, List.Nodup.cons
-- Module: Mathlib.Data.List.Nodup
Goal:
α : Type u
l : List α
le : α → α → Bool
⊢ (l.mergeSort le).Nodup ↔ l.Nodup

Tactic:
(mergeSort_perm l le).nodup_iff

Premises used: List.Perm.nodup_iff, List.mergeSort_perm
-- 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 j : Fin l.length
hg :
  Eq.{u + 1} (α := α)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) i)
    ((fun (i : Fin l.length) ↦ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) j)
obtain :
  ∀ (i : ℕ) (hi : i < 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)),
    (⟨i, hi⟩ : Fin l.length) = j
⊢ i = j

Tactic:
obtain ⟨i, hi⟩ := i
-- 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
j : Fin l.length
i : ℕ
hi : i < 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)
obtain :
  ∀ (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⟩)),
    (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
⊢ (⟨i, hi⟩ : Fin l.length) = j

Tactic:
obtain ⟨j, hj⟩ := j
-- 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⟩)
inl : ∀ (hij : i < j), (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
inr :
  ∀ (hj : i < 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 : ℕ) ⋯) ⟨i, hj⟩)),
    (⟨i, hi⟩ : Fin l.length) = ⟨i, hj⟩
inr₁ : ∀ (hji : j < i), (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩

Tactic:
rcases Nat.lt_trichotomy i j with (hij | rfl | hji)

Premises used: Nat.lt_trichotomy, rfl
-- 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⟩)
hij : i < j
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩

Tactic:
(h i j hi hj hij hg).elim

Premises used: False.elim
-- 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⟩)
hij : i < j
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨j, hj⟩

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

Premises used: False.elim
-- 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 hj : i < 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 : ℕ) ⋯) ⟨i, hj⟩)
⊢ (⟨i, hi⟩ : Fin l.length) = ⟨i, hj⟩

Tactic:
rfl
-- 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:
(h j i hj hi hji hg.symm).elim

Premises used: False.elim, Eq.symm