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