no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
⊢ reverse (as ++ bs) = reverse bs ++ reverse as
induction as generalizing bs with
| nil => simp
| cons a as ih => simp [ih]; rw [append_assoc]
no goals
case nil
α : Type u
β : Type v
γ : Type w
bs : List α
⊢ reverse (nil ++ bs) = reverse bs ++ reverse nil
simp
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (bs : List α), reverse (as ++ bs) = reverse bs ++ reverse as
bs : List α
⊢ reverse bs ++ reverse as ++ a :: nil = reverse bs ++ (reverse as ++ a :: nil)
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (bs : List α), reverse (as ++ bs) = reverse bs ++ reverse as
bs : List α
⊢ reverse (a :: as ++ bs) = reverse bs ++ reverse (a :: as)
simp [ih]
no goals
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (bs : List α), reverse (as ++ bs) = reverse bs ++ reverse as
bs : List α
⊢ reverse bs ++ reverse as ++ a :: nil = reverse bs ++ (reverse as ++ a :: nil)
rw [append_assoc]