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_1 : C ⥤ Cat
E : Cat
F : (↑E : Type u) ⥤ Cat
h :
  Cat.Hom.toFunctor (Over.Hom.left (Over.homMk (map (𝟙 F)).toCatHom ⋯)) =
    (Over.Hom.left (𝟙 (Over.mk (forget F).toCatHom))).toFunctor
⊢ Over.homMk (map (𝟙 F)).toCatHom ⋯ = 𝟙 (Over.mk (forget F).toCatHom)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F_1 : C ⥤ Cat
E : Cat
F : (↑E : Type u) ⥤ Cat
⊢ Cat.Hom.toFunctor (Over.Hom.left (Over.homMk (map (𝟙 F)).toCatHom ⋯)) =
    (Over.Hom.left (𝟙 (Over.mk (forget F).toCatHom))).toFunctor

Tactic:
Grothendieck.map_id_eq (F := F)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Cat.of, CategoryTheory.Cat, CategoryTheory.Grothendieck.map_id_eq, CategoryTheory.Bundled.of, CategoryTheory.Grothendieck.map
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F_1 : C ⥤ Cat
E : Cat
F : (↑E : Type u) ⥤ Cat
⊢ Cat.Hom.toFunctor (Over.Hom.left (Over.homMk (map (𝟙 F)).toCatHom ⋯)) =
    (Over.Hom.left (𝟙 (Over.mk (forget F).toCatHom))).toFunctor

Tactic:
exact Grothendieck.map_id_eq (F := F)

Premises used: CategoryTheory.Grothendieck.map_id_eq
-- 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
E : Cat
X Y Z : (↑E : Type u) ⥤ Cat
α : X ⟶ Y
β : Y ⟶ Z
simp :
  Eq (α := Over.mk (forget X).toCatHom ⟶ Over.mk (forget Z).toCatHom) (Over.homMk (map α ⋙ map β).toCatHom ⋯)
    (CategoryStruct.comp (Y := Over.mk (forget Y).toCatHom) (Over.homMk (map α).toCatHom ⋯)
      (Over.homMk (map β).toCatHom ⋯))
⊢ Eq (α := Over.mk (forget X).toCatHom ⟶ Over.mk (forget Z).toCatHom) (Over.homMk (map (α ≫ β)).toCatHom ⋯)
    (CategoryStruct.comp (Y := Over.mk (forget Y).toCatHom) (Over.homMk (map α).toCatHom ⋯)
      (Over.homMk (map β).toCatHom ⋯))

Tactic:
simp [Grothendieck.map_comp_eq α β]

Premises used: CategoryTheory.Grothendieck.map_comp_eq
-- 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
E : Cat
X Y Z : (↑E : Type u) ⥤ Cat
α : X ⟶ Y
β : Y ⟶ Z
⊢ Eq (α := Over.mk (forget X).toCatHom ⟶ Over.mk (forget Z).toCatHom) (Over.homMk (map α ⋙ map β).toCatHom ⋯)
    (CategoryStruct.comp (Y := Over.mk (forget Y).toCatHom) (Over.homMk (map α).toCatHom ⋯)
      (Over.homMk (map β).toCatHom ⋯))

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)
X : Grothendieck (G ⋙ typeToCat)
rcases :
  (base : C) →
    (as : G.obj base) →
      obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base, fiber := { as := as : Discrete (G.obj base) } } ≅
        (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj
          { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) }
⊢ obj (𝟭 (Grothendieck (G ⋙ typeToCat))) X ≅ (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj X

Tactic:
rcases X with ⟨_, ⟨⟩⟩
-- 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)
base : C
as : G.obj base
⊢ obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base, fiber := { as := as : Discrete (G.obj base) } } ≅
    (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj
      { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) }

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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)
base_1 : C
as : G.obj base_1
base_2 : C
as_1 : G.obj base_2
base :
  Grothendieck.base.{u, v, w, w} (F := G ⋙ typeToCat)
      { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) } ⟶
    Grothendieck.base.{u, v, w, w} (F := G ⋙ typeToCat)
      { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } }
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj
        (fiber { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) })).as =
    Discrete.as (fiber { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } })
