Theorem: list_prefix_leq_length (Katydid/Std/Lists.lean)

State before:
α : Type u_1
xs ys zs : List α
⊢ xs = ys ++ zs → length ys ≤ length xs
Tactic:
intro xsyszs
State after:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
⊢ length ys ≤ length xs

State before:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
⊢ length ys ≤ length xs
Tactic:
have h := list_split_list xs (length ys) ys zs rfl xsyszs
State after:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
h : ys = take (length ys) xs ∧ zs = drop (length ys) xs
⊢ length ys ≤ length xs

State before:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
h : ys = take (length ys) xs ∧ zs = drop (length ys) xs
⊢ length ys ≤ length xs
Tactic:
cases h with
| intro hys hzs =>
  rw [hzs] at xsyszs
  rw [xsyszs]
  rw [list_length_split]
  linarith
State after:
no goals

State before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length xs
Tactic:
rw [hzs] at xsyszs
State after:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length xs

State before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length xs
Tactic:
rw [xsyszs]
State after:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length (ys ++ drop (length ys) xs)

State before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length (ys ++ drop (length ys) xs)
Tactic:
rw [list_length_split]
State after:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length ys + length (drop (length ys) xs)

State before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length ys + length (drop (length ys) xs)
Tactic:
linarith
State after:
no goals