Theorem: List.append_isPrefix_split (One.lean)

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
⊢ s ++ l₁ <+: take n l₂ ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
Tactic:
have ⟨t,heq⟩ := h
State after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ <+: take n l₂ ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ <+: take n l₂ ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
Tactic:
rw [← heq]
State after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
cases hle: decide (length s + length l₁ ≤ n) with
| true =>
  simp only [decide_eq_true_eq] at hle
  left
  exists (take (n-length s - length l₁) t)
  have hle₁ : length s ≤ n := by  calc
    length s ≤  length s + length l₁ := by simp
           _ ≤  n                     := hle
  have hle₂ : length l₁ ≤ (n - length s) := by apply Nat.le_sub_of_add_le; rw [add_comm]; exact hle
  rw [List.take_append_eq_append_take, List.take_append_eq_append_take, List.take_all_of_le hle₁, List.take_all_of_le hle₂]
  simp
  congr 1
  apply Nat.sub_sub
| false =>
  simp only [decide_eq_false_iff_not, not_le] at hle
  right
  rw [List.drop_append_eq_append_drop, List.drop_append_eq_append_drop]
  have heq₁: n + 1 - length l₁ - length s = 0 := by
    rw [Nat.sub_sub, Nat.sub_eq_zero_of_le]
    apply Nat.add_one_le_iff.2
    rw [Nat.add_comm]
    apply hle
  rw [heq₁, drop]
  exists (drop (n + 1 - length l₁ - length (s ++ l₁)) t)
State after:
no goals

State before:
case true
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : decide (length s + length l₁ ≤ n) = true
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
simp only [decide_eq_true_eq] at hle
State after:
case true
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)

State before:
case true
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
left
State after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t)

State before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t)
Tactic:
exists (take (n-length s - length l₁) t)
State after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)

State before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Tactic:
have hle₁ : length s ≤ n := by  calc
  length s ≤  length s + length l₁ := by simp
         _ ≤  n                     := hle
State after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)

State before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Tactic:
have hle₂ : length l₁ ≤ (n - length s) := by apply Nat.le_sub_of_add_le; rw [add_comm]; exact hle
State after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)

State before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Tactic:
rw [List.take_append_eq_append_take, List.take_append_eq_append_take, List.take_all_of_le hle₁, List.take_all_of_le hle₂]
State after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = s ++ l₁ ++ take (n - length (s ++ l₁)) t

State before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = s ++ l₁ ++ take (n - length (s ++ l₁)) t
Tactic:
simp
State after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ take (n - length s - length l₁) t = take (n - (length s + length l₁)) t

State before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ take (n - length s - length l₁) t = take (n - (length s + length l₁)) t
Tactic:
congr 1
State after:
case true.h.e_a
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ n - length s - length l₁ = n - (length s + length l₁)

State before:
case true.h.e_a
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ n - length s - length l₁ = n - (length s + length l₁)
Tactic:
apply Nat.sub_sub
State after:
no goals

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ length s ≤ n
Tactic:
calc
length s ≤  length s + length l₁ := by simp
_ ≤  n                     := hle
State after:
no goals

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ length s ≤ length s + length l₁
Tactic:
simp
State after:
no goals

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length l₁ ≤ n - length s
Tactic:
apply Nat.le_sub_of_add_le
State after:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length l₁ + length s ≤ n

State before:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length l₁ + length s ≤ n
Tactic:
rw [add_comm]
State after:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length s + length l₁ ≤ n

State before:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length s + length l₁ ≤ n
Tactic:
exact hle
State after:
no goals

State before:
case false
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : decide (length s + length l₁ ≤ n) = false
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
simp only [decide_eq_false_iff_not, not_le] at hle
State after:
case false
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)

State before:
case false
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
right
State after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)

State before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
rw [List.drop_append_eq_append_drop, List.drop_append_eq_append_drop]
State after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t

State before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t
Tactic:
have heq₁: n + 1 - length l₁ - length s = 0 := by
  rw [Nat.sub_sub, Nat.sub_eq_zero_of_le]
  apply Nat.add_one_le_iff.2
  rw [Nat.add_comm]
  apply hle
State after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t

State before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t
Tactic:
rw [heq₁, drop]
State after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) s ++ l₁ ++ drop (n + 1 - length l₁ - length (s ++ l₁)) t

State before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) s ++ l₁ ++ drop (n + 1 - length l₁ - length (s ++ l₁)) t
Tactic:
exists (drop (n + 1 - length l₁ - length (s ++ l₁)) t)
State after:
no goals

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n + 1 - length l₁ - length s = 0
Tactic:
rw [Nat.sub_sub, Nat.sub_eq_zero_of_le]
State after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n + 1 ≤ length l₁ + length s

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n + 1 ≤ length l₁ + length s
Tactic:
apply Nat.add_one_le_iff.2
State after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length l₁ + length s

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length l₁ + length s
Tactic:
rw [Nat.add_comm]
State after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length s + length l₁

State before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length s + length l₁
Tactic:
apply hle
State after:
no goals