Theorem: CategoryTheory.List.mapF.unitor_oplax_lax (Moncalc/CategoryTheory/List/Functor.lean)

State before:
α : Type u
inst✝ : Category α
as : List α
⊢ mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
Tactic:
induction as
State after:
case nil
α : Type u
inst✝ : Category α
⊢ mapF.unitorOplax [] ≫ mapF.unitorLax [] = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor [])

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ :
  mapF.unitorOplax tail✝ ≫ mapF.unitorLax tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor tail✝)
⊢ mapF.unitorOplax (head✝ :: tail✝) ≫ mapF.unitorLax (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor (head✝ :: tail✝))

State before:
α : Type u
inst✝ : Category α
⊢ mapF.unitorOplax [] ≫ mapF.unitorLax [] = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor [])
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ mapF.unitorOplax (a :: as) ≫ mapF.unitorLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [mapF.unitorLax, mapF.unitorOplax, List.id, DVect2.fromList]
  rw [h_ind, Category.id_comp]
State after:
no goals

State before:
α : Type u
inst✝ : Category α
⊢ mapF.unitorOplax [] ≫ mapF.unitorLax [] = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor [])
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ mapF.unitorOplax (a :: as) ≫ mapF.unitorLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor (a :: as))
Tactic:
dsimp [mapF.unitorLax, mapF.unitorOplax, List.id, DVect2.fromList]
State after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorOplax as ≫ mapF.unitorLax as) =
    DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as))

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorOplax as ≫ mapF.unitorLax as) =
    DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as))
Tactic:
rw [h_ind, Category.id_comp]
State after:
no goals