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
X Y : Grothendieck F
f : X ⟶ Y
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
subst : f.fiber = eqToHom ⋯ ≫ f.fiber
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = eqToHom ⋯ ≫ f.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
subst : Hom.base (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.base (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ Hom.base (eqToHom ⋯) = eqToHom ⋯

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
X Y : Grothendieck F
h : X = Y
subst : (F.map (Hom.base (eqToHom ⋯))).toFunctor.obj X.fiber = X.fiber
⊢ (F.map (Hom.base (eqToHom h))).toFunctor.obj X.fiber = Y.fiber

Tactic:
subst h
-- 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
X : Grothendieck F
⊢ (F.map (Hom.base (eqToHom ⋯))).toFunctor.obj X.fiber = X.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
subst : Hom.fiber (eqToHom ⋯) = eqToHom ⋯
⊢ Hom.fiber (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ Hom.fiber (eqToHom ⋯) = eqToHom ⋯

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
X Y : Grothendieck F
hF : X = Y
subst : X.base = X.base
⊢ X.base = Y.base

Tactic:
subst hF
-- 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
X : Grothendieck F
⊢ X.base = X.base

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
X Y : Grothendieck F
hF : X = Y
subst : (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = X.fiber
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = Y.fiber

Tactic:
subst hF
-- 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
X : Grothendieck F
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = X.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
subst : eqToHom ⋯ = { base := eqToHom ⋯, fiber := eqToHom ⋯ : X.Hom X }
⊢ eqToHom hF = { base := eqToHom ⋯, fiber := eqToHom ⋯ : X.Hom Y }

Tactic:
subst hF
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ eqToHom ⋯ = { base := eqToHom ⋯, fiber := eqToHom ⋯ : X.Hom X }

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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
rw : (F.map e₁.hom ≫ F.map e₁.inv).toFunctor.obj X.fiber = X.fiber
rw₁ : (F.map (e₁.hom ≫ e₁.inv)).toFunctor.obj X.fiber = X.fiber
rw₂ : (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber
rw₃ : (Cat.Hom.toFunctor (𝟙 (F.obj X.base))).obj X.fiber = X.fiber
rw₄ rw₅ : X.fiber = X.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber

Tactic:
rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Cat.Hom.id_obj, CategoryTheory.Functor.map_id, CategoryTheory.Cat.Hom.comp_obj, 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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ Hom.base
      ({ base := e₁.hom, fiber := e₂.hom : X.Hom Y } ≫
        { base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ }) =
    Hom.base (𝟙 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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ eqToHom ⋯ ≫
      Hom.fiber
        ({ base := e₁.hom, fiber := e₂.hom : X.Hom Y } ≫
          { base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ : Y.Hom X }) =
    Hom.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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ Hom.base
      ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ : Y.Hom X } ≫
        { base := e₁.hom, fiber := e₂.hom }) =
    Hom.base (𝟙 Y)

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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj Y.base) : Type u₂))
      (obj (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) Y.fiber)
      (obj (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) ((F.map e₁.hom).toFunctor.obj X.fiber)))
    (map (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) e₂.inv)
    (eqToHom ⋯ ≫ map (Cat.Hom.toFunctor (𝟙 (F.obj Y.base))) e₂.inv ≫ eqToHom ⋯)

Tactic:
have := Functor.congr_hom congr($((F.mapIso e₁).inv_hom_id).toFunctor) e₂.inv
-- 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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
this :
  Eq (α :=
    Quiver.Hom (V := (↑(F.obj Y.base) : Type u₂))
      (obj (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) Y.fiber)
      (obj (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) ((F.map e₁.hom).toFunctor.obj X.fiber)))
    (map (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) e₂.inv)
    (eqToHom ⋯ ≫ map (Cat.Hom.toFunctor (𝟙 (F.obj Y.base))) e₂.inv ≫ eqToHom ⋯)
⊢ eqToHom ⋯ ≫
      Hom.fiber
        ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ : Y.Hom X } ≫
          { base := e₁.hom, fiber := e₂.hom : X.Hom Y }) =
    Hom.fiber (𝟙 Y)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
