internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor ass =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor ass
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      (as :: ass) =
    Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as :: ass)
Tactic:
dsimp at *
Proof state after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
Tactic:
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 _ _
Proof state after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
this :
  ∀ (as bs : List α),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ bs) =
      Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as : List α
ass : List (List α)
h_ind :
  Prefunctor.obj joinF.toPrefunctor
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.obj joinF.toPrefunctor ass)
this :
  ∀ (as bs : List α),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ bs) =
      Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor bs
⊢ Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as ++
      Prefunctor.obj joinF.toPrefunctor
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor ass) =
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as ++ Prefunctor.obj joinF.toPrefunctor ass)
Tactic:
rw [this, h_ind]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      DVect2.nil)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil)
Tactic:
exact DVect2.Eq.nil_rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      (DVect2.cons f fs))
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs))
Tactic:
dsimp
Proof state after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))
Tactic:
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
Proof state after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))
Tactic:
apply DVect2.Eq.trans _ (this f (joinF.map fs)).symm
Proof state after:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.map joinF.toPrefunctor fs))
Theorem: CategoryTheory.List.joinF.naturality
Proof state before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
this :
  ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂),
    DVect2.Eq (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs₁ ++ fs₂))
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₁ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs₂)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (Prefunctor.map joinF.toPrefunctor fs))
Tactic:
apply DVect2.eq_of_eq_append_eq (DVect2.Eq.of rfl) h_ind
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unit_left
Proof state before:
α : Type u
inst✝ : Category α
⊢ singletonF ⋙ joinF = 𝟭 (List α)
Tactic:
dsimp [Functor.comp, Functor.id]
Proof state after:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor X),
        map := fun {X Y} f ↦ Prefunctor.map joinF.toPrefunctor (Prefunctor.map singletonF.toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Theorem: CategoryTheory.List.joinF.unit_left
Proof state before:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor X),
        map := fun {X Y} f ↦ Prefunctor.map joinF.toPrefunctor (Prefunctor.map singletonF.toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
dsimp [singletonF, joinF, DVect2.join]
Proof state after:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Theorem: CategoryTheory.List.joinF.unit_left
Proof state before:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
apply eqF_List
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor a

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

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)
Tactic:
. intro as
  dsimp
  exact List.append_nil as
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)
Theorem: CategoryTheory.List.joinF.unit_left
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)
Tactic:
. intro as bs fs
  dsimp
  exact DVect2.append_nil _
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
⊢ Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF = 𝟭 (List α)
Tactic:
dsimp [Functor.comp, Functor.id]
Proof state after:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj :=
          fun X ↦
            Prefunctor.obj joinF.toPrefunctor
              (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor X),
        map :=
          fun {X Y} f ↦
            Prefunctor.map joinF.toPrefunctor
              (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj :=
          fun X ↦
            Prefunctor.obj joinF.toPrefunctor
              (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor X),
        map :=
          fun {X Y} f ↦
            Prefunctor.map joinF.toPrefunctor
              (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
dsimp [singletonF, joinF, mapF, DVect2.join]
Proof state after:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ List.join (List.map (fun a ↦ [a]) X),
        map :=
          fun {X Y} f ↦
            DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ List.join (List.map (fun a ↦ [a]) X),
        map :=
          fun {X Y} f ↦
            DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
apply eqF_List <;> dsimp
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α), List.join (List.map (fun a ↦ [a]) a) = a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α), List.join (List.map (fun a ↦ [a]) a) = a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f
Tactic:
. intro as
  induction as
  case a.nil => rfl
  case a.cons a as h_ind => dsimp; rw [h_ind]
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f
Tactic:
. intro as bs fs
  induction fs
  case a.nil =>
    dsimp [DVect2.map, DVect2.join]
    exact DVect2.Eq.of rfl
  case a.cons a as b bs f fs h_ind =>
    dsimp [DVect2.map, DVect2.join]
    rw [DVect2.cons_append, DVect2.nil_append]
    exact DVect2.Eq.descend rfl h_ind
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
⊢ List.join (List.map (fun a ↦ [a]) []) = []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ List.join (List.map (fun a ↦ [a]) (a :: as)) = a :: as
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ a :: List.join (List.map (fun a ↦ [a]) as) = a :: as
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ a :: List.join (List.map (fun a ↦ [a]) as) = a :: as
Tactic:
rw [h_ind]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) DVect2.nil))
    DVect2.nil
Tactic:
dsimp [DVect2.map, DVect2.join]
Proof state after:
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq DVect2.nil DVect2.nil
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq DVect2.nil DVect2.nil
Tactic:
exact DVect2.Eq.of rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) (DVect2.cons f fs)))
    (DVect2.cons f fs)
Tactic:
dsimp [DVect2.map, DVect2.join]
Proof state after:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f DVect2.nil ++
      DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs))
    (DVect2.cons f fs)
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f DVect2.nil ++
      DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs))
    (DVect2.cons f fs)
Tactic:
rw [DVect2.cons_append, DVect2.nil_append]
Proof state after:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)))
    (DVect2.cons f fs)
Theorem: CategoryTheory.List.joinF.unit_right
Proof state before:
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)))
    (DVect2.cons f fs)
Tactic:
exact DVect2.Eq.descend rfl h_ind
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.assoc
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF ⋙ joinF = Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF
Tactic:
dsimp [Functor.comp, joinF, mapF]
Proof state after:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ List.join (List.join X), map := fun {X Y} f ↦ DVect2.join (DVect2.join f) } =
    Functor.mk
      { obj := fun X ↦ List.join (List.map List.join X),
        map := fun {X Y} f ↦ DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f) }
Theorem: CategoryTheory.List.joinF.assoc
Proof state before:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ List.join (List.join X), map := fun {X Y} f ↦ DVect2.join (DVect2.join f) } =
    Functor.mk
      { obj := fun X ↦ List.join (List.map List.join X),
        map := fun {X Y} f ↦ DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f) }
Tactic:
apply eqF_List <;> dsimp
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List (List (List α))), List.join (List.join a) = List.join (List.map List.join a)

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))