Theorem: CategoryTheory.List.mapF.naturality₂ (Moncalc/CategoryTheory/List/Functor.lean)

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ (Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom =
    (mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)
Tactic:
ext as
State after:
case w.h
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
as : List α
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as

State before:
case w.h
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
as : List α
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
Tactic:
induction as
State after:
case w.h.nil
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      [] =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) []

case w.h.cons
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
head✝ : α
tail✝ : List α
tail_ih✝ :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      tail✝ =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) tail✝
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (head✝ :: tail✝) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (head✝ :: tail✝)

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      [] =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) []
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (a :: as) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [mapF.compositor, mapF.compositorLax] at *
  rw [h_ind, Category.id_comp, Category.comp_id]
State after:
no goals

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      [] =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) []
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (a :: as) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (a :: as)
Tactic:
dsimp [mapF.compositor, mapF.compositorLax] at *
State after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  (NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
          (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
      mapF.compositorLax F₂ G₂ as =
    mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ DVect2.cons
      ((NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a)) ≫
        𝟙 (Prefunctor.obj G₂.toPrefunctor (Prefunctor.obj F₂.toPrefunctor a)))
      ((NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
            (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
        mapF.compositorLax F₂ G₂ as) =
    DVect2.cons
      (𝟙 (Prefunctor.obj G₁.toPrefunctor (Prefunctor.obj F₁.toPrefunctor a)) ≫
        NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a))
      (mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as)

State before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  (NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
          (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
      mapF.compositorLax F₂ G₂ as =
    mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ DVect2.cons
      ((NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a)) ≫
        𝟙 (Prefunctor.obj G₂.toPrefunctor (Prefunctor.obj F₂.toPrefunctor a)))
      ((NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
            (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
        mapF.compositorLax F₂ G₂ as) =
    DVect2.cons
      (𝟙 (Prefunctor.obj G₁.toPrefunctor (Prefunctor.obj F₁.toPrefunctor a)) ≫
        NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a))
      (mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as)
Tactic:
rw [h_ind, Category.id_comp, Category.comp_id]
State after:
no goals