awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h_1 : l₁.length ≤ l₂.length
h : l₁ <+: l₂ ++ l₃
rw : ∀ (h : l₁ = take l₁.length (l₂ ++ l₃)), l₁ = take l₁.length l₂
⊢ l₁ <+: l₂

Tactic:
rw [prefix_iff_eq_take] at *

Premises used: List.prefix_iff_eq_take
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h_1 : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
nth_rw : l₃ = [] ∨ l₁.length ≤ l₂.length
⊢ l₁ = take l₁.length l₂

Tactic:
nth_rw 1 [h, take_eq_left_iff]

Premises used: List.take_eq_left_iff
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h_1 : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
tauto : ¬l₃ = [] → l₁.length ≤ l₂.length
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length

Tactic:
tauto
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
m n : ℕ
simp : min m l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n
⊢ take m l <+: take n l ↔ m ≤ n ∨ l.length ≤ n

Tactic:
simp [prefix_take_iff, take_prefix]

Premises used: List.take_prefix, List.prefix_take_iff
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
m n : ℕ
⊢ min m l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n

Tactic:
omega
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+: l₂
rcases : ∀ (l : List (List α)), l₁.flatten <+: (l₁ ++ l).flatten
⊢ l₁.flatten <+: l₂.flatten

Tactic:
rcases h with ⟨l, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <+: (l₁ ++ l).flatten

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
h : l₁ <+: l₂
f : α → List β
⊢ flatMap f l₁ <+: flatMap f l₂

Tactic:
(h.map _).flatten

Premises used: List.IsPrefix.map, List.IsPrefix.flatten
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+ l₂
rcases : ∀ (l : List (List α)), l₁.flatten <:+ (l ++ l₁).flatten
⊢ l₁.flatten <:+ l₂.flatten

Tactic:
rcases h with ⟨l, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <:+ (l ++ l₁).flatten

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
h : l₁ <:+ l₂
f : α → List β
⊢ flatMap f l₁ <:+ flatMap f l₂

Tactic:
(h.map _).flatten

Premises used: List.IsSuffix.flatten, List.IsSuffix.map
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+: l₂
rcases : ∀ (l l' : List (List α)), l₁.flatten <:+: (l ++ l₁ ++ l').flatten
⊢ l₁.flatten <:+: l₂.flatten

Tactic:
rcases h with ⟨l, l', rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l l' : List (List α)
⊢ l₁.flatten <:+: (l ++ l₁ ++ l').flatten

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
h : l₁ <:+: l₂
f : α → List β
⊢ flatMap f l₁ <:+: flatMap f l₂

Tactic:
(h.map _).flatten

Premises used: List.IsInfix.map, List.IsInfix.flatten
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
n m : ℕ
l : List α
rw : take n l ++ drop (n + m) l = take n l ++ drop m (drop n l)
rw₁ : take n l ++ drop (n + m) l = take n l ++ drop (n + m) l
rw₂ rw₃ : take n l ++ drop (m + n) l = take n l ++ drop (m + n) l
⊢ dropSlice n m l = take n l ++ drop m (drop n l)

Tactic:
rw [dropSlice_eq, drop_drop, Nat.add_comm]

Premises used: List.drop_drop, List.dropSlice_eq, Nat.add_comm
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
n m : ℕ
l : List α
⊢ dropSlice n m l ⊆ l

Tactic:
(dropSlice_sublist n m l).subset

Premises used: List.dropSlice_sublist, List.Sublist.subset
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
n m : ℕ
l : List α
a : α
h : a ∈ dropSlice n m l
⊢ a ∈ l

Tactic:
dropSlice_subset n m l h

Premises used: List.dropSlice_subset
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
⊢ l.tail ⊆ l

Tactic:
(tail_sublist l).subset

Premises used: List.Sublist.subset, List.tail_sublist
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
a : α
h : a ∈ l.dropLast
⊢ a ∈ l

Tactic:
dropLast_subset l h

Premises used: List.dropLast_subset
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
h₁ : x ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y
⊢ x ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] <+: y