α : F ⟶ G
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ { base := (f ≫ g).base,
        fiber :=
          (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (f ≫ g).fiber :
        { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
          { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }.base =
    Hom.base
      ({ base := f.base,
          fiber :=
            (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
          { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
            { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
        { base := g.base,
          fiber :=
            (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
X : Grothendieck F
⊢ (map α).obj X = { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
X Y : Grothendieck F
f : X ⟶ Y
⊢ ((map α).map f).base =
    { base := f.base,
        fiber :=
          (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber }.base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
X Y : Grothendieck F
f : X ⟶ Y
⊢ Eq (α :=
    (G.map
              { base := f.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                  ((map α).obj X).Hom ((map α).obj Y) }.base).toFunctor.obj
        ((map α).obj X).fiber ⟶
      ((map α).obj Y).fiber)
    (eqToHom ⋯ ≫ ((map α).map f).fiber)
    { base := f.base,
        fiber :=
          (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber }.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map α).map f =
    { base := f.base,
      fiber := (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber }

Tactic:
apply Grothendieck.ext _ _ (by simp) (by simp)

Premises used: CategoryTheory.Grothendieck.ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
⊢ map α ⋙ forget G = forget F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Grothendieck.forget, rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
h_obj : ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = obj (𝟭 (Grothendieck F)) X
h_map :
  autoParam
    (∀ (X Y : Grothendieck F) (f : X ⟶ Y),
      (map (𝟙 F)).map f = eqToHom ⋯ ≫ Functor.map (𝟭 (Grothendieck F)) f ≫ eqToHom ⋯)
    ext._auto_1
⊢ map (𝟙 F) = 𝟭 (Grothendieck F)

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (map (𝟙 F)).obj X = obj (𝟭 (Grothendieck F)) X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
h_map : { base := f.base, fiber := f.fiber : ((map (𝟙 F)).obj X).Hom ((map (𝟙 F)).obj Y) } = f
⊢ (map (𝟙 F)).map f = eqToHom ⋯ ≫ Functor.map (𝟭 (Grothendieck F)) f ≫ eqToHom ⋯

Tactic:
simp [map_map]

Premises used: CategoryTheory.Grothendieck.map_map
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := f.fiber : ((map (𝟙 F)).obj X).Hom ((map (𝟙 F)).obj Y) } = f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
h_obj : ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X
h_map :
  autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯)
    ext._auto_1
⊢ map (α ≫ β) = map α ⋙ map β

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
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
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
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, map_obj_fiber, NatTrans.comp_app, Cat.Hom.comp_toFunctor,
      comp_obj, Cat.Hom₂.eqToHom_toNatTrans, eqToHom_app, Functor.comp_map, eqToHom_refl, map_comp,
      eqToHom_map, eqToHom_trans_assoc, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Grothendieck.map_map, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Grothendieck.map_obj_fiber, CategoryTheory.Grothendieck.map_obj_base, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_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, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
x : Grothendieck (F ⋙ Cat.asSmallFunctor)
w_fiber :
  CategoryStruct.comp (Y :=
      (F.map
              { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
                  { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
                    { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base).toFunctor.obj
        { base := x.base, fiber := obj AsSmall.down x.fiber }.fiber)
      (eqToHom ⋯) { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) }.fiber =
    Hom.fiber (𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F })
w_base :
  { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
        { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
          { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base =
    Hom.base (𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber })
⊢ { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
      { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
        { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } } =
    𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber }

Tactic:
apply 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 : Functor.{v, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
x : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ CategoryStruct.comp (Y :=
      (F.map
              { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
                  { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
                    { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base).toFunctor.obj
        { base := x.base, fiber := obj AsSmall.down x.fiber }.fiber)
      (eqToHom ⋯) { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) }.fiber =
    Hom.fiber (𝟙 { base := x.base, fiber := obj AsSmall.down 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 : Functor.{v, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
x : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
        { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
          { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base =
    Hom.base (𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber })

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, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
X Y Z : Grothendieck (F ⋙ Cat.asSmallFunctor)
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ { base := (x ≫ x_1).base, fiber := Functor.map AsSmall.down (x ≫ x_1).fiber :
        { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
          { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } }.base =
    Hom.base
      ({ base := x.base, fiber := Functor.map AsSmall.down x.fiber :
          { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
            { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
        { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber })

Tactic:
simp [down_comp]

Premises used: CategoryTheory.down_comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
⊢ Hom.base
      ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
        Iso.hom
          ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
              (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
                (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
            Y)) =
    Hom.base
      (Iso.hom
          ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
              (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
                (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
            X) ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f)

Tactic:
simp [compAsSmallFunctorEquivalenceInverse]

Premises used: CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
w_fiber :
  HEq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((G.map (𝟙 Y.base)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (β :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
    (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))
⊢ Eq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((G.map (𝟙 Y.base)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (CategoryStruct.comp (Y :=
      obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))) (eqToHom ⋯)
      (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down) ≫ eqToHom ⋯))

Tactic:
simp only [conj_eqToHom_iff_heq']

Premises used: CategoryTheory.conj_eqToHom_iff_heq'
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
w_fiber :
  HEq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up
        ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (β :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
    (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))
⊢ HEq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((G.map (𝟙 Y.base)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (β :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
    (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))

Tactic:
rw [G.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 G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
⊢ HEq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up
        ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (β :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
    (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))

Tactic:
simp