[GOAL]
C : Type u₁
inst✝¹ : Category.{u_1, u₁} C
D : Type u₂
inst✝ : Category.{u_2, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : D
h : F.obj Z ⟶ W
⊢ F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h
[PROOFSTEP]
rw [F.map_comp, Category.assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map (f ≫ g) =
      { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map f ≫
        { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map (f✝ ≫ g✝) =
    { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map f✝ ≫
      { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }.map g✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ G.map (F.map (f✝ ≫ g✝)) = G.map (F.map f✝) ≫ G.map (F.map g✝)
[PROOFSTEP]
rw [F.map_comp, G.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
⊢ F ⋙ 𝟭 D = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ mk toPrefunctor✝ ⋙ 𝟭 D = mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
⊢ 𝟭 C ⋙ F = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ 𝟭 C ⋙ mk toPrefunctor✝ = mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
P : Prop
inst✝ : Decidable P
f : P → (X ⟶ Y)
g : ¬P → (X ⟶ Y)
⊢ F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
[PROOFSTEP]
aesop_cat
