awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
⊢ take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse

Tactic:
simp [take_length_add_append]

Premises used: List.take_length_add_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - (n + 1)) (xs ++ [x]) = (drop (n + 1) (xs ++ [x]).reverse).reverse

Tactic:
simp [take_append, IH]

Premises used: List.take_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
n : ℕ
nil : ∀ (n : ℕ), Eq.{u_1 + 1} (α := List α) (take (length.{u_1} (α := α) [] - n) []) (reverse (drop n (reverse [])))
append_singleton :
  ∀ (xs : List α) (x : α) (IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse) (n : ℕ),
    take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse
⊢ take (l.length - n) l = (drop n l.reverse).reverse

Tactic:
induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]

Premises used: List.take_append, List.take_length_add_append, List.nil
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rdrop (n + 1) = l.rdrop n

Tactic:
simp [rdrop_eq_reverse_drop_reverse]

Premises used: List.rdrop_eq_reverse_drop_reverse
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := List α) (rtake [] n) []

Tactic:
simp [rtake]

Premises used: List.rtake
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
⊢ l.rtake 0 = []

Tactic:
simp [rtake]

Premises used: List.rtake
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
n : ℕ
⊢ Eq.{u_1 + 1} (α := List α) (drop (length.{u_1} (α := α) [] - n) []) (reverse (take n (reverse [])))

Tactic:
simp
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
append_singleton : drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse
append_singleton₁ :
  ∀ (n : ℕ), drop ((xs ++ [x]).length - (n + 1)) (xs ++ [x]) = (take (n + 1) (xs ++ [x]).reverse).reverse
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse

Tactic:
cases n
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
⊢ drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse

Tactic:
drop_length

Premises used: List.reverseAux, List.reverse, List.drop_length
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
⊢ drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse

Tactic:
exact drop_length

Premises used: List.drop_length
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - (n + 1)) (xs ++ [x]) = (take (n + 1) (xs ++ [x]).reverse).reverse

Tactic:
simp [drop_append, IH]

Premises used: List.drop_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
n : ℕ
nil : ∀ (n : ℕ), Eq.{u_1 + 1} (α := List α) (drop (length.{u_1} (α := α) [] - n) []) (reverse (take n (reverse [])))
append_singleton :
  ∀ (xs : List α) (x : α) (IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse) (n : ℕ),
    drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse
⊢ drop (l.length - n) l = (take n l.reverse).reverse

Tactic:
induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · exact drop_length
    · simp [drop_append, IH]

Premises used: List.drop_append, List.nil, List.drop_length
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]

Tactic:
simp [rtake_eq_reverse_take_reverse]

Premises used: List.rtake_eq_reverse_take_reverse
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
⊢ rdropWhile p [] = []

Tactic:
simp [rdropWhile]

Premises used: List.rdropWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
simp :
  reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

Tactic:
simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]

Premises used: List.reverse_singleton, List.singleton_append, List.rdropWhile, List.dropWhile, List.reverse_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
pos :
  ∀ (h : p x = true),
    reverse
        (match (motive := Bool → List α) p x with
        | true => dropWhile p l.reverse
        | false => x :: l.reverse) =
      (dropWhile p l.reverse).reverse
neg :
  ∀ (h : ¬p x = true),
    reverse
        (match (motive := Bool → List α) p x with
        | true => dropWhile p l.reverse
        | false => x :: l.reverse) =
      l ++ [x]
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    (dropWhile p l.reverse).reverse

Tactic:
simp [h]
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse) =
    l ++ [x]

Tactic:
simp [h]
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
rw : (if p x = true then rdropWhile p l else l ++ [x]) = rdropWhile p l
rw₁ rw₂ : rdropWhile p l = rdropWhile p l
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l

Tactic:
rw [rdropWhile_concat, if_pos h]

Premises used: if_pos, List.rdropWhile_concat
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
rw : (if p x = true then rdropWhile p l else l ++ [x]) = l ++ [x]
rw₁ rw₂ : l ++ [x] = l ++ [x]
⊢ rdropWhile p (l ++ [x]) = l ++ [x]

Tactic:
rw [rdropWhile_concat, if_neg h]

