no goals
C : Type ?u.2075
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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
rw [w_base]
case mk
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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
cases f
case mk.mk
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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✝ }
case mk
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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
cases g
case mk.mk.h.e_7
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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✝
case mk.mk
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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✝ }
congr
case mk.mk.h.e_7
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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✝
case mk.mk.h.e_7
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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✝
dsimp at w_base
no goals
case mk.mk.h.e_7
C : Type u_1
D : Type ?u.2078
inst✝¹ : Category C
inst✝ : Category 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✝
aesop_cat