[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ l <+: concat l a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m✝ n✝ n m : ℕ
l : List α
⊢ dropSlice n m l = take n l ++ drop m (drop n l)
[PROOFSTEP]
rw [dropSlice_eq, drop_drop, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ dropLast [] ++ [] = []
[PROOFSTEP]
rw [dropLast, List.append_nil]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tail l <:+ l
[PROOFSTEP]
rw [← drop_one]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ drop 1 l <:+ l
[PROOFSTEP]
apply drop_suffix
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ l₁ <+: l₂ → l₁ ++ drop (length l₁) l₂ = l₂
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ l₁ ++ drop (length l₁) (l₁ ++ r) = l₁ ++ r
[PROOFSTEP]
rw [drop_left]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ l₁ <:+ l₂ → take (length l₂ - length l₁) l₂ ++ l₁ = l₂
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
l l₁ l₃ : List α
a b : α
m n : ℕ
r : List α
⊢ take (length (r ++ l₁) - length l₁) (r ++ l₁) ++ l₁ = r ++ l₁
[PROOFSTEP]
simp only [length_append, add_tsub_cancel_right, take_left]
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂✝ l₃ : List α
a✝ b✝ : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h : a = b
⊢ l₁ <+: l₂ ↔ a :: l₁ <+: b :: l₂
[PROOFSTEP]
rw [← h, prefix_cons_inj]
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂✝ l₃ : List α
a✝ b✝ : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
h : ¬a = b
x✝ : a :: l₁ <+: b :: l₂
t : List α
te : a :: l₁ ++ t = b :: l₂
⊢ a = b
[PROOFSTEP]
injection te
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ ¬length (a :: l₁) ≤ length []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁✝ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l₁ : List α
x✝ : a :: l₁ <:+: []
s t : List α
te : s ++ a :: l₁ ++ t = []
⊢ False
[PROOFSTEP]
simp at te 
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L <+: take n L ↔ m ≤ n
[PROOFSTEP]
simp only [prefix_iff_eq_take, length_take]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L = take (min m (length L)) (take n L) ↔ m ≤ n
[PROOFSTEP]
induction m generalizing L n with
| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm 
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List (List (Option α))
hm : m < length L
⊢ take m L = take (min m (length L)) (take n L) ↔ m ≤ n
[PROOFSTEP]
induction m generalizing L n with
| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm 
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case zero
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
n : ℕ
L : List (List (Option α))
hm : zero < length L
⊢ take zero L = take (min zero (length L)) (take n L) ↔ zero ≤ n
[PROOFSTEP]

| zero => simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
[GOAL]
case zero
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
n : ℕ
L : List (List (Option α))
hm : zero < length L
⊢ take zero L = take (min zero (length L)) (take n L) ↔ zero ≤ n
[PROOFSTEP]
simp [min_eq_left, eq_self_iff_true, Nat.zero_le, take]
[GOAL]
case succ
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
[PROOFSTEP]

| succ m IH =>
  cases L with
  | nil => exact (not_lt_bot hm).elim
  | cons l ls =>
    cases n with
    | zero =>
      refine' iff_of_false _ (zero_lt_succ _).not_le
      rw [take_zero, take_nil]
      simp only [take]
    | succ n =>
      simp only [length] at hm 
      have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
      simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
      simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
      exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
[PROOFSTEP]
cases L with
| nil => exact (not_lt_bot hm).elim
| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm 
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
L : List (List (Option α))
hm : succ m < length L
⊢ take (succ m) L = take (min (succ m) (length L)) (take n L) ↔ succ m ≤ n
[PROOFSTEP]
cases L with
| nil => exact (not_lt_bot hm).elim
| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm 
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
hm : succ m < length []
⊢ take (succ m) [] = take (min (succ m) (length [])) (take n []) ↔ succ m ≤ n
[PROOFSTEP]

| nil => exact (not_lt_bot hm).elim
[GOAL]
case succ.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
hm : succ m < length []
⊢ take (succ m) [] = take (min (succ m) (length [])) (take n []) ↔ succ m ≤ n
[PROOFSTEP]
exact (not_lt_bot hm).elim
[GOAL]
case succ.cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
[PROOFSTEP]

| cons l ls =>
  cases n with
  | zero =>
    refine' iff_of_false _ (zero_lt_succ _).not_le
    rw [take_zero, take_nil]
    simp only [take]
  | succ n =>
    simp only [length] at hm 
    have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
    simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
    simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
    exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
[PROOFSTEP]
cases n with
| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
| succ n =>
  simp only [length] at hm 
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
n : ℕ
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take n (l :: ls)) ↔ succ m ≤ n
[PROOFSTEP]
cases n with
| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
| succ n =>
  simp only [length] at hm 
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls)) ↔ succ m ≤ zero
[PROOFSTEP]

