[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.2082, u_1} C
inst✝ : Category.{?u.2086, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : Hom X Y
w_base : f.base = g.base
⊢ (F.map g.base).obj X.fiber = (F.map f.base).obj X.fiber
[PROOFSTEP]
rw [w_base]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.2086, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : Hom X Y
w_base : f.base = g.base
w_fiber : eqToHom (_ : (F.map g.base).obj X.fiber = (F.map f.base).obj X.fiber) ≫ f.fiber = g.fiber
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.2086, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
g : Hom X Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber :
  eqToHom (_ : (F.map g.base).obj X.fiber = (F.map { base := base✝, fiber := fiber✝ }.base).obj X.fiber) ≫
      { base := base✝, fiber := fiber✝ }.fiber =
    g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.2086, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber :
  eqToHom
        (_ :
          (F.map { base := base✝, fiber := fiber✝ }.base).obj X.fiber =
            (F.map { base := base✝¹, fiber := fiber✝¹ }.base).obj X.fiber) ≫
      { base := base✝¹, fiber := fiber✝¹ }.fiber =
    { base := base✝, fiber := fiber✝ }.fiber
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.h.e_7
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.2086, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : { base := base✝¹, fiber := fiber✝¹ }.base = { base := base✝, fiber := fiber✝ }.base
w_fiber :
  eqToHom
        (_ :
          (F.map { base := base✝, fiber := fiber✝ }.base).obj X.fiber =
            (F.map { base := base✝¹, fiber := fiber✝¹ }.base).obj X.fiber) ≫
      { base := base✝¹, fiber := fiber✝¹ }.fiber =
    { base := base✝, fiber := fiber✝ }.fiber
⊢ HEq fiber✝¹ fiber✝
[PROOFSTEP]
dsimp at w_base 
[GOAL]
case mk.mk.h.e_7
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.2086, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
base✝¹ : X.base ⟶ Y.base
fiber✝¹ : (F.map base✝¹).obj X.fiber ⟶ Y.fiber
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).obj X.fiber ⟶ Y.fiber
w_base : base✝¹ = base✝
w_fiber :
  eqToHom
        (_ :
          (F.map { base := base✝, fiber := fiber✝ }.base).obj X.fiber =
            (F.map { base := base✝¹, fiber := fiber✝¹ }.base).obj X.fiber) ≫
      { base := base✝¹, fiber := fiber✝¹ }.fiber =
    { base := base✝, fiber := fiber✝ }.fiber
⊢ HEq fiber✝¹ fiber✝
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.4816, u_1} C
inst✝ : Category.{?u.4820, u_2} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X.base)).obj X.fiber = X.fiber
[PROOFSTEP]
erw [CategoryTheory.Functor.map_id, Functor.id_obj X.fiber]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.6425, u_1} C
inst✝ : Category.{?u.6429, u_2} D
F : C ⥤ Cat
X Y Z : Grothendieck F
f : Hom X Y
g : Hom Y Z
⊢ (F.map (f.base ≫ g.base)).obj X.fiber = (F.map g.base).obj ((F.map f.base).obj X.fiber)
[PROOFSTEP]
erw [Functor.map_comp, Functor.comp_obj]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ comp (id X) f = f
[PROOFSTEP]
ext
[GOAL]
case w_base
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (comp (id X) f).base = f.base
[PROOFSTEP]
simp
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom (_ : (F.map f.base).obj X.fiber = (F.map (comp (id X) f).base).obj X.fiber) ≫ (comp (id X) f).fiber = f.fiber
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ comp f (id Y) = f
[PROOFSTEP]
ext
[GOAL]
case w_base
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (comp f (id Y)).base = f.base
[PROOFSTEP]
simp
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom (_ : (F.map f.base).obj X.fiber = (F.map (comp f (id Y)).base).obj X.fiber) ≫ (comp f (id Y)).fiber = f.fiber
[PROOFSTEP]
dsimp
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom (_ : (F.map f.base).obj X.fiber = (F.map (f.base ≫ 𝟙 Y.base)).obj X.fiber) ≫
      eqToHom (_ : (F.map (f.base ≫ (id Y).base)).obj X.fiber = (F.map (id Y).base).obj ((F.map f.base).obj X.fiber)) ≫
        (F.map (𝟙 Y.base)).map f.fiber ≫ eqToHom (_ : (F.map (𝟙 Y.base)).obj Y.fiber = Y.fiber) =
    f.fiber
