[GOAL]
C D : Cat
F : C ⟶ D
⊢ 𝟙 C ≫ F = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C D : Cat
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ 𝟙 C ≫ Functor.mk toPrefunctor✝ = Functor.mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
C D : Cat
F : C ⟶ D
⊢ F ≫ 𝟙 D = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C D : Cat
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ Functor.mk toPrefunctor✝ ≫ 𝟙 D = Functor.mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
rfl
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ (fun X => Cat.of (Discrete X)) X ⟶ (fun X => Cat.of (Discrete X)) Y
[PROOFSTEP]
dsimp
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ Cat.of (Discrete X) ⟶ Cat.of (Discrete Y)
[PROOFSTEP]
exact Discrete.functor (Discrete.mk ∘ f)
[GOAL]
X : Type u
⊢ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (𝟙 X) =
    𝟙 ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
X : Type u
⊢ autoParam
    (∀
      (X_1 Y :
        ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X))
      (f : X_1 ⟶ Y),
      ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
              (𝟙 X)).map
          f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟙
                  ({ obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                    X)).map
              f ≫
            eqToHom
              (_ :
                (𝟙
                        ({ obj := fun X => Cat.of (Discrete X),
                              map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                          X)).obj
                    Y =
                  ({ obj := fun X => Cat.of (Discrete X),
                            map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                        (𝟙 X)).obj
                    Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
f : X ⟶ Y
⊢ ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
          (𝟙 X✝)).map
      f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (𝟙
              ({ obj := fun X => Cat.of (Discrete X),
                    map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                X✝)).map
          f ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun X => Cat.of (Discrete X),
                          map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                      X✝)).obj
                Y =
              ({ obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    (𝟙 X✝)).obj
                Y)
[PROOFSTEP]
cases f
[GOAL]
case h_map.up
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
down✝ : PLift (X.as = Y.as)
⊢ ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
          (𝟙 X✝)).map
      { down := down✝ } =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (𝟙
              ({ obj := fun X => Cat.of (Discrete X),
                    map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                X✝)).map
          { down := down✝ } ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun X => Cat.of (Discrete X),
                          map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                      X✝)).obj
                Y =
              ({ obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    (𝟙 X✝)).obj
                Y)
[PROOFSTEP]
simp only [id_eq, eqToHom_refl, Cat.id_map, Category.comp_id, Category.id_comp]
[GOAL]
case h_map.up
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
down✝ : PLift (X.as = Y.as)
⊢ (Discrete.functor (Discrete.mk ∘ 𝟙 X✝)).map { down := down✝ } = { down := down✝ }
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h_map.up.h
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
down✝ : PLift (X.as = Y.as)
⊢ ((Discrete.functor (Discrete.mk ∘ 𝟙 X✝)).map { down := down✝ }).down = { down := down✝ }.down
[PROOFSTEP]
aesop_cat
[GOAL]
case h_obj
X : Type u
⊢ ∀
    (X_1 :
      ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)),
    ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
            (𝟙 X)).obj
        X_1 =
      (𝟙
            ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
              X)).obj
        X_1
[PROOFSTEP]
aesop_cat
[GOAL]
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (f ≫ g) =
    { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫
      { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map g
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    (∀
      (X Y :
        ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
            X✝))
      (f_1 : X ⟶ Y),
      ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
              (f ≫ g)).map
          f_1 =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    f ≫
                  { obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    g).map
              f_1 ≫
            eqToHom
              (_ :
                ({ obj := fun X => Cat.of (Discrete X),
                              map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                          f ≫
                        { obj := fun X => Cat.of (Discrete X),
                              map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                          g).obj
                    Y =
                  ({ obj := fun X => Cat.of (Discrete X),
                            map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                        (f ≫ g)).obj
                    Y))
    _auto✝
case h_obj
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀
    (X :
      ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)),
    ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
            (f ≫ g)).obj
        X =
      ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫
            { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
              g).obj
        X
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : Type u} (f : typeToCat.obj X ⟶ typeToCat.obj Y),
    typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) f) = f
[PROOFSTEP]
intro X Y F
[GOAL]
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F) = F
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ autoParam
    (∀ (X_1 Y_1 : ↑(typeToCat.obj X)) (f : X_1 ⟶ Y_1),
      (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          F.map f ≫
            eqToHom (_ : F.obj Y_1 = (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj Y_1))
    _auto✝
[PROOFSTEP]
intro x y f
[GOAL]
case h_map
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : ↑(typeToCat.obj X)
f : x ⟶ y
⊢ (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).map f =
    eqToHom (_ : ?F.obj x = ?G.obj x) ≫
      F.map f ≫ eqToHom (_ : F.obj y = (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj y)
[PROOFSTEP]
dsimp
[GOAL]
case h_map
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : ↑(typeToCat.obj X)
f : x ⟶ y
⊢ (Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).map f =
    𝟙 ((Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).obj x) ≫ F.map f ≫ 𝟙 (F.obj y)
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h_map.h
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : ↑(typeToCat.obj X)
f : x ⟶ y
⊢ ((Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).map f).down =
    (𝟙 ((Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).obj x) ≫ F.map f ≫ 𝟙 (F.obj y)).down
[PROOFSTEP]
aesop_cat
[GOAL]
case h_obj
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ ∀ (X_1 : ↑(typeToCat.obj X)),
    (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj X_1 = F.obj X_1
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case h_obj.mk
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x : X
⊢ (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj { as := x } = F.obj { as := x }
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case h_obj.mk.as
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x : X
⊢ ((typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj { as := x }).as = (F.obj { as := x }).as
[PROOFSTEP]
rfl
