internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.eqF_List
Proof state before:
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ F_map = G_map
Tactic:
apply funext
Proof state after:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ ∀ (x : a ⟶ b), F_map x = G_map x
Theorem: CategoryTheory.List.eqF_List
Proof state before:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ ∀ (x : a ⟶ b), F_map x = G_map x
Tactic:
intro f
Proof state after:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
f : a ⟶ b
⊢ F_map f = G_map f
Theorem: CategoryTheory.List.eqF_List
Proof state before:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
f : a ⟶ b
⊢ F_map f = G_map f
Tactic:
exact (hmap a b f).eq_of
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.obj_id
Proof state before:
α : Type u
inst✝ : Category α
⊢ Prefunctor.obj mapF.toPrefunctor (𝟭 α) = 𝟭 (List α)
Tactic:
apply eqF_List <;> dsimp [Functor.id]
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor a =
      a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
Theorem: CategoryTheory.List.mapF.obj_id
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor a =
      a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
Tactic:
. intro as
  change List.map id as = as
  rw [List.map_id]
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
Theorem: CategoryTheory.List.mapF.obj_id
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
Tactic:
. intro as₁ as₂ fs
  change DVect2.Eq (DVect2.map id id id fs) fs
  exact DVect2.map_id
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.obj_comp
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ Prefunctor.obj mapF.toPrefunctor (F ⋙ G) = Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G
Tactic:
dsimp [Functor.comp, mapF]
Proof state after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ Functor.mk
      { obj := List.map fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X),
        map :=
          fun {X Y} ↦
            DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
              (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
              fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f) } =
    Functor.mk
      { obj := fun X ↦ List.map G.toPrefunctor.obj (List.map F.toPrefunctor.obj X),
        map :=
          fun {X Y} f ↦
            DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
              (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f) }
Theorem: CategoryTheory.List.mapF.obj_comp
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ Functor.mk
      { obj := List.map fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X),
        map :=
          fun {X Y} ↦
            DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
              (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
              fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f) } =
    Functor.mk
      { obj := fun X ↦ List.map G.toPrefunctor.obj (List.map F.toPrefunctor.obj X),
        map :=
          fun {X Y} f ↦
            DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
              (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f) }
Tactic:
apply eqF_List <;> dsimp
Proof state after:
case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a : List α),
    List.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X)) a =
      List.map G.toPrefunctor.obj (List.map F.toPrefunctor.obj a)

case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f)) f)
      (DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
        (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f))
Theorem: CategoryTheory.List.mapF.obj_comp
Proof state before:
case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a : List α),
    List.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X)) a =
      List.map G.toPrefunctor.obj (List.map F.toPrefunctor.obj a)

case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f)) f)
      (DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
        (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f))
Tactic:
. intro as
  rw [←List.map_comp G.obj F.obj]
  rfl
Proof state after:
case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f)) f)
      (DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
        (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f))
Theorem: CategoryTheory.List.mapF.obj_comp
Proof state before:
case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f)) f)
      (DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
        (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f))
Tactic:
. intro as₁ as₂ fs
  exact DVect2.map_comp
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.map_id
Proof state before:
α : Type u
inst✝ : Category α
as bs : List α
⊢ 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
bs : List α
⊢ 𝟙 [] ++ 𝟙 bs = 𝟙 ([] ++ bs)

case cons
α : Type u
inst✝ : Category α
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : 𝟙 tail✝ ++ 𝟙 bs = 𝟙 (tail✝ ++ bs)
⊢ 𝟙 (head✝ :: tail✝) ++ 𝟙 bs = 𝟙 (head✝ :: tail✝ ++ bs)
Theorem: CategoryTheory.List.appendF.map_id
Proof state before:
α : Type u
inst✝ : Category α
bs : List α
⊢ 𝟙 [] ++ 𝟙 bs = 𝟙 ([] ++ bs)
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.map_id
Proof state before:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ 𝟙 (a :: as) ++ 𝟙 bs = 𝟙 (a :: as ++ bs)
Tactic:
case cons a as h_ind =>
  dsimp
  rw [DVect2.cons_append, h_ind]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.map_id
