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

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

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

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorLax F as₁ as₂ ≫ appendF.naturatorOplax F as₁ as₂ =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₁ ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)
⊢ appendF.naturatorLax F (a :: as₁) as₂ ≫ appendF.naturatorOplax F (a :: as₁) as₂ =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a :: as₁) ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor 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.naturatorLax F [] as₂ ≫ appendF.naturatorOplax F [] as₂ =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor [] ++
        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 [] ++
        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 [] ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)
Tactic:
rw [Category.id_comp (X:=(mapF.obj F).obj as₂)]
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 [] ++
        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 [] ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)
Tactic:
rfl
State after:
no goals

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