Theorem: List.reverseAux_append_left (Algdata/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
γ : Type w
as₁ as₂ bs : List α
⊢ reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
Tactic:
revert bs
State after:
α : Type u
β : Type v
γ : Type w
as₁ as₂ : List α
⊢ ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs

State before:
α : Type u
β : Type v
γ : Type w
as₁ as₂ : List α
⊢ ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
Tactic:
induction as₁ <;> intro bs
State after:
case nil
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs

case cons
α : Type u
β : Type v
γ : Type w
as₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {bs : List α}, reverseAux (tail✝ ++ as₂) bs = reverse as₂ ++ reverseAux tail✝ bs
bs : List α
⊢ reverseAux (head✝ :: tail✝ ++ as₂) bs = reverse as₂ ++ reverseAux (head✝ :: tail✝) bs

State before:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs
Tactic:
case nil => rw [reverseAux_eq_append]; rfl
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: as₁ ++ as₂) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Tactic:
case cons a₁ as₁ h_ind =>
  rw [cons_append]
  unfold reverseAux
  rw [h_ind]
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs
Tactic:
rw [reverseAux_eq_append]
State after:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) [] ++ bs = reverse as₂ ++ reverseAux [] bs

State before:
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) [] ++ bs = reverse as₂ ++ reverseAux [] bs
Tactic:
rfl
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: as₁ ++ as₂) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Tactic:
rw [cons_append]
State after:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: (as₁ ++ as₂)) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs

State before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: (as₁ ++ as₂)) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
Tactic:
unfold reverseAux
State after:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (as₁ ++ as₂) (a₁ :: bs) = reverse as₂ ++ reverseAux as₁ (a₁ :: bs)

State before:
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (as₁ ++ as₂) (a₁ :: bs) = reverse as₂ ++ reverseAux as₁ (a₁ :: bs)
Tactic:
rw [h_ind]
State after:
no goals