Theorem: CategoryTheory.List.appendF.naturator_oplax_lax (Moncalc/CategoryTheory/List/Monad.lean)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List α
⊢ appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
Tactic:
induction as₁
State after:
case nil
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
⊢ appendF.naturatorOplax F [] as₂ ≫ appendF.naturatorLax F [] as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor ([] ++ as₂))

case cons
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  appendF.naturatorOplax F tail✝ as₂ ≫ appendF.naturatorLax F tail✝ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (tail✝ ++ as₂))
⊢ appendF.naturatorOplax F (head✝ :: tail✝) as₂ ≫ appendF.naturatorLax F (head✝ :: tail✝) as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (head✝ :: tail✝ ++ as₂))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
⊢ appendF.naturatorOplax F [] as₂ ≫ appendF.naturatorLax F [] as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor ([] ++ as₂))
Tactic:
case nil =>
  dsimp [appendF.naturatorLax, appendF.naturatorOplax]
  rw [Category.id_comp]
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ appendF.naturatorOplax F (a :: as₁) as₂ ≫ appendF.naturatorLax F (a :: as₁) as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a :: as₁ ++ as₂))
Tactic:
case cons a as₁ h_ind =>
  dsimp [appendF.naturatorLax, appendF.naturatorOplax]
  rw [Category.id_comp]
  rw [h_ind]
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
⊢ appendF.naturatorOplax F [] as₂ ≫ appendF.naturatorLax F [] as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor ([] ++ as₂))
Tactic:
dsimp [appendF.naturatorLax, appendF.naturatorOplax]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
⊢ 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) ≫
      𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
⊢ 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) ≫
      𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)
Tactic:
rw [Category.id_comp]
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ appendF.naturatorOplax F (a :: as₁) as₂ ≫ appendF.naturatorLax F (a :: as₁) as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a :: as₁ ++ as₂))
Tactic:
dsimp [appendF.naturatorLax, appendF.naturatorOplax]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a) ≫ 𝟙 (Prefunctor.obj F.toPrefunctor a))
      (appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂)))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a) ≫ 𝟙 (Prefunctor.obj F.toPrefunctor a))
      (appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂)))
Tactic:
rw [Category.id_comp]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂)))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂)))
Tactic:
rw [h_ind]
State after:
no goals