Tactic:
use y.drop (x.length + 1)

Premises used: List.drop, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
h₁ : take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y
⊢ x ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y

Tactic:
nth_rw 1 [List.prefix_iff_eq_take.mp h]

Premises used: List.prefix_iff_eq_take, Iff.mp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take (x.length + 1) y ++ drop (x.length + 1) y = y

Tactic:
List.take_append_drop (x.length + 1) y

Premises used: List.take_append_drop, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
h₁ : take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] = take (x.length + 1) y
⊢ take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y

Tactic:
convert! List.take_append_drop (x.length + 1) y using 2

Premises used: List.take_append_drop, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
h₁ :
  take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] =
    take x.length y ++ [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y x.length hl]
h₂ : x.length < y.length
⊢ take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] = take (x.length + 1) y

Tactic:
rw [← List.take_concat_get, List.concat_eq_append]

Premises used: List.concat_eq_append, List.take_concat_get
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ : List α
h : l₁ <+: []
⊢ [] = l₁ ++ drop l₁.length []

Tactic:
simp [List.prefix_nil.mp h]

Premises used: List.prefix_nil, Iff.mp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
head : α
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
h : [] <+: head :: tail
⊢ head :: tail = [] ++ drop (length.{u_1} (α := α) []) (head :: tail)

Tactic:
rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
head : α
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
head_1 : α
tail_1 : List α
h : head_1 :: tail_1 <+: head :: tail
cons :
  ∀ (h' : tail_1 <+: tail) (h : head_1 :: tail_1 <+: head_1 :: tail),
    head_1 :: tail = head_1 :: tail_1 ++ drop (head_1 :: tail_1).length (head_1 :: tail)
⊢ head :: tail = head_1 :: tail_1 ++ drop (head_1 :: tail_1).length (head :: tail)

Tactic:
obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h

Premises used: List.cons_prefix_cons, Iff.mp, rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
head : α
tail_1 : List α
h' : tail_1 <+: tail
h : head :: tail_1 <+: head :: tail
⊢ head :: tail = head :: tail_1 ++ drop (head :: tail_1).length (head :: tail)

Tactic:
simpa using ih h'
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
head : α
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
l₁ : List α
h : l₁ <+: head :: tail
cons : ∀ (h : [] <+: head :: tail), head :: tail = [] ++ drop (length.{u_1} (α := α) []) (head :: tail)
cons₁ :
  ∀ (head_1 : α) (tail_1 : List α) (h : head_1 :: tail_1 <+: head :: tail),
    head :: tail = head_1 :: tail_1 ++ drop (head_1 :: tail_1).length (head :: tail)
⊢ head :: tail = l₁ ++ drop l₁.length (head :: tail)

Tactic:
cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

Premises used: List.cons, rfl, List.nil
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
nil : ∀ {l₁ : List α} (h : l₁ <+: []), [] = l₁ ++ drop l₁.length []
cons :
  ∀ (head : α) (tail : List α) (ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail) {l₁ : List α}
    (h : l₁ <+: head :: tail), head :: tail = l₁ ++ drop l₁.length (head :: tail)
⊢ l₂ = l₁ ++ drop l₁.length l₂

Tactic:
induction l₂ generalizing l₁ with
  | nil => simp [List.prefix_nil.mp h]
  | cons _ _ ih =>
    cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

Premises used: List.prefix_nil, List.cons, Iff.mp, rfl, List.nil
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
β : Type u_2
l l₁_1 l₂ l₃ : List α
a_1 b : α
inst : DecidableEq α
a : α
l₁ : List α
h : a :: l₁ <:+: []
s t : List α
te : s ++ a :: l₁ ++ t = []
⊢ False

Tactic:
simp at te
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List (Option α)
h : l₁ <+: l₂
⊢ l₁.reduceOption <+: l₂.reduceOption

Tactic:
h.filterMap id

Premises used: id, List.IsPrefix.filterMap
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x : α
xs : List α
rw : (∃ (s : List α), ∃ (t : List α), s ++ [x] ++ t = xs) ↔ ∃ (s : List α), ∃ (t : List α), xs = s ++ x :: t
⊢ [x] <:+: xs ↔ x ∈ xs

Tactic:
rw [List.mem_iff_append, List.IsInfix]

Premises used: List.IsInfix, List.mem_iff_append
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x : α
xs : List α
a : ∀ (x_1 x_2 : List α), x_1 ++ [x] ++ x_2 = xs ↔ xs = x_1 ++ x :: x_2
⊢ (∃ (s : List α), ∃ (t : List α), s ++ [x] ++ t = xs) ↔ ∃ (s : List α), ∃ (t : List α), xs = s ++ x :: t

Tactic:
congr! 4
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x : α
xs x_1 x_2 : List α
⊢ x_1 ++ [x] ++ x_2 = xs ↔ xs = x_1 ++ x :: x_2

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : α
mp : [x] <:+: [y] → x = y
mpr : x = y → [x] <:+: [y]
⊢ [x] <:+: [y] ↔ x = y

Tactic:
constructor
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y : α
bs : List α
h : [] ++ [x] ++ bs = [y]
⊢ x = y

Tactic:
simp_all
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x y head : α
tail bs : List α
h : head :: tail ++ [x] ++ bs = [y]
⊢ x = y

Tactic:
simp_all
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x : α
⊢ [x] <:+: [x]

Tactic:
rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x : α
⊢ [] <:+: [x] ↔ Eq.{u_1 + 1} (α := List α) [] [] ∨ [] = [x]

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x head : α
⊢ [head] <:+: [x] ↔ [head] = [] ∨ [head] = [x]

Tactic:
simp [List.singleton_infix_singleton_iff]

Premises used: List.singleton_infix_singleton_iff
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x head head_1 : α
tail : List α
mp : head :: head_1 :: tail <:+: [x] → head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]
mpr : head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x] → head :: head_1 :: tail <:+: [x]
⊢ head :: head_1 :: tail <:+: [x] ↔ head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]

