Theorem: append_assoc' (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

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

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

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