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

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
as : List α
⊢ mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor 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.compositorLax F G [] ≫ mapF.compositorOplax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor [])

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

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

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorLax F G [] ≫ mapF.compositorOplax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor 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.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ mapF.compositorLax F G (a :: as) ≫ mapF.compositorOplax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor 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.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorLax F G as ≫ mapF.compositorOplax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))

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

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