[PROOFSTEP]
rw [← NatIso.naturality_2 (eqToIso (F.map_id Y.base)) f.fiber]
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom (_ : (F.map f.base).obj X.fiber = (F.map (f.base ≫ 𝟙 Y.base)).obj X.fiber) ≫
      eqToHom (_ : (F.map (f.base ≫ (id Y).base)).obj X.fiber = (F.map (id Y).base).obj ((F.map f.base).obj X.fiber)) ≫
        (NatTrans.app (eqToIso (_ : F.map (𝟙 Y.base) = 𝟙 (F.obj Y.base))).hom ((F.map f.base).obj X.fiber) ≫
            (𝟙 (F.obj Y.base)).map f.fiber ≫
              NatTrans.app (eqToIso (_ : F.map (𝟙 Y.base) = 𝟙 (F.obj Y.base))).inv Y.fiber) ≫
          eqToHom (_ : (F.map (𝟙 Y.base)).obj Y.fiber = Y.fiber) =
    f.fiber
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ comp (comp f g) h = comp f (comp g h)
[PROOFSTEP]
ext
[GOAL]
case w_base
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (comp (comp f g) h).base = (comp f (comp g h)).base
[PROOFSTEP]
simp
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ eqToHom (_ : (F.map (comp f (comp g h)).base).obj W.fiber = (F.map (comp (comp f g) h).base).obj W.fiber) ≫
      (comp (comp f g) h).fiber =
    (comp f (comp g h)).fiber
[PROOFSTEP]
dsimp
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ eqToHom (_ : (F.map (f.base ≫ g.base ≫ h.base)).obj W.fiber = (F.map ((f.base ≫ g.base) ≫ h.base)).obj W.fiber) ≫
      eqToHom
          (_ :
            (F.map ((comp f g).base ≫ h.base)).obj W.fiber = (F.map h.base).obj ((F.map (comp f g).base).obj W.fiber)) ≫
        (F.map h.base).map
            (eqToHom (_ : (F.map (f.base ≫ g.base)).obj W.fiber = (F.map g.base).obj ((F.map f.base).obj W.fiber)) ≫
              (F.map g.base).map f.fiber ≫ g.fiber) ≫
          h.fiber =
    eqToHom
        (_ :
          (F.map (f.base ≫ (comp g h).base)).obj W.fiber = (F.map (comp g h).base).obj ((F.map f.base).obj W.fiber)) ≫
      (F.map (g.base ≫ h.base)).map f.fiber ≫
        eqToHom (_ : (F.map (g.base ≫ h.base)).obj X.fiber = (F.map h.base).obj ((F.map g.base).obj X.fiber)) ≫
          (F.map h.base).map g.fiber ≫ h.fiber
