[GOAL]
C : Cat
⊢ { obj := fun C => Quotient (isIsomorphicSetoid ↑C),
          map := fun {C D} F => Quot.map F.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (F.obj X) (F.obj Y)) }.map
      (𝟙 C) =
    𝟙
      ({ obj := fun C => Quotient (isIsomorphicSetoid ↑C),
            map := fun {C D} F => Quot.map F.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (F.obj X) (F.obj Y)) }.obj
        C)
[PROOFSTEP]
dsimp
[GOAL]
C : Cat
⊢ Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y)) =
    𝟙 (Quotient (isIsomorphicSetoid ↑C))
[PROOFSTEP]
apply funext
[GOAL]
case h
C : Cat
⊢ ∀ (x : Quot Setoid.r),
    Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y)) x =
      𝟙 (Quotient (isIsomorphicSetoid ↑C)) x
[PROOFSTEP]
intro x
[GOAL]
case h
C : Cat
x : Quot Setoid.r
⊢ Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y)) x =
    𝟙 (Quotient (isIsomorphicSetoid ↑C)) x
[PROOFSTEP]
apply x.recOn
[GOAL]
case h.h
C : Cat
x : Quot Setoid.r
⊢ ∀ (a b : ↑C) (p : Setoid.r a b),
    (_ :
        Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y))
            (Quot.mk Setoid.r b) =
          𝟙 (Quotient (isIsomorphicSetoid ↑C)) (Quot.mk Setoid.r b)) =
      (_ : ?m.1036 (Quot.mk Setoid.r b))
[PROOFSTEP]
intro _ _ p
[GOAL]
case h.h
C : Cat
x : Quot Setoid.r
a✝ b✝ : ↑C
p : Setoid.r a✝ b✝
⊢ (_ :
      Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y)) (Quot.mk Setoid.r b✝) =
        𝟙 (Quotient (isIsomorphicSetoid ↑C)) (Quot.mk Setoid.r b✝)) =
    (_ : ?m.1036 (Quot.mk Setoid.r b✝))
[PROOFSTEP]
simp only [types_id_apply]
[GOAL]
case h.f
C : Cat
x : Quot Setoid.r
⊢ ∀ (a : ↑C),
    Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y)) (Quot.mk Setoid.r a) =
      𝟙 (Quotient (isIsomorphicSetoid ↑C)) (Quot.mk Setoid.r a)
[PROOFSTEP]
intro _
[GOAL]
case h.f
C : Cat
x : Quot Setoid.r
a✝ : ↑C
⊢ Quot.map (𝟙 C).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r ((𝟙 C).obj X) ((𝟙 C).obj Y)) (Quot.mk Setoid.r a✝) =
    𝟙 (Quotient (isIsomorphicSetoid ↑C)) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ { obj := fun C => Quotient (isIsomorphicSetoid ↑C),
          map := fun {C D} F => Quot.map F.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (F.obj X) (F.obj Y)) }.map
      (f ≫ g) =
    { obj := fun C => Quotient (isIsomorphicSetoid ↑C),
            map := fun {C D} F => Quot.map F.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (F.obj X) (F.obj Y)) }.map
        f ≫
      { obj := fun C => Quotient (isIsomorphicSetoid ↑C),
            map := fun {C D} F => Quot.map F.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (F.obj X) (F.obj Y)) }.map
        g
[PROOFSTEP]
dsimp
[GOAL]
C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y))) =
    Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
      Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y))
[PROOFSTEP]
apply funext
[GOAL]
case h
C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ ∀ (x : Quot Setoid.r),
    Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y))) x =
      (Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
          Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y)))
        x
[PROOFSTEP]
intro x
[GOAL]
case h
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quot Setoid.r
⊢ Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y))) x =
    (Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
        Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y)))
      x
[PROOFSTEP]
apply x.recOn
[GOAL]
case h.h
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quot Setoid.r
⊢ ∀ (a b : ↑C) (p : Setoid.r a b),
    (_ :
        Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y)))
            (Quot.mk Setoid.r b) =
          (Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
              Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y)))
            (Quot.mk Setoid.r b)) =
      (_ : ?m.1407 (Quot.mk Setoid.r b))
[PROOFSTEP]
intro _ _ _
[GOAL]
case h.h
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quot Setoid.r
a✝ b✝ : ↑C
p✝ : Setoid.r a✝ b✝
⊢ (_ :
      Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y)))
          (Quot.mk Setoid.r b✝) =
        (Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
            Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y)))
          (Quot.mk Setoid.r b✝)) =
    (_ : ?m.1407 (Quot.mk Setoid.r b✝))
[PROOFSTEP]
simp only [types_id_apply]
[GOAL]
case h.f
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quot Setoid.r
⊢ ∀ (a : ↑C),
    Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y)))
        (Quot.mk Setoid.r a) =
      (Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
          Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y)))
        (Quot.mk Setoid.r a)
[PROOFSTEP]
intro _
[GOAL]
case h.f
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quot Setoid.r
a✝ : ↑C
⊢ Quot.map (f ≫ g).obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (g.obj (f.obj X)) (g.obj (f.obj Y)))
      (Quot.mk Setoid.r a✝) =
    (Quot.map f.obj (_ : ∀ (X Y : ↑C), Setoid.r X Y → Setoid.r (f.obj X) (f.obj Y)) ≫
        Quot.map g.obj (_ : ∀ (X Y : ↑D), Setoid.r X Y → Setoid.r (g.obj X) (g.obj Y)))
      (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
