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

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
as : List α
⊢ mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
Tactic:
induction as
State after:
case nil
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])

case cons
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  mapF.compositorOplax F G tail✝ ≫ mapF.compositorLax F G tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor tail✝)
⊢ mapF.compositorOplax F G (head✝ :: tail✝) ≫ mapF.compositorLax F G (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor (head✝ :: tail✝))

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ mapF.compositorOplax F G (a :: as) ≫ mapF.compositorLax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
dsimp [mapF.compositorLax, mapF.compositorOplax]
rw [h_ind, Category.id_comp]
State after:
no goals

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ mapF.compositorOplax F G (a :: as) ≫ mapF.compositorLax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor (a :: as))
Tactic:
dsimp [mapF.compositorLax, mapF.compositorOplax]
State after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorOplax F G as ≫ mapF.compositorLax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as))

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorOplax F G as ≫ mapF.compositorLax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as))
Tactic:
rw [h_ind, Category.id_comp]
State after:
no goals