Tactic:
constructor
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x head head_1 : α
tail w : List α
h : [] ++ head :: head_1 :: tail ++ w = [x]
⊢ head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]

Tactic:
simp at h
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x head head_1 : α
tail : List α
head_2 : α
tail_1 w : List α
h : head_2 :: tail_1 ++ head :: head_1 :: tail ++ w = [x]
⊢ head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]

Tactic:
simp at h
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x head head_1 : α
tail : List α
⊢ head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x] → head :: head_1 :: tail <:+: [x]

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
xs : List α
x : α
⊢ xs <:+: [x] ↔ xs = [] ∨ xs = [x]

Tactic:
match xs with
  | [] => simp
  | [_] => simp [List.singleton_infix_singleton_iff]
  | _ :: _ :: _ =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₁
⊢ l₁ = l₂

Tactic:
h₁.sublist.antisymm h₂.sublist

Premises used: List.Sublist.antisymm, List.IsInfix.sublist
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
hn : l₂.Nodup
⊢ l₁.Nodup

Tactic:
hn.sublist h.sublist

Premises used: List.Nodup.sublist, List.IsPrefix.sublist
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
hn : l₂.Nodup
⊢ l₁.Nodup

Tactic:
hn.sublist h.sublist

Premises used: List.Nodup.sublist, List.IsInfix.sublist
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+ l₂
hn : l₂.Nodup
⊢ l₁.Nodup

Tactic:
hn.sublist h.sublist

Premises used: List.Nodup.sublist, List.IsSuffix.sublist
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s : List α
this : s = [] ↔ s <+: []
⊢ Membership.mem (γ := List (List α)) (inits []) s ↔ s <+: []

Tactic:
simpa only [inits, mem_singleton]

Premises used: List.mem_singleton, List.inits
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
o : s_1 = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s_1
s r : List α
hr : r ∈ t.inits
hs : a :: r = s
let : ∀ (s_2 : List α) (ht : r ++ s_2 = t), s <+: a :: t
⊢ s <+: a :: t

