Theorem: reverseAux_append (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

State before:
α : Type
as bs cs : List α
a b c : α
⊢ reverseAux (as ++ bs) cs = reverseAux bs (reverseAux as cs)
Tactic:
induction as generalizing cs with
| nil => rw [nil_append, reverseAux]
| cons a as ih => rw [cons_append, reverseAux, reverseAux, ih]
State after:
no goals

State before:
case nil
α : Type
bs : List α
a b c : α
cs : List α
⊢ reverseAux ([] ++ bs) cs = reverseAux bs (reverseAux [] cs)
Tactic:
rw [nil_append, reverseAux]
State after:
no goals

State before:
case cons
α : Type
bs : List α
a✝ b c a : α
as : List α
ih : ∀ (cs : List α), reverseAux (as ++ bs) cs = reverseAux bs (reverseAux as cs)
cs : List α
⊢ reverseAux (a :: as ++ bs) cs = reverseAux bs (reverseAux (a :: as) cs)
Tactic:
rw [cons_append, reverseAux, reverseAux, ih]
State after:
no goals