| zero =>
  refine' iff_of_false _ (zero_lt_succ _).not_le
  rw [take_zero, take_nil]
  simp only [take]
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls)) ↔ succ m ≤ zero
[PROOFSTEP]
refine' iff_of_false _ (zero_lt_succ _).not_le
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take zero (l :: ls))
[PROOFSTEP]
rw [take_zero, take_nil]
[GOAL]
case succ.cons.zero
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
⊢ ¬take (succ m) (l :: ls) = []
[PROOFSTEP]
simp only [take]
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]

| succ n =>
  simp only [length] at hm 
  have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
  simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
  simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
  exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length (l :: ls)
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
simp only [length] at hm 
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
have specializedIH := @IH n ls (Nat.lt_of_succ_lt_succ hm)
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take (min m (length ls)) (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
simp only [le_of_lt (Nat.lt_of_succ_lt_succ hm), min_eq_left] at specializedIH 
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ take (succ m) (l :: ls) = take (min (succ m) (length (l :: ls))) (take (succ n) (l :: ls)) ↔ succ m ≤ succ n
[PROOFSTEP]
simp [le_of_lt hm, specializedIH, true_and_iff, min_eq_left, eq_self_iff_true, length, take]
[GOAL]
case succ.cons.succ
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m : ℕ
IH : ∀ {n : ℕ} {L : List (List (Option α))}, m < length L → (take m L = take (min m (length L)) (take n L) ↔ m ≤ n)
l : List (Option α)
ls : List (List (Option α))
hm : succ m < length ls + 1
n : ℕ
specializedIH : take m ls = take m (take n ls) ↔ m ≤ n
⊢ m ≤ n ↔ succ m ≤ succ n
[PROOFSTEP]
exact ⟨Nat.succ_le_succ, Nat.le_of_succ_le_succ⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+: b :: l₂ → a = b ∧ l₁ <+: l₂
[PROOFSTEP]
rintro ⟨L, hL⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: l₁ ++ L = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
simp only [cons_append] at hL 
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hL : a :: (l₁ ++ L) = b :: l₂
⊢ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
injection hL with hLLeft hLRight
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
L : List α
hLLeft : a = b
hLRight : l₁ ++ L = l₂
⊢ a = b ∧ l₁ <+: l₂
[PROOFSTEP]
exact ⟨hLLeft, ⟨L, hLRight⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ a = b ∧ l₁ <+: l₂ → a :: l₁ <+: b :: l₂
[PROOFSTEP]
rintro ⟨rfl, h⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a : α
m n : ℕ
h : l₁ <+: l₂
⊢ a :: l₁ <+: a :: l₂
[PROOFSTEP]
rwa [prefix_cons_inj]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h : l₁ <+: l₂
f : α → β
⊢ List.map f l₁ <+: List.map f l₂
[PROOFSTEP]
induction' l₁ with hd tl hl generalizing l₂
[GOAL]
case nil
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
l₂ : List α
h : [] <+: l₂
⊢ List.map f [] <+: List.map f l₂
[PROOFSTEP]
simp only [nil_prefix, map_nil]
[GOAL]
case cons
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
l₂ : List α
h : hd :: tl <+: l₂
⊢ List.map f (hd :: tl) <+: List.map f l₂
[PROOFSTEP]
cases' l₂ with hd₂ tl₂
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
h : hd :: tl <+: []
⊢ List.map f (hd :: tl) <+: List.map f []
[PROOFSTEP]
simpa only using eq_nil_of_prefix_nil h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd :: tl <+: hd₂ :: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
[PROOFSTEP]
rw [cons_prefix_iff] at h 
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd = hd₂ ∧ tl <+: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
[PROOFSTEP]
simp only [List.map_cons, h, prefix_cons_inj, hl, map]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h : l₁ <+: l₂
f : α → Option β
⊢ filterMap f l₁ <+: filterMap f l₂
[PROOFSTEP]
induction' l₁ with hd₁ tl₁ hl generalizing l₂
[GOAL]
case nil
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → Option β
l₂ : List α
h : [] <+: l₂
⊢ filterMap f [] <+: filterMap f l₂
[PROOFSTEP]
simp only [nil_prefix, filterMap_nil]
[GOAL]
case cons
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
l₂ : List α
h : hd₁ :: tl₁ <+: l₂
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f l₂
[PROOFSTEP]
cases' l₂ with hd₂ tl₂
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
h : hd₁ :: tl₁ <+: []
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f []
[PROOFSTEP]
simpa only using eq_nil_of_prefix_nil h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
hd₂ : α
tl₂ : List α
h : hd₁ :: tl₁ <+: hd₂ :: tl₂
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f (hd₂ :: tl₂)
[PROOFSTEP]
rw [cons_prefix_iff] at h 
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
hd₂ : α
tl₂ : List α
h : hd₁ = hd₂ ∧ tl₁ <+: tl₂
⊢ filterMap f (hd₁ :: tl₁) <+: filterMap f (hd₂ :: tl₂)
[PROOFSTEP]
rw [← @singleton_append _ hd₁ _, ← @singleton_append _ hd₂ _, filterMap_append, filterMap_append, h.left,
  prefix_append_right_inj]
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → Option β
hd₁ : α
tl₁ : List α
hl : ∀ {l₂ : List α}, tl₁ <+: l₂ → filterMap f tl₁ <+: filterMap f l₂
hd₂ : α
tl₂ : List α
h : hd₁ = hd₂ ∧ tl₁ <+: tl₂
⊢ filterMap f tl₁ <+: filterMap f tl₂
[PROOFSTEP]
exact hl h.right
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
s : List α
this : s = [] ↔ s <+: []
⊢ s ∈ inits [] ↔ s <+: []
[PROOFSTEP]
simpa only [inits, mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝ : List α
a : α
t : List α
o : s✝ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝
s r : List α
hr : r ∈ inits t
hs : a :: r = s
⊢ s <+: a :: t
[PROOFSTEP]
let ⟨s, ht⟩ := (mem_inits _ _).1 hr
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t
[PROOFSTEP]
rw [← hs, ← ht]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)
[PROOFSTEP]
exact ⟨s, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = b :: s
[PROOFSTEP]
rw [ba]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = a :: s
[PROOFSTEP]
exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
this : (s = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s) ↔ s <+: a :: t
⊢ s ∈ inits (a :: t) ↔ s <+: a :: t
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
s : List α
⊢ s ∈ tails [] ↔ s <:+ []
[PROOFSTEP]
simp only [tails, mem_singleton, suffix_nil]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s ∈ tails (a :: t) ↔ s <:+ a :: t
[PROOFSTEP]
simp only [tails, mem_cons, mem_tails s t]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
[PROOFSTEP]
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 he fun _ lt => Or.inr ⟨l, lt⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ inits (a :: l) = [] :: map (fun t => a :: t) (inits l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ tails (a :: l) = (a :: l) :: tails l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ inits ([] ++ []) = inits [] ++ map (fun l => [] ++ l) (tail (inits []))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
t : List α
⊢ inits ([] ++ a :: t) = inits [] ++ map (fun l => [] ++ l) (tail (inits (a :: t)))
[PROOFSTEP]
simp [· ∘ ·]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
s t : List α
⊢ inits (a :: s ++ t) = inits (a :: s) ++ map (fun l => a :: s ++ l) (tail (inits t))
[PROOFSTEP]
simp [inits_append s t, · ∘ ·]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ tails ([] ++ []) = map (fun l => l ++ []) (tails []) ++ tail (tails [])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
t : List α
⊢ tails ([] ++ a :: t) = map (fun l => l ++ a :: t) (tails []) ++ tail (tails (a :: t))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
s t : List α
⊢ tails (a :: s ++ t) = map (fun l => l ++ t) (tails (a :: s)) ++ tail (tails t)
[PROOFSTEP]
simp [tails_append s t]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ inits [] = reverse (map reverse (tails (reverse [])))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ inits (a :: l) = reverse (map reverse (tails (reverse (a :: l))))
[PROOFSTEP]
simp [inits_eq_tails l, map_eq_map_iff, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ tails [] = reverse (map reverse (inits (reverse [])))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ tails (a :: l) = reverse (map reverse (inits (reverse (a :: l))))
[PROOFSTEP]
simp [tails_eq_inits l, append_left_inj]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ inits (reverse l) = reverse (map reverse (tails l))
[PROOFSTEP]
rw [tails_eq_inits l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ inits (reverse l) = reverse (map reverse (reverse (map reverse (inits (reverse l)))))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (inits l))
[PROOFSTEP]
rw [inits_eq_tails l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ tails (reverse l) = reverse (map reverse (reverse (map reverse (tails (reverse l)))))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (inits l) = reverse (tails (reverse l))
[PROOFSTEP]
rw [inits_eq_tails l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (reverse (map reverse (tails (reverse l)))) = reverse (tails (reverse l))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (tails l) = reverse (inits (reverse l))
[PROOFSTEP]
rw [tails_eq_inits l]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ map reverse (reverse (map reverse (inits (reverse l)))) = reverse (inits (reverse l))
[PROOFSTEP]
simp [reverse_involutive.comp_self, reverse_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ length (tails l) = length l + 1
[PROOFSTEP]
induction' l with x l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ length (tails []) = length [] + 1
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
x : α
l : List α
IH : length (tails l) = length l + 1
⊢ length (tails (x :: l)) = length (x :: l) + 1
[PROOFSTEP]
simpa using IH
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ length (inits l) = length l + 1
[PROOFSTEP]
simp [inits_eq_tails]
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l : List α
n : ℕ
hn : n < length (tails l)
⊢ nthLe (tails l) n hn = drop n l
[PROOFSTEP]
induction' l with x l IH generalizing n
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l)
n : ℕ
hn : n < length (tails [])
⊢ nthLe (tails []) n hn = drop n []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n : ℕ
hn : n < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) n hn = drop n (x :: l)
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
hn : zero < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) zero hn = drop zero (x :: l)
[PROOFSTEP]
simp [nthLe_cons]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n✝ : ℕ
hn : succ n✝ < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) (succ n✝) hn = drop (succ n✝) (x :: l)
[PROOFSTEP]
simpa [nthLe_cons] using IH _ _
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l : List α
n : ℕ
hn : n < length (inits l)
⊢ nthLe (inits l) n hn = take n l
[PROOFSTEP]
induction' l with x l IH generalizing n
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l : List α
n✝ : ℕ
hn✝ : n✝ < length (inits l)
n : ℕ
hn : n < length (inits [])
⊢ nthLe (inits []) n hn = take n []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n✝ : ℕ
hn✝ : n✝ < length (inits l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (inits l)), nthLe (inits l) n hn = take n l
n : ℕ
hn : n < length (inits (x :: l))
⊢ nthLe (inits (x :: l)) n hn = take n (x :: l)
[PROOFSTEP]
cases n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (inits l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (inits l)), nthLe (inits l) n hn = take n l
hn : zero < length (inits (x :: l))
⊢ nthLe (inits (x :: l)) zero hn = take zero (x :: l)
[PROOFSTEP]
simp [nthLe_cons]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (inits l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (inits l)), nthLe (inits l) n hn = take n l
n✝ : ℕ
hn : succ n✝ < length (inits (x :: l))
⊢ nthLe (inits (x :: l)) (succ n✝) hn = take (succ n✝) (x :: l)
[PROOFSTEP]
simpa [nthLe_cons] using IH _ _
[GOAL]
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l
[PROOFSTEP]
by_cases h : a ∈ l
[GOAL]
case pos
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l
[PROOFSTEP]
simp only [insert_of_mem h, insert, suffix_refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l
[PROOFSTEP]
simp only [insert_of_not_mem h, suffix_cons, insert]
