internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.appendF.naturatorOplax_naturality
Proof 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]
Proof 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)
Theorem: CategoryTheory.List.appendF.naturatorOplax_naturality
Proof 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]
Proof 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))
Theorem: CategoryTheory.List.appendF.naturatorOplax_naturality
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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₁
Proof 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₂)
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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]
Proof 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₂)
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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₂)]
Proof 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₂)
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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]
Proof 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₂))
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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]
Proof 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₂))
Theorem: CategoryTheory.List.appendF.naturator_lax_oplax
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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₁
Proof 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₂))
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof 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₂)
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof 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₂)))
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof 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₂)))
Theorem: CategoryTheory.List.appendF.naturator_oplax_lax
Proof 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]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF =
    joinF ⋙ Prefunctor.obj mapF.toPrefunctor F
Tactic:
apply eqF_List
Proof state after:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a : List (List α)),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor a =
      Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a

case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a : List (List α)),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor a =
      Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a

case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
Tactic:
. intro ass
  induction ass
  case a.nil => rfl
  case a.cons as ass h_ind =>
    dsimp at *
    have : ∀ (as bs : List α), (mapF.obj F).obj (as++bs) = (mapF.obj F).obj as ++ (mapF.obj F).obj bs :=
      λ as bs => List.map_append F.obj _ _
    rw [this, h_ind]
Proof state after:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
Tactic:
. intros as₁ as₂ fs
  induction fs
  case a.nil => exact DVect2.Eq.nil_rfl
  case a.cons f fs h_ind =>
    dsimp
    have : ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂), DVect2.Eq ((mapF.obj F).map (fs₁ ++ fs₂)) ((mapF.obj F).map fs₁ ++ (mapF.obj F).map fs₂) :=
      λ fs₁ fs₂ => DVect2.map_append F.obj F.obj F.map
    apply DVect2.Eq.trans _ (this f (joinF.map fs)).symm
    apply DVect2.eq_of_eq_append_eq (DVect2.Eq.of rfl) h_ind
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor [] =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor []
Tactic:
rfl
Proof state after:
no goals