Theorem: List.isInfix_take_of_isInfix_append (One.lean)

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have ⟨s,t,ih⟩ := h
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have hl: s.length + l₁.length + t.length = l₂.length + l₃.length := by
  apply_fun @List.length α at ih
  simp only [List.length_append] at ih
  exact ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have l₁split := List.take_append_drop (length l₁ - length l₃) l₁
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
rw [←l₁split] at ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
apply_fun List.take (length l₂) at ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) (s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t) =
    take (length l₂) (l₂ ++ l₃)
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) (s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t) =
    take (length l₂) (l₂ ++ l₃)
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
simp only [List.take_append_eq_append_take, List.take_take, List.length_take, length_drop, length_append,
  take_length, Nat.sub_self, take_zero, append_nil, Nat.min_self_sub_left] at ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have l2len : l₂.length = s.length + l₁.length + t.length - l₃.length := by
  apply Eq.symm
  rw [Nat.sub_eq_of_eq_add]
  exact hl
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
rw [l2len, min_eq_right] at ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (length l₁ - length l₃) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (length l₁ - length l₃) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s
Tactic:
. rw [← ih]
  apply List.isInfix_append_right_of_isInfix
  apply List.isInfix_append_left_of_isInfix
  apply List.isInfix_append_right_of_isInfix
  apply List.isInfix_self
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s
Tactic:
. rw [Nat.sub_sub, add_comm l₃.length, ← Nat.sub_sub, add_assoc, add_comm, Nat.add_sub_cancel, add_comm]
  simp only [Nat.sub_le_sub_right, le_add_iff_nonneg_left, zero_le]
State after:
no goals

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
apply_fun @List.length α at ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length (s ++ l₁ ++ t) = length (l₂ ++ l₃)
⊢ length s + length l₁ + length t = length l₂ + length l₃

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length (s ++ l₁ ++ t) = length (l₂ ++ l₃)
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
simp only [List.length_append] at ih
State after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length s + length l₁ + length t = length l₂ + length l₃
⊢ length s + length l₁ + length t = length l₂ + length l₃

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length s + length l₁ + length t = length l₂ + length l₃
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
exact ih
State after:
no goals

State before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length l₂ = length s + length l₁ + length t - length l₃
Tactic:
apply Eq.symm
State after:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t - length l₃ = length l₂

State before:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t - length l₃ = length l₂
Tactic:
rw [Nat.sub_eq_of_eq_add]
State after:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t = length l₂ + length l₃

State before:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
exact hl
State after:
no goals