-- Mathlib/CategoryTheory/Grothendieck.lean
theorem map_comp_eq (α : F ⟶ G) (β : G ⟶ H) :
    map (α ≫ β) = map α ⋙ map β

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ map (α ≫ β) = map α ⋙ map β

Tactic:
fapply Functor.ext

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯)
    _auto✝

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

Tactic:
intro X

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X : Grothendieck F
⊢ (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯

Tactic:
simp only [map_map, map_obj_base, NatTrans.comp_app, Cat.comp_obj, Cat.comp_map,
  eqToHom_refl, Functor.comp_map, Functor.map_comp, Category.comp_id, Category.id_comp]

Result:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) } =
    { base := f.base,
      fiber :=
        (eqToHom ⋯).app ((map α).obj X).fiber ≫
          (β.app Y.base).map ((eqToHom ⋯).app X.fiber) ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) } =
    { base := f.base,
      fiber :=
        (eqToHom ⋯).app ((map α).obj X).fiber ≫
          (β.app Y.base).map ((eqToHom ⋯).app X.fiber) ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }

Tactic:
fapply Grothendieck.ext

Result:
case h_map.w_base
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.base =
    { base := f.base,
        fiber :=
          (eqToHom ⋯).app ((map α).obj X).fiber ≫
            (β.app Y.base).map ((eqToHom ⋯).app X.fiber) ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.base

case h_map.w_fiber
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom ⋯ ≫
      { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.fiber =
    { base := f.base,
        fiber :=
          (eqToHom ⋯).app ((map α).obj X).fiber ≫
            (β.app Y.base).map ((eqToHom ⋯).app X.fiber) ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.fiber

Proof state:
case h_map.w_fiber
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom ⋯ ≫
      { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.fiber =
    { base := f.base,
        fiber :=
          (eqToHom ⋯).app ((map α).obj X).fiber ≫
            (β.app Y.base).map ((eqToHom ⋯).app X.fiber) ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.fiber

Tactic:
simp

Result:
no goals

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro X Y f

Result:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯

Proof state:
case h_map.w_base
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := (eqToHom ⋯).app X.fiber ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.base =
    { base := f.base,
        fiber :=
          (eqToHom ⋯).app ((map α).obj X).fiber ≫
            (β.app Y.base).map ((eqToHom ⋯).app X.fiber) ≫ (β.app Y.base).map ((α.app Y.base).map f.fiber) }.base

Tactic:
rfl

Result:
no goals

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X : Grothendieck F
⊢ (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

Tactic:
rfl

Result:
no goals