Proof state before:
α : Type u
inst✝ : Category α
bs : List α
⊢ 𝟙 [] ++ 𝟙 bs = 𝟙 ([] ++ bs)
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.map_id
Proof state before:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ 𝟙 (a :: as) ++ 𝟙 bs = 𝟙 (a :: as ++ bs)
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ DVect2.cons (𝟙 a) (𝟙 as) ++ 𝟙 bs = DVect2.cons (𝟙 a) (𝟙 (as ++ bs))
Theorem: CategoryTheory.List.appendF.map_id
Proof state before:
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ DVect2.cons (𝟙 a) (𝟙 as) ++ 𝟙 bs = DVect2.cons (𝟙 a) (𝟙 (as ++ bs))
Tactic:
rw [DVect2.cons_append, h_ind]
Proof state after:
no goals
Theorem: CategoryTheory.List.appendF.map_comp
Proof state before:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ (DVect2.cons f fs₁ ++ fs₂) ≫ (DVect2.cons g gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂
Tactic:
rw [DVect2.cons_append, DVect2.cons_append]
Proof state after:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons f (fs₁ ++ fs₂) ≫ DVect2.cons g (gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂
Theorem: CategoryTheory.List.appendF.map_comp
Proof state before:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons f (fs₁ ++ fs₂) ≫ DVect2.cons g (gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons (f ≫ g) ((fs₁ ++ fs₂) ≫ (gs₁ ++ gs₂)) = DVect2.cons (f ≫ g) (fs₁ ≫ gs₁) ++ fs₂ ≫ gs₂
Theorem: CategoryTheory.List.appendF.map_comp
Proof state before:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons (f ≫ g) ((fs₁ ++ fs₂) ≫ (gs₁ ++ gs₂)) = DVect2.cons (f ≫ g) (fs₁ ≫ gs₁) ++ fs₂ ≫ gs₂
Tactic:
rw [appendF.map_comp fs₁ _ gs₁ _, DVect2.cons_append]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
as : List α
⊢ mapF.unitorLax as ≫ mapF.unitorOplax as = 𝟙 as
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ mapF.unitorLax [] ≫ mapF.unitorOplax [] = 𝟙 []

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ : mapF.unitorLax tail✝ ≫ mapF.unitorOplax tail✝ = 𝟙 tail✝
⊢ mapF.unitorLax (head✝ :: tail✝) ≫ mapF.unitorOplax (head✝ :: tail✝) = 𝟙 (head✝ :: tail✝)
Theorem: CategoryTheory.List.mapF.unitor_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
⊢ mapF.unitorLax [] ≫ mapF.unitorOplax [] = 𝟙 []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : mapF.unitorLax as ≫ mapF.unitorOplax as = 𝟙 as
⊢ mapF.unitorLax (a :: as) ≫ mapF.unitorOplax (a :: as) = 𝟙 (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [mapF.unitorLax, mapF.unitorOplax, List.id, DVect2.fromList]
  rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
⊢ mapF.unitorLax [] ≫ mapF.unitorOplax [] = 𝟙 []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : mapF.unitorLax as ≫ mapF.unitorOplax as = 𝟙 as
⊢ mapF.unitorLax (a :: as) ≫ mapF.unitorOplax (a :: as) = 𝟙 (a :: as)
Tactic:
dsimp [mapF.unitorLax, mapF.unitorOplax, List.id, DVect2.fromList]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : mapF.unitorLax as ≫ mapF.unitorOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorLax as ≫ mapF.unitorOplax as) = DVect2.cons (𝟙 a) (𝟙 as)
Theorem: CategoryTheory.List.mapF.unitor_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : mapF.unitorLax as ≫ mapF.unitorOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorLax as ≫ mapF.unitorOplax as) = DVect2.cons (𝟙 a) (𝟙 as)
Tactic:
rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
as : List α
⊢ mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ mapF.unitorOplax [] ≫ mapF.unitorLax [] = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor [])

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ :
  mapF.unitorOplax tail✝ ≫ mapF.unitorLax tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor tail✝)
⊢ mapF.unitorOplax (head✝ :: tail✝) ≫ mapF.unitorLax (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor (head✝ :: tail✝))
Theorem: CategoryTheory.List.mapF.unitor_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
⊢ mapF.unitorOplax [] ≫ mapF.unitorLax [] = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ mapF.unitorOplax (a :: as) ≫ mapF.unitorLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [mapF.unitorLax, mapF.unitorOplax, List.id, DVect2.fromList]
  rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
⊢ mapF.unitorOplax [] ≫ mapF.unitorLax [] = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor [])
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.unitor_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ mapF.unitorOplax (a :: as) ≫ mapF.unitorLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor (a :: as))
Tactic:
dsimp [mapF.unitorLax, mapF.unitorOplax, List.id, DVect2.fromList]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorOplax as ≫ mapF.unitorLax as) =
    DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as))
Theorem: CategoryTheory.List.mapF.unitor_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorOplax as ≫ mapF.unitorLax as) =
    DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as))
Tactic:
rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
as : List α
⊢ mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorLax F G [] ≫ mapF.compositorOplax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor [])

case cons
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  mapF.compositorLax F G tail✝ ≫ mapF.compositorOplax F G tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor tail✝)
⊢ mapF.compositorLax F G (head✝ :: tail✝) ≫ mapF.compositorOplax F G (head✝ :: tail✝) =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
        (head✝ :: tail✝))