[PROOFSTEP]
rw [← NatIso.naturality_2 (eqToIso (F.map_comp _ _)) f.fiber]
[GOAL]
case w_fiber
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.9208, u_1} C
inst✝ : Category.{?u.9212, u_2} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ eqToHom (_ : (F.map (f.base ≫ g.base ≫ h.base)).obj W.fiber = (F.map ((f.base ≫ g.base) ≫ h.base)).obj W.fiber) ≫
      eqToHom
          (_ :
            (F.map ((comp f g).base ≫ h.base)).obj W.fiber = (F.map h.base).obj ((F.map (comp f g).base).obj W.fiber)) ≫
        (F.map h.base).map
            (eqToHom (_ : (F.map (f.base ≫ g.base)).obj W.fiber = (F.map g.base).obj ((F.map f.base).obj W.fiber)) ≫
              (F.map g.base).map f.fiber ≫ g.fiber) ≫
          h.fiber =
    eqToHom
        (_ :
          (F.map (f.base ≫ (comp g h).base)).obj W.fiber = (F.map (comp g h).base).obj ((F.map f.base).obj W.fiber)) ≫
      (NatTrans.app (eqToIso (_ : F.map (g.base ≫ h.base) = F.map g.base ≫ F.map h.base)).hom
            ((F.map f.base).obj W.fiber) ≫
          (F.map g.base ≫ F.map h.base).map f.fiber ≫
            NatTrans.app (eqToIso (_ : F.map (g.base ≫ h.base) = F.map g.base ≫ F.map h.base)).inv X.fiber) ≫
        eqToHom (_ : (F.map (g.base ≫ h.base)).obj X.fiber = (F.map h.base).obj ((F.map g.base).obj X.fiber)) ≫
          (F.map h.base).map g.fiber ≫ h.fiber
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.18727, u_1} C
inst✝ : Category.{?u.18731, u_2} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X).base).obj X.fiber = X.fiber
[PROOFSTEP]
erw [CategoryTheory.Functor.map_id, Functor.id_obj X.fiber]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.20428, u_1} C
inst✝ : Category.{?u.20432, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ (F.map f.base).obj X.fiber = (F.map g.base).obj X.fiber
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.20428, u_1} C
inst✝ : Category.{?u.20432, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (F.map f.base).obj X.fiber = (F.map f.base).obj X.fiber
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.20432, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ f.fiber = eqToHom (_ : (F.map f.base).obj X.fiber = (F.map g.base).obj X.fiber) ≫ g.fiber
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.20432, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = eqToHom (_ : (F.map f.base).obj X.fiber = (F.map f.base).obj X.fiber) ≫ f.fiber
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{?u.20432, u_2} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = 𝟙 ((F.map f.base).obj X.fiber) ≫ f.fiber
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
X : Grothendieck (G ⋙ typeToCat)
⊢ (𝟭 (Grothendieck (G ⋙ typeToCat))).obj X ≅ (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj X
[PROOFSTEP]
rcases X with ⟨_, ⟨⟩⟩
[GOAL]
case mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝ : C
as✝ : G.obj base✝
⊢ (𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base✝, fiber := { as := as✝ } } ≅
    (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj { base := base✝, fiber := { as := as✝ } }
[PROOFSTEP]
exact Iso.refl _
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
⊢ ∀ {X Y : Grothendieck (G ⋙ typeToCat)} (f : X ⟶ Y),
    (𝟭 (Grothendieck (G ⋙ typeToCat))).map f ≫
        ((fun X =>
              Grothendieck.casesOn X fun base fiber =>
                Discrete.casesOn fiber fun as =>
                  Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
            Y).hom =
      ((fun X =>
              Grothendieck.casesOn X fun base fiber =>
                Discrete.casesOn fiber fun as =>
                  Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
            X).hom ≫
        (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map f
[PROOFSTEP]
rintro ⟨_, ⟨⟩⟩ ⟨_, ⟨⟩⟩ ⟨base, ⟨⟨f⟩⟩⟩
[GOAL]
case mk.mk.mk.mk.mk.up.up
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ (𝟭 (Grothendieck (G ⋙ typeToCat))).map { base := base, fiber := { down := { down := f } } } ≫
      ((fun X =>
            Grothendieck.casesOn X fun base fiber =>
              Discrete.casesOn fiber fun as =>
                Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
          { base := base✝, fiber := { as := as✝ } }).hom =
    ((fun X =>
            Grothendieck.casesOn X fun base fiber =>
              Discrete.casesOn fiber fun as =>
                Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
          { base := base✝¹, fiber := { as := as✝¹ } }).hom ≫
      (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map
        { base := base, fiber := { down := { down := f } } }
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.mk.mk.mk.up.up
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ { base := base, fiber := { down := { down := f } } } ≫ 𝟙 { base := base✝, fiber := { as := as✝ } } =
    𝟙 { base := base✝¹, fiber := { as := as✝¹ } } ≫
      (grothendieckTypeToCatInverse G).map
        ((grothendieckTypeToCatFunctor G).map { base := base, fiber := { down := { down := f } } })
[PROOFSTEP]
simp
[GOAL]
case mk.mk.mk.mk.mk.up.up
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ { base := base, fiber := { down := { down := f } } } =
    (grothendieckTypeToCatInverse G).map
      ((grothendieckTypeToCatFunctor G).map { base := base, fiber := { down := { down := f } } })
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
X : Functor.Elements G
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ (𝟭 (Functor.Elements G)).obj X
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝ : C
snd✝ : G.obj fst✝
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj { fst := fst✝, snd := snd✝ } ≅
    (𝟭 (Functor.Elements G)).obj { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
exact Iso.refl _
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
⊢ ∀ {X Y : Functor.Elements G} (f : X ⟶ Y),
    (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).map f ≫
        ((fun X =>
              Sigma.casesOn (motive := fun t =>
                X = t →
                  ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅
                    (𝟭 (Functor.Elements G)).obj X))
                X
                (fun fst snd h =>
                  (_ : { fst := fst, snd := snd } = X) ▸
                    Iso.refl
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
                        { fst := fst, snd := snd }))
                (_ : X = X))
            Y).hom =
      ((fun X =>
              Sigma.casesOn (motive := fun t =>
                X = t →
                  ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅
                    (𝟭 (Functor.Elements G)).obj X))
                X
                (fun fst snd h =>
                  (_ : { fst := fst, snd := snd } = X) ▸
                    Iso.refl
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
                        { fst := fst, snd := snd }))
                (_ : X = X))
            X).hom ≫
        (𝟭 (Functor.Elements G)).map f
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨f, e⟩
[GOAL]
case mk.mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : { fst := fst✝¹, snd := snd✝¹ }.fst ⟶ { fst := fst✝, snd := snd✝ }.fst
e : G.map f { fst := fst✝¹, snd := snd✝¹ }.snd = { fst := fst✝, snd := snd✝ }.snd
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).map { val := f, property := e } ≫
      ((fun X =>
            Sigma.casesOn (motive := fun t =>
              X = t →
                ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅
                  (𝟭 (Functor.Elements G)).obj X))
              X
              (fun fst snd h =>
                (_ : { fst := fst, snd := snd } = X) ▸
                  Iso.refl
                    ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj { fst := fst, snd := snd }))
              (_ : X = X))
          { fst := fst✝, snd := snd✝ }).hom =
    ((fun X =>
            Sigma.casesOn (motive := fun t =>
              X = t →
                ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅
                  (𝟭 (Functor.Elements G)).obj X))
              X
              (fun fst snd h =>
                (_ : { fst := fst, snd := snd } = X) ▸
                  Iso.refl
                    ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj { fst := fst, snd := snd }))
              (_ : X = X))
          { fst := fst✝¹, snd := snd✝¹ }).hom ≫
      (𝟭 (Functor.Elements G)).map { val := f, property := e }
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : { fst := fst✝¹, snd := snd✝¹ }.fst ⟶ { fst := fst✝, snd := snd✝ }.fst
e : G.map f { fst := fst✝¹, snd := snd✝¹ }.snd = { fst := fst✝, snd := snd✝ }.snd
⊢ (grothendieckTypeToCatFunctor G).map ((grothendieckTypeToCatInverse G).map { val := f, property := e }) ≫
      𝟙 ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj { fst := fst✝, snd := snd✝ })) =
    𝟙 ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj { fst := fst✝¹, snd := snd✝¹ })) ≫
      { val := f, property := e }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : { fst := fst✝¹, snd := snd✝¹ }.fst ⟶ { fst := fst✝, snd := snd✝ }.fst