⊢ { base := base,
      fiber :=
        {
          down :=
            { down := f :
              PLift
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                  as_1) } :
          ULift.{w, 0}
            (PLift
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                as_1)) } :
      Hom.{u, v, w, w} (F := G ⋙ typeToCat)
        { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) }
        { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } : Grothendieck (G ⋙ typeToCat) } } =
    (grothendieckTypeToCatInverse G).map
      ((grothendieckTypeToCatFunctor G).map
        { base := base,
          fiber :=
            {
              down :=
                { down := f :
                  PLift
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                      as_1) } :
              ULift.{w, 0}
                (PLift
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                    as_1)) } })

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)
X : G.Elements
mk :
  (fst : C) →
    (snd : G.obj fst) →
      (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
          (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ≅
        obj (𝟭 G.Elements) (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd)
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X

Tactic:
cases 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 : Functor.{v, w, u, w + 1} C (Type w)
fst : C
snd : G.obj fst
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
      (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ≅
    obj (𝟭 G.Elements) (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd)

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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)
fst : C
snd : G.obj fst
fst_1 : C
snd_1 : G.obj fst_1
f :
  (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).fst (β := fun (c : C) ↦ G.obj c) ⟶
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ G.obj c)
e :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
        (a : (fun (X : Type w) ↦ X) (G.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (G.obj ⟨fst_1, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).snd (β := fun (c : C) ↦ G.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ G.obj c)
simp :
  (grothendieckTypeToCatFunctor G).map
      ((grothendieckTypeToCatInverse G).map
        (Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e)) =
    Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e
⊢ (grothendieckTypeToCatFunctor G).map
        ((grothendieckTypeToCatInverse G).map
          (Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e)) ≫
      𝟙
        ((grothendieckTypeToCatFunctor G).obj
          ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1))) =
    𝟙
        ((grothendieckTypeToCatFunctor G).obj
          ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd))) ≫
      Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e

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)
fst : C
snd : G.obj fst
fst_1 : C
snd_1 : G.obj fst_1
f :
  (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).fst (β := fun (c : C) ↦ G.obj c) ⟶
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ G.obj c)
e :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
        (a : (fun (X : Type w) ↦ X) (G.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (G.obj ⟨fst_1, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).snd (β := fun (c : C) ↦ G.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ G.obj c)
⊢ (grothendieckTypeToCatFunctor G).map
      ((grothendieckTypeToCatInverse G).map
        (Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e)) =
    Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e

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)
base : C
as : G.obj base
⊢ Iso.hom
      (Sigma.rec (β := fun (c : C) ↦ G.obj c) (motive := fun (t : (c : C) × G.obj c) ↦
        (h :
            (grothendieckTypeToCatFunctor G).obj
                { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) } =
              t) →
          (grothendieckTypeToCatFunctor G).obj
              ((grothendieckTypeToCatInverse G).obj
                ((grothendieckTypeToCatFunctor G).obj
                  { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })) ≅
            (grothendieckTypeToCatFunctor G).obj { base := base, fiber := { as := as : Discrete (G.obj base) } })
        (fun (fst : C) (snd : G.obj fst)
            (h :
              (grothendieckTypeToCatFunctor G).obj
                  { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) } =
                Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ↦
          Eq.rec (motive := fun (x : G.Elements) (x_1 : Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd = x) ↦
            (grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj x) ≅ x)
            (Iso.refl
              ((grothendieckTypeToCatFunctor G).obj
                ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd))))
            ⋯)
        ((grothendieckTypeToCatFunctor G).obj
          { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })
        ⋯) =
    𝟙
      ((grothendieckTypeToCatFunctor G).obj
        { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })

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_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Functor.{v₁, v, u₁, u} D C
X : Grothendieck (G ⋙ F)
⊢ CategoryStruct.comp (Y :=
      (F.map
              { base := G.map (Hom.base (𝟙 X)), fiber := Hom.fiber (𝟙 X) :
                  { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.Hom
                    { base := G.obj X.base, fiber := X.fiber : Grothendieck F } }.base).toFunctor.obj
        { base := G.obj X.base, fiber := X.fiber }.fiber)
      (eqToHom ⋯) { base := G.map (Hom.base (𝟙 X)), fiber := Hom.fiber (𝟙 X) }.fiber =
    Hom.fiber (𝟙 { base := G.obj X.base, fiber := X.fiber : Grothendieck F })

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_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Functor.{v₁, v, u₁, u} D C
X Y Z : Grothendieck (G ⋙ F)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ({ base := G.map f.base, fiber := f.fiber :
                  { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.Hom
                    { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F } } ≫
                { base := G.map g.base, fiber := g.fiber :
                  { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F }.Hom
                    { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F } }))))
        { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.fiber ⟶
      { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F }.fiber)
    (CategoryStruct.comp (Y :=
        (F.map
                { base := G.map (f ≫ g).base, fiber := (f ≫ g).fiber :
                    { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.Hom
                      { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F } }.base).toFunctor.obj
          { base := G.obj X.base, fiber := X.fiber }.fiber)
        (eqToHom ⋯) { base := G.map (f ≫ g).base, fiber := (f ≫ g).fiber }.fiber :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := G.map f.base, fiber := f.fiber :
                    { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.Hom
                      { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F } } ≫
                  { base := G.map g.base, fiber := g.fiber :
                    { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F }.Hom
                      { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F } }))))
          { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.fiber ⟶
        { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F }.fiber)
    (Hom.fiber
        ({ base := G.map f.base, fiber := f.fiber :
            { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.Hom
              { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F } } ≫
          { base := G.map g.base, fiber := g.fiber }) :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := G.map f.base, fiber := f.fiber :
                    { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.Hom
                      { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F } } ≫
                  { base := G.map g.base, fiber := g.fiber :
                    { base := G.obj Y.base, fiber := Y.fiber : Grothendieck F }.Hom
                      { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F } }))))
          { base := G.obj X.base, fiber := X.fiber : Grothendieck F }.fiber ⟶
        { base := G.obj Z.base, fiber := Z.fiber : Grothendieck F }.fiber)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
