Theorem: CategoryTheory.List.mapF.obj_comp (Moncalc/CategoryTheory/List/Basic.lean)

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]
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) }

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
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))

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
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))

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
State after:
no goals