Theorem: List.reverseAux_spec (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
xs acc : List α
⊢ reverseAux xs acc = reverse xs ++ acc
Tactic:
induction xs generalizing acc with
| nil => simp [reverse, reverseAux]
| cons x xs ih =>
  simp only [reverse, reverseAux]
  simp only [ih]
  rw [←singleton_append, append_assoc]
State after:
no goals

State before:
case nil
α : Type u_1
acc : List α
⊢ reverseAux [] acc = reverse [] ++ acc
Tactic:
simp [reverse, reverseAux]
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux (x :: xs) acc = reverse (x :: xs) ++ acc
Tactic:
simp only [reverse, reverseAux]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux xs (x :: acc) = reverseAux xs [x] ++ acc

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux xs (x :: acc) = reverseAux xs [x] ++ acc
Tactic:
simp only [ih]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverse xs ++ x :: acc = reverse xs ++ [x] ++ acc

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverse xs ++ x :: acc = reverse xs ++ [x] ++ acc
Tactic:
rw [←singleton_append, append_assoc]
State after:
no goals