awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
e_α :
  ∀ (X : D),
    (NatTrans.app (𝟙 (G.functor ⋙ F)) X).toFunctor =
      ((G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)).app X).toFunctor
⊢ 𝟙 (G.functor ⋙ F) = G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : D
⊢ (NatTrans.app (𝟙 (G.functor ⋙ F)) X).toFunctor =
    ((G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)).app X).toFunctor

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, Functor.id_obj,
      Functor.map_id, NatTrans.comp_app, NatTrans.id_app, whiskerLeft_app, whiskerRight_app,
      Equivalence.counitInv_functor_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Equivalence.counitInv_functor_comp, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : Grothendieck (G.functor ⋙ F)
simp :
  (pre F G.functor).map
        (eqToHom ⋯ ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            NatTrans.app
              (𝟙
                (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                  pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
    𝟙 ((pre F G.functor).obj X)
⊢ CategoryStruct.comp (Y := (pre F G.functor).obj ((preInv F G).obj ((pre F G.functor).obj X)))
      ((pre F G.functor).map
          ((eqToIso ⋯ ≪≫
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).isoWhiskerLeft
                      (Grothendieck.preUnitIso F G) ≪≫
                    eqToIso ⋯).hom.app
            X) :
        (pre F G.functor).obj X ⟶ (pre F G.functor).obj ((preInv F G).obj ((pre F G.functor).obj X)))
      ((preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) :
        (preInv F G ⋙ pre F G.functor).obj ((pre F G.functor).obj X) ⟶
          obj (𝟭 (Grothendieck F)) ((pre F G.functor).obj X)) =
    𝟙 ((pre F G.functor).obj X)

Tactic:
simp only [preInv, Grothendieck.preUnitIso, pre_id,
      Iso.trans_hom, eqToIso.hom, eqToHom_app, eqToHom_refl, isoWhiskerLeft_hom, NatTrans.comp_app]

Premises used: CategoryTheory.Grothendieck.preInv, CategoryTheory.eqToIso.hom, CategoryTheory.Grothendieck.preUnitIso, CategoryTheory.eqToHom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Iso.trans_hom, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.isoWhiskerLeft_hom, CategoryTheory.Grothendieck.pre_id
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : Grothendieck (G.functor ⋙ F)
w_base :
  Hom.base
      ((pre F G.functor).map
          (eqToHom ⋯ ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              NatTrans.app
                (𝟙
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                    pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)) =
    Hom.base (𝟙 ((pre F G.functor).obj X))
w_fiber :
  CategoryStruct.comp (Y :=
      obj.{v₂, v₂, u₂, u₂}
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ((pre F G.functor).map
                  (eqToHom ⋯ ≫
                    ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                            (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                        X ≫
                      NatTrans.app
                        (𝟙
                          (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                            pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                        X) ≫
                (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)))))
        ((pre F G.functor).obj X).fiber)
      (eqToHom ⋯)
      (Hom.fiber
        ((pre F G.functor).map
            (eqToHom ⋯ ≫
              ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                      (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                  X ≫
                NatTrans.app
                  (𝟙
                    (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                      pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                  X) ≫
          (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X))) =
    Hom.fiber (𝟙 ((pre F G.functor).obj X))
⊢ (pre F G.functor).map
        (eqToHom ⋯ ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            NatTrans.app
              (𝟙
                (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                  pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
    𝟙 ((pre F G.functor).obj X)

Tactic:
fapply Grothendieck.ext

Premises used: CategoryTheory.Grothendieck.ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : Grothendieck (G.functor ⋙ F)
⊢ CategoryStruct.comp (Y :=
      obj.{v₂, v₂, u₂, u₂}
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ((pre F G.functor).map
                  (eqToHom ⋯ ≫
                    ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                            (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                        X ≫
                      NatTrans.app
                        (𝟙
                          (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                            pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                        X) ≫
                (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)))))
        ((pre F G.functor).obj X).fiber)
      (eqToHom ⋯)
      (Hom.fiber
        ((pre F G.functor).map
            (eqToHom ⋯ ≫
              ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                      (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                  X ≫
                NatTrans.app
                  (𝟙
                    (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                      pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                  X) ≫
          (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X))) =
    Hom.fiber (𝟙 ((pre F G.functor).obj X))

Tactic:
simp [preNatIso, transportIso]

Premises used: CategoryTheory.Grothendieck.transportIso, CategoryTheory.Grothendieck.preNatIso
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
⊢ (F.map (𝟙 { base := c, fiber := X : Grothendieck F }.base)).toFunctor.obj
      { base := c, fiber := X : Grothendieck F }.fiber =
    X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
d : (↑(F.obj c) : Type u₂)
dsimp :
  { base := 𝟙 c, fiber := eqToHom ⋯ ≫ 𝟙 d :
      { base := c, fiber := d : Grothendieck F }.Hom { base := c, fiber := d : Grothendieck F } } =
    𝟙 { base := c, fiber := d }
⊢ { base := 𝟙 { base := c, fiber := d : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ 𝟙 d :
      { base := c, fiber := d : Grothendieck F }.Hom { base := c, fiber := d : Grothendieck F } } =
    𝟙 { base := c, fiber := d }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
d : (↑(F.obj c) : Type u₂)
e_fiber : eqToHom ⋯ ≫ 𝟙 d = eqToHom ⋯
⊢ { base := 𝟙 c, fiber := eqToHom ⋯ ≫ 𝟙 d :
      { base := c, fiber := d : Grothendieck F }.Hom { base := c, fiber := d : Grothendieck F } } =
    𝟙 { base := c, fiber := d }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
d : (↑(F.obj c) : Type u₂)
⊢ eqToHom ⋯ ≫ 𝟙 d = eqToHom ⋯

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y Z : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
g : Y ⟶ Z
⊢ { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f ≫ g :
        { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }.base =
    Hom.base
      ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
          { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
        { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y Z : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
g : Y ⟶ Z
e_a :
  Eq (α := (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Y) (eqToHom ⋯ ≫ f : (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Y)
    (CategoryStruct.comp (Y := (F.map (𝟙 c)).toFunctor.obj Y) (eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f) (eqToHom ⋯) :
      (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Y)
⊢ Eq (α := (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Z) ((eqToHom ⋯ ≫ f) ≫ g : (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Z)
    (CategoryStruct.comp (Y := (F.map (𝟙 c)).toFunctor.obj Y) (eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f) (eqToHom ⋯) ≫
        g :
      (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Z)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y Z : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
g : Y ⟶ Z
e_a : f = eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f ≫ eqToHom ⋯
⊢ Eq (α := (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Y) (eqToHom ⋯ ≫ f : (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Y)
    (CategoryStruct.comp (Y := (F.map (𝟙 c)).toFunctor.obj Y) (eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f) (eqToHom ⋯) :
      (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Y)

Tactic:
simp only [eqToHom_comp_iff, Category.assoc, eqToHom_trans_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.eqToHom_comp_iff
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y Z : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
g : Y ⟶ Z
⊢ f = eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f ≫ eqToHom ⋯

Tactic:
apply Functor.congr_hom congr($(F.map_id _).toFunctor).symm

Premises used: congrArg, CategoryTheory.Functor.congr_hom, id, CategoryTheory.Functor.map_id, Eq.symm, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y : (↑(F.obj c) : Type u₂)
a₁ a₂ : X ⟶ Y
f : (ι F c).map a₁ = (ι F c).map a₂
⊢ Eq.{v + 1} (α := { base := c, fiber := X : Grothendieck F }.base ⟶ { base := c, fiber := X : Grothendieck F }.base)
    (𝟙 { base := c, fiber := X : Grothendieck F }.base) (𝟙 { base := c, fiber := X : Grothendieck F }.base)

Tactic:
injection f with _ f
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y : (↑(F.obj c) : Type u₂)
a₁ a₂ : X ⟶ Y
f : (ι F c).map a₁ = (ι F c).map a₂
base_eq :
  Eq.{v + 1} (α := { base := c, fiber := X : Grothendieck F }.base ⟶ { base := c, fiber := X : Grothendieck F }.base)
    (𝟙 { base := c, fiber := X : Grothendieck F }.base) (𝟙 { base := c, fiber := X : Grothendieck F }.base)
⊢ Eq (α :=
    (F.map (𝟙 { base := c, fiber := X : Grothendieck F }.base)).toFunctor.obj
        { base := c, fiber := X : Grothendieck F }.fiber ⟶
      { base := c, fiber := Y }.fiber)
    (eqToHom ⋯ ≫ a₁) (eqToHom ⋯ ≫ a₂)

Tactic:
injection f with _ f
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y : (↑(F.obj c) : Type u₂)
a₁ a₂ : X ⟶ Y
base_eq :
  Eq.{v + 1} (α := { base := c, fiber := X : Grothendieck F }.base ⟶ { base := c, fiber := X : Grothendieck F }.base)
    (𝟙 { base := c, fiber := X : Grothendieck F }.base) (𝟙 { base := c, fiber := X : Grothendieck F }.base)
f :
  Eq (α :=
    (F.map (𝟙 { base := c, fiber := X : Grothendieck F }.base)).toFunctor.obj
        { base := c, fiber := X : Grothendieck F }.fiber ⟶
      { base := c, fiber := Y }.fiber)
    (eqToHom ⋯ ≫ a₁) (eqToHom ⋯ ≫ a₂)
rwa rwa₁ rwa₂ rwa₃ : ∀ (f : a₁ = a₂), a₁ = a₂
⊢ a₁ = a₂

Tactic:
rwa [cancel_epi] at f

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x x_1 : (↑(F.obj X) : Type u₂)
x_2 : x ⟶ x_1
simp :
  Eq (α := { base := X, fiber := x : Grothendieck F } ⟶ { base := Y, fiber := (F.map f).toFunctor.obj x_1 })
    (CategoryStruct.comp (Y := { base := X, fiber := x_1 }) { base := 𝟙 X, fiber := eqToHom ⋯ ≫ x_2 }
      { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x_1) })
    (CategoryStruct.comp (Y := { base := Y, fiber := (F.map f).toFunctor.obj x })
      { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x) }
      { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x_2 })
⊢ (ι F X).map x_2 ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((ι F X).obj x_1).fiber) } =
    { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((ι F X).obj x).fiber) :
        ((ι F X).obj x).Hom (((F.map f).toFunctor ⋙ ι F Y).obj x) } ≫
      ((F.map f).toFunctor ⋙ ι F Y).map x_2

Tactic:
simp only [ι, Functor.comp_obj, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Grothendieck.ι, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x x_1 : (↑(F.obj X) : Type u₂)
x_2 : x ⟶ x_1
⊢ Eq.{v + 1} (α :=
    { base := X, fiber := x : Grothendieck F }.base ⟶
      { base := Y, fiber := (F.map f).toFunctor.obj x_1 : Grothendieck F }.base)
    (Hom.base
      (CategoryStruct.comp (Y := { base := X, fiber := x_1 }) { base := 𝟙 X, fiber := eqToHom ⋯ ≫ x_2 }
        { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x_1) }))
    (Hom.base
      (CategoryStruct.comp (Y := { base := Y, fiber := (F.map f).toFunctor.obj x })
        { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x) }
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x_2 }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x x_1 : (↑(F.obj X) : Type u₂)
x_2 : x ⟶ x_1
⊢ eqToHom ⋯ ≫
      Hom.fiber
        (CategoryStruct.comp (Y := { base := X, fiber := x_1 : Grothendieck F })
          { base := 𝟙 X, fiber := eqToHom ⋯ ≫ x_2 :
            { base := X, fiber := x : Grothendieck F }.Hom { base := X, fiber := x_1 : Grothendieck F } }
          { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x_1) :
            { base := X, fiber := x_1 : Grothendieck F }.Hom
              { base := Y, fiber := (F.map f).toFunctor.obj x_1 : Grothendieck F } }) =
    Hom.fiber
      (CategoryStruct.comp (Y := { base := Y, fiber := (F.map f).toFunctor.obj x })
        { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x) }
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x_2 })

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x x_1 : (↑(F.obj X) : Type u₂)
x_2 : x ⟶ x_1
⊢ Eq (α := { base := X, fiber := x : Grothendieck F } ⟶ { base := Y, fiber := (F.map f).toFunctor.obj x_1 })
    (CategoryStruct.comp (Y := { base := X, fiber := x_1 }) { base := 𝟙 X, fiber := eqToHom ⋯ ≫ x_2 }
      { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x_1) })
    (CategoryStruct.comp (Y := { base := Y, fiber := (F.map f).toFunctor.obj x })
      { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x) }
      { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x_2 })

Tactic:
exact Grothendieck.ext _ _ (by simp) (by simp [eqToHom_map])

Premises used: CategoryTheory.Grothendieck.ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
c : C
simp : fib c = Cat.Hom.toFunctor (𝟙 (F.obj c)) ⋙ fib c
⊢ fib c = (F.map (𝟙 c)).toFunctor ⋙ fib c

Tactic:
simp only [Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
c : C
⊢ fib c = Cat.Hom.toFunctor (𝟙 (F.obj c)) ⋙ fib c

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
simp : (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map f ≫ F.map g).toFunctor ⋙ fib c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map (f ≫ g)).toFunctor ⋙ fib c₃

Tactic:
simp only [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map f ≫ F.map g).toFunctor ⋙ fib c₃

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) = hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom ⋯
X : Grothendieck F
⊢ (hom (Hom.base (𝟙 X))).app X.fiber ≫ Functor.map (fib X.base) (Hom.fiber (𝟙 X)) = 𝟙 (obj (fib X.base) X.fiber)

Tactic:
simp [hom_id]
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) = hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom ⋯
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ (hom (f ≫ g).base).app X.fiber ≫ Functor.map (fib Z.base) (f ≫ g).fiber =
    ((hom f.base).app X.fiber ≫ Functor.map (fib Y.base) f.fiber) ≫
      (hom g.base).app Y.fiber ≫ Functor.map (fib Z.base) g.fiber

Tactic:
simp [hom_comp]