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

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

case cons
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝² : α
as✝ : List α
b✝ : α
bs✝ : List α
a✝¹ : a✝² ⟶ b✝
a✝ : DVect2 Quiver.Hom as✝ bs✝
a_ih✝ :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a✝ ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a✝ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons a✝¹ a✝ ++ gs) ≫
      appendF.naturatorOplax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorOplax F (a✝² :: as✝) as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons a✝¹ a✝) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)

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

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs) ≫
      appendF.naturatorOplax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorOplax F (a✝ :: as✝) as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
Tactic:
case cons f fs h_ind =>
  dsimp [appendF.naturatorOplax]
  conv =>
    lhs
    rw [DVect2.cons_append]
    dsimp
    rw [Category.comp_id]
  conv =>
    rhs
    rw [DVect2.cons_append]
    dsimp
    rw [Category.id_comp]
  rw [h_ind]
State after:
no goals

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

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs) ≫
      𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs₂) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
Tactic:
rw [Category.comp_id, Category.id_comp]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs) =
    Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs) =
    Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs) ≫
      appendF.naturatorOplax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorOplax F (a✝ :: as✝) as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
Tactic:
dsimp [appendF.naturatorOplax]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs) ≫
      DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor b✝)) (appendF.naturatorOplax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorOplax F as✝ as₂) ≫
      (DVect2.cons (Prefunctor.map F.toPrefunctor f)
          (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs) ≫
      DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor b✝)) (appendF.naturatorOplax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorOplax F as✝ as₂) ≫
      (DVect2.cons (Prefunctor.map F.toPrefunctor f)
          (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
Tactic:
conv =>
  lhs
  rw [DVect2.cons_append]
  dsimp
  rw [Category.comp_id]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorOplax F as✝ as₂) ≫
      (DVect2.cons (Prefunctor.map F.toPrefunctor f)
          (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorOplax F as✝ as₂) ≫
      (DVect2.cons (Prefunctor.map F.toPrefunctor f)
          (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
Tactic:
conv =>
  rhs
  rw [DVect2.cons_append]
  dsimp
  rw [Category.id_comp]
State after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂) =
    DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (appendF.naturatorOplax F as✝ as₂ ≫
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs))

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂) =
    DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (appendF.naturatorOplax F as✝ as₂ ≫
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs))
Tactic:
rw [h_ind]
State after:
no goals