[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


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Balanced C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
fmono : Mono f
fepi : Epi f
⊢ IsIso f
[PROOFSTEP]
rw [← Quiver.Hom.op_unop f]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Balanced C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
fmono : Mono f
fepi : Epi f
⊢ IsIso f.unop.op
[PROOFSTEP]
exact isIso_of_op _


[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.op ≫ g.op = h.op ≫ f.op
[PROOFSTEP]
simp only [← op_comp, p.w]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.unop ≫ g.unop = h.unop ≫ f.unop
[PROOFSTEP]
simp only [← unop_comp, p.w]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
D : Type u_2
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i
[PROOFSTEP]
simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w
[GOAL]
C : Type u_1
inst✝ : Category.{?u.5324, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ p.op ≫ l.l.op = g.op
[PROOFSTEP]
rw [← op_comp, l.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.5324, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ l.l.op ≫ i.op = f.op
[PROOFSTEP]
rw [← op_comp, l.fac_left]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.6224, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ p.unop ≫ l.l.unop = g.unop
[PROOFSTEP]
rw [← unop_comp, l.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.6224, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : LiftStruct sq
⊢ l.l.unop ≫ i.unop = f.unop
[PROOFSTEP]
rw [← unop_comp, l.fac_left]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7227, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse unop op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7227, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse unop op
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.8602, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.LeftInverse op unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.8602, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Function.RightInverse op unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.10063, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : LiftStruct sq
⊢ l₁ = l₂
[PROOFSTEP]
ext
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10063, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : LiftStruct sq
⊢ l₁.l = l₂.l
[PROOFSTEP]
rw [← cancel_epi i]
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10063, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : LiftStruct sq
⊢ i ≫ l₁.l = i ≫ l₂.l
[PROOFSTEP]
simp only [LiftStruct.fac_left]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.10732, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Mono p
l₁ l₂ : LiftStruct sq
⊢ l₁ = l₂
[PROOFSTEP]
ext
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10732, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Mono p
l₁ l₂ : LiftStruct sq
⊢ l₁.l = l₂.l
[PROOFSTEP]
rw [← cancel_mono p]
[GOAL]
case l
C : Type u_1
inst✝¹ : Category.{?u.10732, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Mono p
l₁ l₂ : LiftStruct sq
⊢ l₁.l ≫ p = l₂.l ≫ p
[PROOFSTEP]
simp only [LiftStruct.fac_right]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ Nonempty (LiftStruct sq)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq → Nonempty (LiftStruct sq)
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) → HasLift sq
[PROOFSTEP]
exacts [fun h => h.exists_lift, fun h => mk h]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ HasLift (_ : CommSq g.op p.op i.op f.op)
[PROOFSTEP]
rw [iff, iff]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) ↔ Nonempty (LiftStruct (_ : CommSq g.op p.op i.op f.op))
[PROOFSTEP]
exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
sq✝ : CommSq f✝ i✝ p✝ g✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ HasLift (_ : CommSq g.unop p.unop i.unop f.unop)
[PROOFSTEP]
rw [iff, iff]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
sq✝ : CommSq f✝ i✝ p✝ g✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) ↔ Nonempty (LiftStruct (_ : CommSq g.unop p.unop i.unop f.unop))
[PROOFSTEP]
exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit
X : C
⊢ F.obj X = G.obj X
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit
X : C
⊢ F.obj X = G.obj X
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
[PROOFSTEP]
refine' ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro _⟩
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
⊢ Unique (x ⟶ y)
[PROOFSTEP]
let f : x ⟶ y := by
  have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
  have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
  exact hx ≫ hy
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
⊢ x ⟶ y
[PROOFSTEP]
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
⊢ x ⟶ h.inverse.obj { as := PUnit.unit }
[PROOFSTEP]
convert h.unit.app x
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y
[PROOFSTEP]
have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ h.inverse.obj { as := PUnit.unit } ⟶ y
[PROOFSTEP]
convert h.unitInv.app y
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit } ⟶ y
⊢ x ⟶ y
[PROOFSTEP]
exact hx ≫ hy
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
⊢ Unique (x ⟶ y)
[PROOFSTEP]
suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
⊢ Subsingleton (x ⟶ y)
[PROOFSTEP]
have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y :=
  by
  intro z
  simp [congrArg (· ≫ h.unitInv.app y) (h.unit.naturality z)]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
⊢ ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
intro z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
z : x ⟶ y
⊢ z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
simp [congrArg (· ≫ h.unitInv.app y) (h.unit.naturality z)]
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
⊢ Subsingleton (x ⟶ y)
[PROOFSTEP]
apply Subsingleton.intro
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
⊢ ∀ (a b : x ⟶ y), a = b
[PROOFSTEP]
intro a b
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ a = b
[PROOFSTEP]
rw [this a, this b]
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map a ≫ NatTrans.app (Equivalence.unitInv h) y =
    NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map b ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
simp only [Functor.comp_map]
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ NatTrans.app (Equivalence.unit h) x ≫ h.inverse.map (h.functor.map a) ≫ NatTrans.app (Equivalence.unitInv h) y =
    NatTrans.app (Equivalence.unit h) x ≫ h.inverse.map (h.functor.map b) ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
congr 3
[GOAL]
case mp.intro.allEq.e_a.e_a.e_a
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b
[PROOFSTEP]
apply ULift.ext
[GOAL]
case mp.intro.allEq.e_a.e_a.e_a.h
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ (h.functor.map a).down = (h.functor.map b).down
[PROOFSTEP]
simp
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit)
[PROOFSTEP]
rintro ⟨⟨p⟩, h⟩
[GOAL]
case mpr.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
⊢ Nonempty (C ≌ Discrete PUnit)
[PROOFSTEP]
haveI := fun x y => (h x y).some
[GOAL]
case mpr.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty (C ≌ Discrete PUnit)
[PROOFSTEP]
refine'
  Nonempty.intro
    (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩) ((@Functor.const <| Discrete PUnit).obj p) ?_
      (by apply Functor.punitExt))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ (Functor.const (Discrete PUnit)).obj p ⋙ (Functor.const C).obj { as := PUnit.unit } ≅ 𝟭 (Discrete PUnit)