e : G.map f { fst := fst✝¹, snd := snd✝¹ }.snd = { fst := fst✝, snd := snd✝ }.snd
⊢ (grothendieckTypeToCatFunctor G).map ((grothendieckTypeToCatInverse G).map { val := f, property := e }) =
    { val := f, property := e }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
⊢ ∀ (X : Grothendieck (G ⋙ typeToCat)),
    (grothendieckTypeToCatFunctor G).map
          (NatTrans.app
            (NatIso.ofComponents fun X =>
                Grothendieck.casesOn X fun base fiber =>
                  Discrete.casesOn fiber fun as =>
                    Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom
            X) ≫
        NatTrans.app
          (NatIso.ofComponents fun X =>
              Sigma.casesOn (motive := fun t =>
                X = t →
                  ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅
                    (𝟭 (Functor.Elements G)).obj X))
                X
                (fun fst snd h =>
                  (_ : { fst := fst, snd := snd } = X) ▸
                    Iso.refl
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
                        { fst := fst, snd := snd }))
                (_ : X = X)).hom
          ((grothendieckTypeToCatFunctor G).obj X) =
      𝟙 ((grothendieckTypeToCatFunctor G).obj X)
[PROOFSTEP]
rintro ⟨_, ⟨⟩⟩
[GOAL]
case mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝ : C
as✝ : G.obj base✝
⊢ (grothendieckTypeToCatFunctor G).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              Grothendieck.casesOn X fun base fiber =>
                Discrete.casesOn fiber fun as =>
                  Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom
          { base := base✝, fiber := { as := as✝ } }) ≫
      NatTrans.app
        (NatIso.ofComponents fun X =>
            Sigma.casesOn (motive := fun t =>
              X = t →
                ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅
                  (𝟭 (Functor.Elements G)).obj X))
              X
              (fun fst snd h =>
                (_ : { fst := fst, snd := snd } = X) ▸
                  Iso.refl
                    ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj { fst := fst, snd := snd }))
              (_ : X = X)).hom
        ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }) =
    𝟙 ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝ : C
