Theorem: Vec.toList_ofList_iso (Qpf/Util/Vec.lean)

State before:
α : Type u_1
as : List α
⊢ toList (ofList as) = as
Tactic:
induction as
State after:
case nil
α : Type u_1
⊢ toList (ofList []) = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : toList (ofList tail✝) = tail✝
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝

State before:
α : Type u_1
⊢ toList (ofList []) = []
Tactic:
case nil          => rfl
State after:
no goals

State before:
α : Type u_1
a : α
as : List α
ih : toList (ofList as) = as
⊢ toList (ofList (a :: as)) = a :: as
Tactic:
case cons a as ih =>
  simp only [toList, ofList, append1, last, DVec.last, drop_append1', ih]
State after:
no goals

State before:
α : Type u_1
⊢ toList (ofList []) = []
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
a : α
as : List α
ih : toList (ofList as) = as
⊢ toList (ofList (a :: as)) = a :: as
Tactic:
simp only [toList, ofList, append1, last, DVec.last, drop_append1', ih]
State after:
no goals