Tactic:
let ⟨s, ht⟩ := (mem_inits _ _).1 hr
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
o : s_1 = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s_1
s_2 r : List α
hr : r ∈ t.inits
hs : a :: r = s_2
s : List α
ht : r ++ s = t
rw : a :: r <+: a :: (r ++ s)
⊢ s_2 <+: a :: t

Tactic:
rw [← hs, ← ht]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
o : s_1 = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s_1
s_2 r : List α
hr : r ∈ t.inits
hs : a :: r = s_2
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)

Tactic:
⟨s, rfl⟩

Premises used: List.IsPrefix, Exists.intro, rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
o : s_1 = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s_1
s_2 r : List α
hr : r ∈ t.inits
hs : a :: r = s_2
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)

Tactic:
exact ⟨s, rfl⟩
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
mi : s_1 <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
rw : ∃ (l : List α), l ∈ t.inits ∧ a :: l = a :: s
⊢ ∃ (l : List α), l ∈ t.inits ∧ a :: l = b :: s

Tactic:
rw [eq_of_heq ba]

Premises used: eq_of_heq
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
mi : s_1 <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ (l : List α), l ∈ t.inits ∧ a :: l = a :: s

Tactic:
⟨_, (mem_inits _ _).2 ⟨_, eq_of_heq st⟩, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, eq_of_heq, rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
mi : s_1 <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ (l : List α), l ∈ t.inits ∧ a :: l = a :: s

Tactic:
exact ⟨_, (mem_inits _ _).2 ⟨_, eq_of_heq st⟩, rfl⟩
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s : List α
a : α
t : List α
this : (s = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s) ↔ s <+: a :: t
⊢ s ∈ (a :: t).inits ↔ s <+: a :: t

Tactic:
simpa
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s : List α
⊢ Membership.mem (γ := List (List α)) (tails []) s ↔ s <:+ []

Tactic:
simp only [tails, mem_singleton, suffix_nil]

Premises used: List.mem_singleton, List.tails, List.suffix_nil
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s : List α
a : α
t : List α
simp : s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
⊢ s ∈ (a :: t).tails ↔ s <:+ a :: t

Tactic:
simp only [tails, mem_cons, mem_tails s t]

Premises used: List.mem_cons, List.tails
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t

Tactic:
show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
        ⟨fun o =>
          match s, t, o with
          | _, t, Or.inl rfl => suffix_rfl
          | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
          fun e =>
          match s, t, e with
          | _, t, ⟨[], rfl⟩ => Or.inl rfl
          | s, t, ⟨b :: l, he⟩ =>
            List.noConfusion rfl (heq_of_eq he) fun _ lt => Or.inr ⟨l, eq_of_heq lt⟩⟩

Premises used: _private.0.List.mem_tails.match_3, List.suffix_rfl, List.cons, heq_of_eq, Iff.intro, Exists.intro, List.IsSuffix, List.noConfusion, eq_of_heq, Or.inl, Or, Eq, _private.0.List.mem_tails.match_2, Or.inr, rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t

Tactic:
exact
      show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
        ⟨fun o =>
          match s, t, o with
          | _, t, Or.inl rfl => suffix_rfl
          | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
          fun e =>
          match s, t, e with
          | _, t, ⟨[], rfl⟩ => Or.inl rfl
          | s, t, ⟨b :: l, he⟩ =>
            List.noConfusion rfl (heq_of_eq he) fun _ lt => Or.inr ⟨l, eq_of_heq lt⟩⟩

Premises used: _private.0.List.mem_tails.match_3, List.suffix_rfl, List.cons, heq_of_eq, Iff.intro, Exists.intro, List.IsSuffix, List.noConfusion, eq_of_heq, Or.inl, Or, Eq, _private.0.List.mem_tails.match_2, Or.inr, rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = [] :: map (fun (t : List α) ↦ a :: t) l.inits

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (a :: l) :: l.tails

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
⊢ (HAppend.hAppend (α := List α) [] []).inits =
    HAppend.hAppend (α := List (List α)) (inits []) (map (fun (l : List α) ↦ [] ++ l) (tail (inits [])))

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).inits =
    HAppend.hAppend (α := List (List α)) (inits []) (map (fun (l : List α) ↦ [] ++ l) (a :: t).inits.tail)

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).inits = (a :: s).inits ++ map (fun (l : List α) ↦ a :: s ++ l) t.inits.tail

