Theorem: List.init_prefix (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
l l' : List V
h : l <+: l'
⊢ init l <+: init l'
Tactic:
have h1 : length l ≤ length l' := List.IsPrefix.length_le h
State after:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
⊢ init l <+: init l'

State before:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
⊢ init l <+: init l'
Tactic:
have h2 : length l - 1 ≤ length l' - 1 := Nat.sub_le_sub_right h1 1
State after:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
⊢ init l <+: init l'

State before:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
⊢ init l <+: init l'
Tactic:
have h3 : (length l - 1) ≤ (length l') := h2.trans <| Nat.sub_le (length l') 1
State after:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'

State before:
V : Type u_1
l l' : List V
h : l <+: l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'
Tactic:
rw [List.prefix_iff_eq_take] at h
State after:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'

State before:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init l <+: init l'
Tactic:
rw [h, List.prefix_iff_eq_take]
State after:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init (take (length l) l') = take (length (init (take (length l) l'))) (init l')

State before:
V : Type u_1
l l' : List V
h : l = take (length l) l'
h1 : length l ≤ length l'
h2 : length l - 1 ≤ length l' - 1
h3 : length l - 1 ≤ length l'
⊢ init (take (length l) l') = take (length (init (take (length l) l'))) (init l')
Tactic:
simp [init, h1, List.take_take, List.take_take, min_eq_left h3, min_eq_left h2]
State after:
no goals