[PROOFSTEP]
apply Functor.punitExt
[GOAL]
case mpr.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ 𝟭 C ≅ (Functor.const C).obj { as := PUnit.unit } ⋙ (Functor.const (Discrete PUnit)).obj p
[PROOFSTEP]
exact
  NatIso.ofComponents fun _ =>
    { hom := default
      inv := default }


[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X : Paths V
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (𝟙 X) =
    𝟙
      ({ obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.obj
        X)
[PROOFSTEP]
rfl
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map g
[PROOFSTEP]
induction' g with _ _ g' p ih _ _ _
[GOAL]
case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.nil) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        Quiver.Path.nil
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.nil) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.cons g' p) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        (Quiver.Path.cons g' p)
[PROOFSTEP]
have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
⊢ f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
[PROOFSTEP]
apply Quiver.Path.comp_cons
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
this : f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ Quiver.Path.cons g' p) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        (Quiver.Path.cons g' p)
[PROOFSTEP]
rw [this]
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (f ≫ g') =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        g'
this : f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
⊢ { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
      (Quiver.Path.cons (f ≫ g') p) =
    { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map f ≫
      { obj := φ.obj, map := fun {X Y} f => Quiver.Path.rec (𝟙 (φ.obj X)) (fun {b c} x f ihp => ihp ≫ φ.map f) f }.map
        (Quiver.Path.cons g' p)
[PROOFSTEP]
simp only at ih ⊢
[GOAL]
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.1599
inst✝ : Category.{?u.1600, ?u.1599} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) g'
this : f ≫ Quiver.Path.cons g' p = Quiver.Path.cons (f ≫ g') p
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) (f ≫ g') ≫ φ.map p =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp => ihp ≫ φ.map f) g' ≫ φ.map p
[PROOFSTEP]
rw [ih, Category.assoc]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map (Quiver.Hom.toPath f) = φ.map f
[PROOFSTEP]
dsimp [Quiver.Hom.toPath, lift]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
[PROOFSTEP]
simp
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ of ⋙q (lift φ).toPrefunctor = φ
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X : V
⊢ (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of ⋙q (lift φ).toPrefunctor).map f =
      Eq.recOn (_ : φ.obj Y = (of ⋙q (lift φ).toPrefunctor).obj Y)
        (Eq.recOn (_ : φ.obj X = (of ⋙q (lift φ).toPrefunctor).obj X) (φ.map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (of ⋙q (lift φ).toPrefunctor).map f =
    Eq.recOn (_ : φ.obj Y = (of ⋙q (lift φ).toPrefunctor).obj Y)
      (Eq.recOn (_ : φ.obj X = (of ⋙q (lift φ).toPrefunctor).obj X) (φ.map f))
[PROOFSTEP]
rcases φ with ⟨φo, φm⟩
[GOAL]
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).map f =
    Eq.recOn (_ : { obj := φo, map := φm }.obj Y = (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).obj Y)
      (Eq.recOn (_ : { obj := φo, map := φm }.obj X = (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).obj X)
        ({ obj := φo, map := φm }.map f))
[PROOFSTEP]
dsimp [lift, Quiver.Hom.toPath]
[GOAL]
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ 𝟙 (φo X) ≫ φm f = φm f
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
Φ : Paths V ⥤ C
hΦ : of ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ
[PROOFSTEP]
subst_vars
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ Φ = lift (of ⋙q Φ.toPrefunctor)
[PROOFSTEP]
fapply Functor.ext
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam
    (∀ (X Y : Paths V) (f : X ⟶ Y),
      Φ.map f =
        eqToHom (_ : Φ.obj X = Φ.obj X) ≫
          (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom (_ : (lift (of ⋙q Φ.toPrefunctor)).obj Y = Φ.obj Y))
    _auto✝
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f =
    eqToHom (_ : Φ.obj X = Φ.obj X) ≫
      (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom (_ : (lift (of ⋙q Φ.toPrefunctor)).obj Y = Φ.obj Y)
[PROOFSTEP]
dsimp [lift]
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f =
    𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) f ≫ 𝟙 (Φ.obj Y)
[PROOFSTEP]
induction' f with _ _ p f' ih
[GOAL]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) Quiver.Path.nil ≫
        𝟙 (Φ.obj X)
[PROOFSTEP]
simp only [Category.comp_id]
[GOAL]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)
[PROOFSTEP]
apply Functor.map_id
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih :
  Φ.map p =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p ≫ 𝟙 (Φ.obj b✝)
⊢ Φ.map (Quiver.Path.cons p f') =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) (Quiver.Path.cons p f') ≫
        𝟙 (Φ.obj c✝)
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp] at ih ⊢
  -- porting note: Had to do substitute `p.cons f'` and `f'.toPath` by their fully qualified
        -- versions in this `have` clause (elsewhere too).
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p
⊢ Φ.map (Quiver.Path.cons p f') =
    Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p ≫
      Φ.map (Quiver.Hom.toPath f')
[PROOFSTEP]
have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
  convert Functor.map_comp Φ p (Quiver.Hom.toPath f')
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p
⊢ Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f')
[PROOFSTEP]
convert Functor.map_comp Φ p (Quiver.Hom.toPath f')
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p
this : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f')
⊢ Φ.map (Quiver.Path.cons p f') =
    Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map (Quiver.Hom.toPath f)) p ≫
      Φ.map (Quiver.Hom.toPath f')
[PROOFSTEP]
rw [this, ih]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
⊢ F = G
[PROOFSTEP]
fapply Functor.ext
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
⊢ ∀ (X : Paths V), F.obj X = G.obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X : Paths V
⊢ F.obj X = G.obj X
[PROOFSTEP]
rw [h_obj]
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
⊢ autoParam
    (∀ (X Y : Paths V) (f : X ⟶ Y),
      F.map f = eqToHom (_ : F.obj X = G.obj X) ≫ G.map f ≫ eqToHom (_ : G.obj Y = F.obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y : Paths V
f : X ⟶ Y
⊢ F.map f = eqToHom (_ : F.obj X = G.obj X) ≫ G.map f ≫ eqToHom (_ : G.obj Y = F.obj Y)
[PROOFSTEP]
induction' f with Y' Z' g e ih
[GOAL]
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y : Paths V
⊢ F.map Quiver.Path.nil = eqToHom (_ : F.obj X = G.obj X) ≫ G.map Quiver.Path.nil ≫ eqToHom (_ : G.obj X = F.obj X)
[PROOFSTEP]
erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom (_ : F.obj X = G.obj X) ≫ G.map g ≫ eqToHom (_ : G.obj Y' = F.obj Y')
⊢ F.map (Quiver.Path.cons g e) =
    eqToHom (_ : F.obj X = G.obj X) ≫ G.map (Quiver.Path.cons g e) ≫ eqToHom (_ : G.obj Z' = F.obj Z')
[PROOFSTEP]
erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
[GOAL]
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h :
  ∀ (a b : V) (e : a ⟶ b),
    F.map (Quiver.Hom.toPath e) =
      eqToHom (_ : F.obj a = G.obj a) ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj b = F.obj b)
X Y Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom (_ : F.obj X = G.obj X) ≫ G.map g ≫ eqToHom (_ : G.obj Y' = F.obj Y')
⊢ (eqToHom (_ : F.obj X = G.obj X) ≫ G.map g ≫ eqToHom (_ : G.obj Y' = F.obj Y')) ≫
      eqToHom (_ : F.obj Y' = G.obj Y') ≫ G.map (Quiver.Hom.toPath e) ≫ eqToHom (_ : G.obj Z' = F.obj Z') =
    eqToHom (_ : F.obj X = G.obj X) ≫ (G.map g ≫ G.map (Quiver.Hom.toPath e)) ≫ eqToHom (_ : G.obj Z' = F.obj Z')
[PROOFSTEP]
simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
g : Path Y Z
⊢ composePath (Path.comp f g) = composePath f ≫ composePath g
[PROOFSTEP]
induction' g with Y' Z' g e ih
[GOAL]
case nil
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
⊢ composePath (Path.comp f Path.nil) = composePath f ≫ composePath Path.nil
[PROOFSTEP]
simp
[GOAL]
case cons
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
Y' Z' : C
g : Path Y Y'
e : Y' ⟶ Z'
ih : composePath (Path.comp f g) = composePath f ≫ composePath g
⊢ composePath (Path.comp f (Path.cons g e)) = composePath f ≫ composePath (Path.cons g e)
[PROOFSTEP]
simp [ih]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ pathsHomRel C (Hom.toPath (𝟙 X))
    (𝟙
      ({ obj := fun X => { as := X },
              map := fun {X Y} f => Quot.mk (Quotient.CompClosure (pathsHomRel C)) (Hom.toPath f) }.obj
          X).as)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ pathsHomRel C (Hom.toPath (f ≫ g)) (Hom.toPath f ≫ Hom.toPath g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ (𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (𝟭 (Quotient (pathsHomRel C))).obj { as := as✝ } ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj { as := as✝ }
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Quotient (pathsHomRel C)
f : X✝.as ⟶ Y✝.as
⊢ (𝟭 (Quotient (pathsHomRel C))).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f) ≫
      ((fun X =>
            Quotient.casesOn (motive := fun t =>
              X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
              (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
              (_ : X = X))
          Y✝).hom =
    ((fun X =>
            Quotient.casesOn (motive := fun t =>
              X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
              (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
              (_ : X = X))
          X✝).hom ≫
      (quotientPathsTo C ⋙ toQuotientPaths C).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Quotient (pathsHomRel C)
f : X✝.as ⟶ Y✝.as
⊢ Quotient.CompClosure (pathsHomRel C) (f ≫ 𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := Y✝.as }).as)
    (𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := X✝.as }).as ≫
      Hom.toPath ((quotientPathsTo C).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f)))
[PROOFSTEP]
apply Quotient.CompClosure.of
[GOAL]
case a.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Quotient (pathsHomRel C)
f : X✝.as ⟶ Y✝.as
⊢ pathsHomRel C (f ≫ 𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := Y✝.as }).as)
    (𝟙 ((𝟭 (Quotient (pathsHomRel C))).obj { as := X✝.as }).as ≫
      Hom.toPath ((quotientPathsTo C).map (Quot.mk (Quotient.CompClosure (pathsHomRel C)) f)))
[PROOFSTEP]
simp [Category.comp_id, Category.id_comp, pathsHomRel]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (toQuotientPaths C ⋙ quotientPathsTo C).map f ≫
      ((fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)) Y✝).hom =
    ((fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)) X✝).hom ≫ (𝟭 C).map f
[PROOFSTEP]
simp [Quot.liftOn_mk]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ (quotientPathsTo C).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              Quotient.casesOn (motive := fun t =>
                X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
                (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
                (_ : X = X)).hom
          X) ≫
      NatTrans.app (NatIso.ofComponents fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)).hom
        ((quotientPathsTo C).obj X) =
    𝟙 ((quotientPathsTo C).obj X)
[PROOFSTEP]
cases X
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (quotientPathsTo C).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              Quotient.casesOn (motive := fun t =>
                X = t → ((𝟭 (Quotient (pathsHomRel C))).obj X ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj X)) X
                (fun as h => (_ : { as := as } = X) ▸ Iso.refl ((𝟭 (Quotient (pathsHomRel C))).obj { as := as }))
                (_ : X = X)).hom
          { as := as✝ }) ≫
      NatTrans.app (NatIso.ofComponents fun X => Iso.refl ((toQuotientPaths C ⋙ quotientPathsTo C).obj X)).hom
        ((quotientPathsTo C).obj { as := as✝ }) =
    𝟙 ((quotientPathsTo C).obj { as := as✝ })
[PROOFSTEP]
simp only [pathsHomRel, pathComposition_obj, pathComposition_map, Functor.id_obj, quotientPathsTo_obj, Functor.comp_obj,
  toQuotientPaths_obj_as, NatIso.ofComponents_hom_app, Iso.refl_hom, quotientPathsTo_map, Category.comp_id]
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ Quot.liftOn (𝟙 { as := as✝ }) (fun f => composePath f)
      (_ :
        ∀ (a b : { as := as✝ }.as ⟶ ((toQuotientPaths C).obj as✝).as),
          Quotient.CompClosure (fun x x_1 p q => composePath p = composePath q) a b →
            (fun f => composePath f) a = (fun f => composePath f) b) =
    𝟙 as✝
[PROOFSTEP]
rfl