Theorem: CategoryTheory.List.appendF.naturatorLax_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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs₁ bs₂ =
    appendF.naturatorLax F as₁ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F [] bs₂ =
    appendF.naturatorLax F [] as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ 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✝ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a✝ ++ gs)
⊢ (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons a✝¹ a✝) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorLax F (a✝² :: as✝) as₂ ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons a✝¹ a✝ ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F [] bs₂ =
    appendF.naturatorLax F [] as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs)
Tactic:
case nil =>
  dsimp [appendF.naturatorLax]
  rw [Category.comp_id (Y:=(mapF.obj F).obj bs₂)]
  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₁ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorLax F (a✝ :: as✝) as₂ ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs)
Tactic:
case cons f fs h_ind =>
  dsimp [appendF.naturatorLax]
  conv =>
    lhs
    rw [DVect2.cons_append, comp_cons]
    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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F [] bs₂ =
    appendF.naturatorLax F [] as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs)
Tactic:
dsimp [appendF.naturatorLax]
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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor 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 ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor 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 ++ gs)
Tactic:
rw [Category.comp_id (Y:=(mapF.obj F).obj bs₂)]
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 ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ 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 ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs)
Tactic:
rw [Category.id_comp (X:=(mapF.obj F).obj as₂)]
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 ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs =
    Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ 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 ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs =
    Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorLax F (a✝ :: as✝) as₂ ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs)
Tactic:
dsimp [appendF.naturatorLax]
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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ (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) ≫
      DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor b✝)) (appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorLax F as✝ as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ (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) ≫
      DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor b✝)) (appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorLax F as✝ as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs)
Tactic:
conv =>
  lhs
  rw [DVect2.cons_append, comp_cons]
  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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ 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) ≫
        appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorLax F as✝ as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ 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) ≫
        appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorLax F as✝ as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ 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) ≫
        appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ 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 ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ 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) ≫
        appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs))
Tactic:
rw [h_ind]
State after:
no goals