as✝ : G.obj base✝
⊢ (grothendieckTypeToCatFunctor G).map (𝟙 { base := base✝, fiber := { as := as✝ } }) ≫
      (Sigma.rec (motive := fun t =>
          (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } } = t →
            ((grothendieckTypeToCatFunctor G).obj
                ((grothendieckTypeToCatInverse G).obj
                  ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })) ≅
              (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }))
          (fun fst snd h =>
            (_ :
                { fst := fst, snd := snd } =
                  (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }) ▸
              Iso.refl
                ((grothendieckTypeToCatFunctor G).obj
                  ((grothendieckTypeToCatInverse G).obj { fst := fst, snd := snd })))
          ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })
          (_ :
            (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } } =
              (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })).hom =
    𝟙 ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })
[PROOFSTEP]
simp
[GOAL]
case mk.mk
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.34627, u_1} C
inst✝ : Category.{?u.34631, u_2} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝ : C
as✝ : G.obj base✝
⊢ (Sigma.rec (motive := fun t =>
        (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } } = t →
          ((grothendieckTypeToCatFunctor G).obj
              ((grothendieckTypeToCatInverse G).obj
                ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })) ≅
            (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }))
        (fun fst snd h =>
          (_ :
              { fst := fst, snd := snd } =
                (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }) ▸
            Iso.refl
              ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj { fst := fst, snd := snd })))
        ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })
        (_ :
          (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } } =
            (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })).hom =
    𝟙 ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })
[PROOFSTEP]
rfl