Premises used: if_neg, List.rdropWhile_concat
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
x : α
rw : rdropWhile p ([] ++ [x]) = if p x = true then [] else [] ++ [x]
rw₁ : (if p x = true then rdropWhile p [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]
rw₂ rw₃ : (if p x = true then [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]
⊢ rdropWhile p [x] = if p x = true then [] else [x]

Tactic:
rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]

Premises used: List.cons, List.rdropWhile_nil, List.nil_append, List.nil, List.rdropWhile_concat
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
simp_rw : ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true
⊢ ¬p ((rdropWhile p l).getLast hl) = true

Tactic:
simp_rw [rdropWhile]

Premises used: List.rdropWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
rw : ¬false = true
⊢ ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true

Tactic:
rw [getLast_reverse, head_dropWhile_not p]

Premises used: List.getLast_reverse, List.head_dropWhile_not
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬false = true

Tactic:
simp
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
rw : dropWhile p l.reverse <:+ l.reverse
⊢ rdropWhile p l <+: l

Tactic:
rw [← reverse_suffix, rdropWhile, reverse_reverse]

Premises used: List.reverse_reverse, List.rdropWhile, List.reverse_suffix
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l.reverse <:+ l.reverse

Tactic:
dropWhile_suffix _

Premises used: List.dropWhile_suffix
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l.reverse <:+ l.reverse

Tactic:
exact dropWhile_suffix _

Premises used: List.dropWhile_suffix
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp [rdropWhile]

Premises used: List.rdropWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
simp [rdropWhile, reverse_eq_iff, getLast_eq_getElem, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero, List.reverse_eq_iff, List.rdropWhile, List.getLast_eq_getElem
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
simp :
  ∀ (hl : 0 < (dropWhile p l).length),
    ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p l) 0 hl) = true
⊢ dropWhile p (dropWhile p l) = dropWhile p l

Tactic:
simp only [dropWhile_eq_self_iff]

Premises used: List.dropWhile_eq_self_iff
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < (dropWhile p l).length),
    ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p l) 0 hl) = true

Tactic:
fun h => dropWhile_get_zero_not p l h

Premises used: List.dropWhile_get_zero_not
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < (dropWhile p l).length),
    ¬p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (dropWhile p l) 0 hl) = true

Tactic:
exact fun h => dropWhile_get_zero_not p l h

Premises used: List.dropWhile_get_zero_not
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p (rdropWhile p l) = rdropWhile p l

Tactic:
rdropWhile_eq_self_iff.mpr (rdropWhile_last_not _ _)

Premises used: Iff.mpr, List.rdropWhile_last_not, List.rdropWhile_eq_self_iff
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
⊢ rtakeWhile p [] = []

Tactic:
simp [rtakeWhile]

Premises used: List.rtakeWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
simp :
  reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []) =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []

Tactic:
simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]

Premises used: List.reverse_singleton, List.singleton_append, List.rtakeWhile, List.takeWhile, List.reverse_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
pos :
  ∀ (h : p x = true),
    reverse
        (match (motive := Bool → List α) p x with
        | true => x :: takeWhile p l.reverse
        | false => []) =
      (takeWhile p l.reverse).reverse ++ [x]
neg :
  ∀ (h : ¬p x = true),
    Eq.{u_1 + 1} (α := List α)
      (reverse
        (match (motive := Bool → List α) p x with
        | true => x :: takeWhile p l.reverse
        | false => []))
      []
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []) =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []) =
    (takeWhile p l.reverse).reverse ++ [x]

Tactic:
simp [h]
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ Eq.{u_1 + 1} (α := List α)
    (reverse
      (match (motive := Bool → List α) p x with
      | true => x :: takeWhile p l.reverse
      | false => []))
    []

Tactic:
simp [h]
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
rw : (if p x = true then rtakeWhile p l ++ [x] else []) = rtakeWhile p l ++ [x]
rw₁ rw₂ : rtakeWhile p l ++ [x] = rtakeWhile p l ++ [x]
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Tactic:
rw [rtakeWhile_concat, if_pos h]

Premises used: if_pos, List.rtakeWhile_concat
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
rw : (if p x = true then rtakeWhile p l ++ [x] else []) = []
rw₁ rw₂ : Eq.{u_1 + 1} (α := List α) [] []
⊢ rtakeWhile p (l ++ [x]) = []

Tactic:
rw [rtakeWhile_concat, if_neg h]

Premises used: List.rtakeWhile_concat, if_neg
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
rw : takeWhile p l.reverse <+: l.reverse
⊢ rtakeWhile p l <:+ l

Tactic:
rw [← reverse_prefix, rtakeWhile, reverse_reverse]

Premises used: List.reverse_prefix, List.reverse_reverse, List.rtakeWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l.reverse <+: l.reverse

Tactic:
takeWhile_prefix _

Premises used: List.takeWhile_prefix
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l.reverse <+: l.reverse

Tactic:
exact takeWhile_prefix _