Tactic:
simp [inits_append s t, Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
⊢ (HAppend.hAppend (α := List α) [] []).tails =
    HAppend.hAppend (α := List (List α)) (map (fun (l : List α) ↦ l ++ []) (tails [])) (tail (tails []))

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).tails = map (fun (l : List α) ↦ l ++ a :: t) (tails []) ++ (a :: t).tails.tail

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).tails = map (fun (l : List α) ↦ l ++ t) (a :: s).tails ++ t.tails.tail

Tactic:
simp [tails_append s t]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (List α)) (inits []) (reverse (map reverse (tails (reverse []))))

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = (map reverse (a :: l).reverse.tails).reverse

Tactic:
simp [inits_eq_tails l, map_inj_left, ← map_reverse]

Premises used: List.map_inj_left, List.map_reverse
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (List α)) (tails []) (reverse (map reverse (inits (reverse []))))

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (map reverse (a :: l).reverse.inits).reverse

Tactic:
simp [tails_eq_inits l]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
rw : l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse
⊢ l.reverse.inits = (map reverse l.tails).reverse

Tactic:
rw [tails_eq_inits l]

Premises used: List.tails_eq_inits
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse

Tactic:
simp [← map_reverse]

Premises used: List.map_reverse
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
rw : l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse
⊢ l.reverse.tails = (map reverse l.inits).reverse

Tactic:
rw [inits_eq_tails l]

Premises used: List.inits_eq_tails
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse

Tactic:
simp [← map_reverse]

Premises used: List.map_reverse
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
rw : map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse
⊢ map reverse l.inits = l.reverse.tails.reverse

Tactic:
rw [inits_eq_tails l]

Premises used: List.inits_eq_tails
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse

Tactic:
simp [← map_reverse]

Premises used: List.map_reverse
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
rw : map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
⊢ map reverse l.tails = l.reverse.inits.reverse

Tactic:
rw [tails_eq_inits l]

Premises used: List.tails_eq_inits
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse

Tactic:
simp [← map_reverse]

Premises used: List.map_reverse
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
⊢ length.{u_1} (α := List α) (tails []) = length.{u_1} (α := α) [] + 1

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
x : α
l : List α
IH : l.tails.length = l.length + 1
⊢ (x :: l).tails.length = (x :: l).length + 1

Tactic:
simpa using IH
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
nil : length.{u_1} (α := List α) (tails []) = length.{u_1} (α := α) [] + 1
cons : ∀ (x : α) (l : List α) (IH : l.tails.length = l.length + 1), (x :: l).tails.length = (x :: l).length + 1
⊢ l.tails.length = l.length + 1

Tactic:
induction l with
  | nil => simp
  | cons x l IH => simpa using IH

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
⊢ l.inits.length = l.length + 1

Tactic:
simp [inits_eq_tails]

Premises used: List.inits_eq_tails
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
n : ℕ
h : n < length.{u_1} (α := List α) (tails [])
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tails []) n h = drop n []

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
h : 0 < (a :: l).tails.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails 0 h = drop 0 (a :: l)

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
n : ℕ
h : n + 1 < (a :: l).tails.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails (n + 1) h = drop (n + 1) (a :: l)

Tactic:
simp [ihl]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
n : ℕ
h : n < (a :: l).tails.length
cons :
  ∀ (h : 0 < (a :: l).tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails 0 h = drop 0 (a :: l)
cons₁ :
  ∀ (n : ℕ) (h : n + 1 < (a :: l).tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails (n + 1) h = drop (n + 1) (a :: l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails n h = drop n (a :: l)

Tactic:
cases n with
    | zero => simp
    | succ n => simp [ihl]