Theorem: CategoryTheory.List.appendF.map_id (Moncalc/CategoryTheory/List/Basic.lean)

State before:
α : Type u
inst✝ : Category α
as bs : List α
⊢ 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
Tactic:
induction as
State after:
case nil
α : Type u
inst✝ : Category α
bs : List α
⊢ 𝟙 [] ++ 𝟙 bs = 𝟙 ([] ++ bs)

case cons
α : Type u
inst✝ : Category α
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : 𝟙 tail✝ ++ 𝟙 bs = 𝟙 (tail✝ ++ bs)
⊢ 𝟙 (head✝ :: tail✝) ++ 𝟙 bs = 𝟙 (head✝ :: tail✝ ++ bs)

State before:
α : Type u
inst✝ : Category α
bs : List α
⊢ 𝟙 [] ++ 𝟙 bs = 𝟙 ([] ++ bs)
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ 𝟙 (a :: as) ++ 𝟙 bs = 𝟙 (a :: as ++ bs)
Tactic:
case cons a as h_ind =>
  dsimp
  rw [DVect2.cons_append, h_ind]
State after:
no goals

State before:
α : Type u
inst✝ : Category α
bs : List α
⊢ 𝟙 [] ++ 𝟙 bs = 𝟙 ([] ++ bs)
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ 𝟙 (a :: as) ++ 𝟙 bs = 𝟙 (a :: as ++ bs)
Tactic:
dsimp
State after:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ DVect2.cons (𝟙 a) (𝟙 as) ++ 𝟙 bs = DVect2.cons (𝟙 a) (𝟙 (as ++ bs))

State before:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ DVect2.cons (𝟙 a) (𝟙 as) ++ 𝟙 bs = DVect2.cons (𝟙 a) (𝟙 (as ++ bs))
Tactic:
rw [DVect2.cons_append, h_ind]
State after:
no goals