Premises used: List.takeWhile_prefix
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp [rtakeWhile, reverse_eq_iff]

Premises used: List.reverse_eq_iff, List.rtakeWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
nil : rtakeWhile p [] = [] ↔ ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), ¬p (getLast [] hl) = true
append_singleton :
  ∀ (l : List α) (a : α),
    (rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true) →
      (rtakeWhile p (l ++ [a]) = [] ↔ ∀ (hl : l ++ [a] ≠ []), ¬p ((l ++ [a]).getLast hl) = true)
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
induction l using List.reverseRecOn
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p [] = [] ↔ ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), ¬p (getLast [] hl) = true

Tactic:
simp [rtakeWhile]

Premises used: List.rtakeWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l l_1 : List α
a : α
h : rtakeWhile p l_1 = [] ↔ ∀ (hl : l_1 ≠ []), ¬p (l_1.getLast hl) = true
⊢ rtakeWhile p (l_1 ++ [a]) = [] ↔ ∀ (hl : l_1 ++ [a] ≠ []), ¬p ((l_1 ++ [a]).getLast hl) = true

Tactic:
simp [rtakeWhile]

Premises used: List.rtakeWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ x ∈ takeWhile p l.reverse

Tactic:
rw [rtakeWhile, mem_reverse] at hx

Premises used: List.mem_reverse, List.rtakeWhile
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true

Tactic:
mem_takeWhile_imp hx

Premises used: List.mem_takeWhile_imp
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true

Tactic:
exact mem_takeWhile_imp hx

Premises used: List.mem_takeWhile_imp
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p (rtakeWhile p l) = rtakeWhile p l

Tactic:
rtakeWhile_eq_self_iff.mpr fun _ => mem_rtakeWhile_imp

Premises used: Iff.mpr, List.mem_rtakeWhile_imp, List.rtakeWhile_eq_self_iff
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
p : α → Bool
l : List α
rw : (takeWhile p l.reverse ++ dropWhile p l.reverse).reverse = l
rw₁ : l.reverse.reverse = l
rw₂ rw₃ : l = l
⊢ (dropWhile p l.reverse).reverse ++ (takeWhile p l.reverse).reverse = l

Tactic:
rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]

Premises used: List.takeWhile_append_dropWhile, List.reverse_reverse, List.reverse_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l : List α
i j : ℕ
simp_rw : (drop j (drop i l.reverse).reverse.reverse).reverse = (drop (i + j) l.reverse).reverse
simp_rw₁ : (drop j (drop i l.reverse)).reverse = (drop (i + j) l.reverse).reverse
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)

Tactic:
simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]