⊢ pre F (𝟭 C) = 𝟭 (Grothendieck (𝟭 C ⋙ F))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Grothendieck.pre, 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_1 : Functor.{v, w, u, w + 1} C (Type w)
G H : Functor.{v₁, v, u₁, u} D C
α : G ≅ H
X Y : Grothendieck (G ⋙ F)
f : X ⟶ Y
w_base :
  Hom.base
      ((pre F G).map f ≫
        Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            Y)) =
    Hom.base
      (Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            X) ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f)
w_fiber :
  eqToHom ⋯ ≫
      Hom.fiber
        ((pre F G).map f ≫
          Iso.hom
            ((fun (X : Grothendieck (G ⋙ F)) ↦
                ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
              Y)) =
    Hom.fiber
      (Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            X) ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f)
⊢ (pre F G).map f ≫
      Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          Y) =
    Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          X) ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f

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 H : Functor.{v₁, v, u₁, u} D C
α : G ≅ H
X Y : Grothendieck (G ⋙ F)
f : X ⟶ Y
⊢ Hom.base
      ((pre F G).map f ≫
        Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            Y)) =
    Hom.base
      (Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            X) ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f)

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_1 : Functor.{v, w, u, w + 1} C (Type w)
G H : Functor.{v₁, v, u₁, u} D C
α : G ≅ H
X Y : Grothendieck (G ⋙ F)
f : X ⟶ Y
⊢ eqToHom ⋯ ≫
      Hom.fiber
        ((pre F G).map f ≫
          Iso.hom
            ((fun (X : Grothendieck (G ⋙ F)) ↦
                ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
              Y)) =
    Hom.fiber
      (Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            X) ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f)

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₁, v, u₁, u} D C
H : C ⥤ Cat
α : F ⟶ H
⊢ pre F G ⋙ map α = map (G.whiskerLeft α) ⋙ pre H G

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.comp, CategoryTheory.Grothendieck.map, 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₁, v, u₁, u} D C
H : C ⥤ Cat
α : F ⟶ H
E : Type u_1
inst_2 : Category.{v_1, u_1} E
K : Grothendieck H ⥤ E
⊢ pre F G ⋙ map α ⋙ K = map (G.whiskerLeft α) ⋙ pre H G ⋙ K

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.comp, CategoryTheory.Grothendieck.map, 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
E : Type u_1
inst_2 : Category.{v_1, u_1} E
G : Functor.{v₁, v, u₁, u} D C
H : Functor.{v_1, v₁, u_1, u₁} E D
⊢ pre F (H ⋙ G) = pre (G ⋙ F) H ⋙ pre F G

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Grothendieck.pre, 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_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
refine :
  𝟭 (Grothendieck (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) ≅ pre F G.functor ⋙ preInv F G

Tactic:
refine (eqToIso ?_)
      ≪≫ (Grothendieck.preUnitIso F G |> isoWhiskerLeft (map _))
      ≪≫ (pre_comp_map_assoc G.functor _ _ |> Eq.symm |> eqToIso)

Premises used: CategoryTheory.Grothendieck.pre_comp_map_assoc, CategoryTheory.Grothendieck.preUnitIso, CategoryTheory.eqToIso, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Grothendieck.map, Eq.symm
-- 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
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) = map (𝟙 (G.functor ⋙ F))

Tactic:
map_id_eq.symm

Premises used: CategoryTheory.Grothendieck.map_id_eq, Eq.symm
-- 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
⊢ map (𝟙 (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))

Tactic:
?_
-- 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
⊢ map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))

Tactic:
map_comp_eq _ _

Premises used: CategoryTheory.Grothendieck.map_comp_eq
-- 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
_ :
  map (𝟙 (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))

Tactic:
calc
      _ = map (𝟙 _) := map_id_eq.symm
      _ = map _ := ?_
      _ = map _ ⋙ map _ := map_comp_eq _ _

Premises used: CategoryTheory.Grothendieck.map_comp_eq, CategoryTheory.CategoryStruct.id, CategoryTheory.Grothendieck.map_id_eq, CategoryTheory.Grothendieck.map, Eq.symm
-- 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_α : 𝟙 (G.functor ⋙ F) = G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)
⊢ map (𝟙 (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))

Tactic:
congr