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 as bs ++ cs
Tactic:
induction as generalizing bs with
| nil => rw [reverseAux, reverseAux]
| cons a as ih => rw [reverseAux, reverseAux, ←cons_append, ih]
State after:
no goals

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

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