Premises used: List.drop_drop, List.rdrop_eq_reverse_drop_reverse, List.reverse_reverse
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l₁ l₂ : List α
rw : (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
rw₁ : (drop l₂.reverse.length (l₁ ++ l₂).reverse).reverse = l₁
rw₂ : (drop l₂.reverse.length (l₂.reverse ++ l₁.reverse)).reverse = l₁
rw₃ : l₁.reverse.reverse = l₁
rw₄ rw₅ : l₁ = l₁
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁

Tactic:
rw [rdrop_eq_reverse_drop_reverse, ← length_reverse,
      reverse_append, drop_left, reverse_reverse]

Premises used: List.rdrop_eq_reverse_drop_reverse, List.length_reverse, List.drop_left, List.reverse_reverse, List.reverse_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.length
⊢ k ≤ l₂.reverse.length

Tactic:
rw [← length_reverse] at hk

Premises used: List.length_reverse
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
rw : (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
rw₁ : (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k
rw₂ : (drop k l₂.reverse ++ l₁.reverse).reverse = l₁ ++ l₂.rdrop k
rw₃ : l₁.reverse.reverse ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
rw₄ : l₁ ++ (drop k l₂.reverse).reverse = l₁ ++ l₂.rdrop k
rw₅ rw₆ : l₁ ++ l₂.rdrop k = l₁ ++ l₂.rdrop k
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]

Premises used: List.rdrop_eq_reverse_drop_reverse, List.drop_append_of_le_length, List.reverse_reverse, List.reverse_append
-- Module: Mathlib.Data.List.DropRight
Goal:
α : Type u_1
l₁ l₂ : List α
k : ℕ
rw : ((l₁ ++ l₂).rdrop l₂.length).rdrop k = l₁.rdrop k
rw₁ rw₂ : l₁.rdrop k = l₁.rdrop k
⊢ (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k

Tactic:
rw [← rdrop_add, rdrop_append_length]

Premises used: List.rdrop_append_length, List.rdrop_add
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈+ x :: l

Tactic:
Duplicate.cons_mem h

Premises used: List.Duplicate.cons_mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ x ∈+ y :: l

Tactic:
Duplicate.cons_duplicate h

Premises used: List.Duplicate.cons_duplicate
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l_1 : List α
h : x ∈ l_1
⊢ x ∈ x :: l_1

Tactic:
mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l_1 : List α
h : x ∈ l_1
⊢ x ∈ x :: l_1

Tactic:
exact mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
l_1 : List α
h : x ∈+ l_1
hm : x ∈ l_1
⊢ x ∈ y :: l_1

Tactic:
mem_cons_of_mem _ hm

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
l_1 : List α
h : x ∈+ l_1
hm : x ∈ l_1
⊢ x ∈ y :: l_1

Tactic:
exact mem_cons_of_mem _ hm

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
cons_mem : ∀ {l : List α}, x ∈ l → x ∈ x :: l
cons_duplicate : ∀ {y : α} {l : List α}, x ∈+ l → ∀ (hm : x ∈ l), x ∈ y :: l
⊢ x ∈ l

Tactic:
induction h with
  | cons_mem => exact mem_cons_self
  | cons_duplicate _ hm => exact mem_cons_of_mem _ hm

Premises used: List.Duplicate.cons_duplicate, List.Duplicate.cons_mem, List.mem_cons_self
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
cons_mem : ∀ (h : x ∈ l), x ∈ l
cons_duplicate : ∀ (h : x ∈+ l), x ∈ l
⊢ x ∈ l

Tactic:
obtain h | h := h
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

Tactic:
h
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

Tactic:
exact h
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Tactic:
h.mem

Premises used: List.Duplicate.mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Tactic:
exact h.mem

Premises used: List.Duplicate.mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
⊢ x ∈+ x :: l ↔ x ∈ l

Tactic:
⟨Duplicate.mem_cons_self, Mem.duplicate_cons_self⟩

Premises used: List.Mem.duplicate_cons_self, Iff.intro, List.Duplicate.mem_cons_self
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ l ≠ []

Tactic:
fun H => (mem_nil_iff x).mp (H ▸ h.mem)

Premises used: Eq.rec, List.Duplicate.mem, Iff.mp, List.mem_nil_iff, Not
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
x : α
⊢ ¬x ∈+ []

Tactic:
fun H => H.ne_nil rfl

Premises used: List.Duplicate.ne_nil, Not, rfl
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
l_1 : List α
h : x ∈ l_1
⊢ x :: l_1 ≠ [y]

Tactic:
simp [ne_nil_of_mem h]

Premises used: List.ne_nil_of_mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y y_1 : α
l_1 : List α
h : x ∈+ l_1
a_ih : l_1 ≠ [y]
⊢ y_1 :: l_1 ≠ [y]

Tactic:
simp [ne_nil_of_mem h.mem]

Premises used: List.ne_nil_of_mem, List.Duplicate.mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
cons_mem : ∀ {l : List α} (h : x ∈ l), x :: l ≠ [y]
cons_duplicate : ∀ {y_1 : α} {l : List α} (h : x ∈+ l), l ≠ [y] → y_1 :: l ≠ [y]
⊢ l ≠ [y]

Tactic:
induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]

Premises used: List.Duplicate.cons_duplicate, List.Duplicate.cons_mem, List.ne_nil_of_mem, List.Duplicate.mem
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
x y : α
⊢ ¬x ∈+ [y]

Tactic:
fun H => H.ne_singleton _ rfl

Premises used: Not, rfl, List.Duplicate.ne_singleton
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
x : α
h : x ∈+ []
⊢ False

Tactic:
not_duplicate_nil x h

Premises used: List.not_duplicate_nil
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
x y : α
h : x ∈+ [y]
⊢ False

Tactic:
not_duplicate_singleton x y h

Premises used: List.not_duplicate_singleton
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l

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

Premises used: Iff.intro
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
refine_1 : ∀ (h : x ∈+ y :: l), y = x ∧ x ∈ l ∨ x ∈+ l
refine_2 : ∀ (h : y = x ∧ x ∈ l ∨ x ∈+ l), x ∈+ y :: l
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
refine_1 : ∀ (hm : x ∈ l), x = x ∧ x ∈ l ∨ x ∈+ l
refine_1₁ : ∀ (hm : x ∈+ l), y = x ∧ x ∈ l ∨ x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
obtain hm | hm := h
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
Or.inl ⟨rfl, hm⟩

Premises used: And.intro, Or.inl, rfl
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
exact Or.inl ⟨rfl, hm⟩

Premises used: Or.inl