-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
J : Type u₂
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C
x y : J
f : { as := x : Discrete J } ⟶ { as := y }
obtain :
  ∀ (f : { as := x : Discrete J } ⟶ { as := x }),
    Eq (α :=
      Functor.obj.{u₂, v₁, u₂, u₁}
          (Functor.obj
            (Functor.comp (D := J → C)
              { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦ f.app { as := j },
                map_id := ⋯, map_comp := ⋯ }
              { obj := fun (F : J → C) ↦ Discrete.functor F,
                map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as, map_id := ⋯,
                map_comp := ⋯ })
            F)
          { as := x : Discrete J } ⟶
        (Functor.obj (𝟭 (Functor.{u₂, v₁, u₂, u₁} (Discrete J) C)) F).obj { as := x : Discrete J })
      (Functor.map
          (Functor.obj
            (Functor.comp (D := J → C)
              { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j : Discrete J },
                map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                  f.app { as := j : Discrete J },
                map_id := ⋯, map_comp := ⋯ : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C ⥤ (J → C) }
              { obj := fun (F : J → C) ↦ Discrete.functor F,
                map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as, map_id := ⋯,
                map_comp := ⋯ : (J → C) ⥤ Functor.{u₂, v₁, u₂, u₁} (Discrete J) C })
            F)
          f ≫
        Iso.hom
          ((fun (x : Discrete J) ↦
              (Iso.refl
                  (Functor.obj.{u₂, v₁, u₂, u₁}
                    (Functor.obj
                      (Functor.comp (D := J → C)
                        { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                          map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                            f.app { as := j },
                          map_id := ⋯, map_comp := ⋯ }
                        { obj := fun (F : J → C) ↦ Discrete.functor F,
                          map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                          map_id := ⋯, map_comp := ⋯ })
                      F)
                    x) :
                Iso.{v₁, u₁} (C := C)
                  (Functor.obj.{u₂, v₁, u₂, u₁}
                    (Functor.obj
                      (Functor.comp (D := J → C)
                        { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                          map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                            f.app { as := j },
                          map_id := ⋯, map_comp := ⋯ }
                        { obj := fun (F : J → C) ↦ Discrete.functor F,
                          map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                          map_id := ⋯, map_comp := ⋯ })
                      F)
                    x)
                  (Functor.obj.{u₂, v₁, u₂, u₁}
                    (Functor.obj
                      (Functor.comp (D := J → C)
                        { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                          map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                            f.app { as := j },
                          map_id := ⋯, map_comp := ⋯ }
                        { obj := fun (F : J → C) ↦ Discrete.functor F,
                          map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                          map_id := ⋯, map_comp := ⋯ })
                      F)
                    x)))
            { as := x }))
      (Iso.hom
          ((fun (x : Discrete J) ↦
              (Iso.refl
                  (Functor.obj.{u₂, v₁, u₂, u₁}
                    (Functor.obj
                      (Functor.comp (D := J → C)
                        { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                          map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                            f.app { as := j },
                          map_id := ⋯, map_comp := ⋯ }
                        { obj := fun (F : J → C) ↦ Discrete.functor F,
                          map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                          map_id := ⋯, map_comp := ⋯ })
                      F)
                    x) :
                Iso.{v₁, u₁} (C := C)
                  (Functor.obj.{u₂, v₁, u₂, u₁}
                    (Functor.obj
                      (Functor.comp (D := J → C)
                        { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                          map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                            f.app { as := j },
                          map_id := ⋯, map_comp := ⋯ }
                        { obj := fun (F : J → C) ↦ Discrete.functor F,
                          map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                          map_id := ⋯, map_comp := ⋯ })
                      F)
                    x)
                  (Functor.obj.{u₂, v₁, u₂, u₁}
                    (Functor.obj
                      (Functor.comp (D := J → C)
                        { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                          map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                            f.app { as := j },
                          map_id := ⋯, map_comp := ⋯ }
                        { obj := fun (F : J → C) ↦ Discrete.functor F,
                          map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                          map_id := ⋯, map_comp := ⋯ })
                      F)
                    x)))
            { as := x }) ≫
        (Functor.obj (𝟭 (Functor.{u₂, v₁, u₂, u₁} (Discrete J) C)) F).map f)
⊢ Eq (α :=
    Functor.obj.{u₂, v₁, u₂, u₁}
        (Functor.obj
          (Functor.comp (D := J → C)
            { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
              map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦ f.app { as := j },
              map_id := ⋯, map_comp := ⋯ }
            { obj := fun (F : J → C) ↦ Discrete.functor F,
              map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as, map_id := ⋯,
              map_comp := ⋯ })
          F)
        { as := x : Discrete J } ⟶
      (Functor.obj (𝟭 (Functor.{u₂, v₁, u₂, u₁} (Discrete J) C)) F).obj { as := y : Discrete J })
    (Functor.map
        (Functor.obj
          (Functor.comp (D := J → C)
            { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j : Discrete J },
              map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                f.app { as := j : Discrete J },
              map_id := ⋯, map_comp := ⋯ : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C ⥤ (J → C) }
            { obj := fun (F : J → C) ↦ Discrete.functor F,
              map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as, map_id := ⋯,
              map_comp := ⋯ : (J → C) ⥤ Functor.{u₂, v₁, u₂, u₁} (Discrete J) C })
          F)
        f ≫
      Iso.hom
        ((fun (x : Discrete J) ↦
            (Iso.refl
                (Functor.obj.{u₂, v₁, u₂, u₁}
                  (Functor.obj
                    (Functor.comp (D := J → C)
                      { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                        map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                          f.app { as := j },
                        map_id := ⋯, map_comp := ⋯ }
                      { obj := fun (F : J → C) ↦ Discrete.functor F,
                        map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ })
                    F)
                  x) :
              Iso.{v₁, u₁} (C := C)
                (Functor.obj.{u₂, v₁, u₂, u₁}
                  (Functor.obj
                    (Functor.comp (D := J → C)
                      { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                        map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                          f.app { as := j },
                        map_id := ⋯, map_comp := ⋯ }
                      { obj := fun (F : J → C) ↦ Discrete.functor F,
                        map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ })
                    F)
                  x)
                (Functor.obj.{u₂, v₁, u₂, u₁}
                  (Functor.obj
                    (Functor.comp (D := J → C)
                      { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                        map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                          f.app { as := j },
                        map_id := ⋯, map_comp := ⋯ }
                      { obj := fun (F : J → C) ↦ Discrete.functor F,
                        map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ })
                    F)
                  x)))
          { as := y }))
    (Iso.hom
        ((fun (x : Discrete J) ↦
            (Iso.refl
                (Functor.obj.{u₂, v₁, u₂, u₁}
                  (Functor.obj
                    (Functor.comp (D := J → C)
                      { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                        map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                          f.app { as := j },
                        map_id := ⋯, map_comp := ⋯ }
                      { obj := fun (F : J → C) ↦ Discrete.functor F,
                        map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ })
                    F)
                  x) :
              Iso.{v₁, u₁} (C := C)
                (Functor.obj.{u₂, v₁, u₂, u₁}
                  (Functor.obj
                    (Functor.comp (D := J → C)
                      { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                        map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                          f.app { as := j },
                        map_id := ⋯, map_comp := ⋯ }
                      { obj := fun (F : J → C) ↦ Discrete.functor F,
                        map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ })
                    F)
                  x)
                (Functor.obj.{u₂, v₁, u₂, u₁}
                  (Functor.obj
                    (Functor.comp (D := J → C)
                      { obj := fun (F : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C) (j : J) ↦ F.obj { as := j },
                        map := fun {X Y : Functor.{u₂, v₁, u₂, u₁} (Discrete J) C} (f : X ⟶ Y) (j : J) ↦
                          f.app { as := j },
                        map_id := ⋯, map_comp := ⋯ }
                      { obj := fun (F : J → C) ↦ Discrete.functor F,
                        map := fun {X Y : J → C} (f : X ⟶ Y) ↦ Discrete.natTrans fun (j : Discrete J) ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ })
                    F)
                  x)))
          { as := x }) ≫
      (Functor.obj (𝟭 (Functor.{u₂, v₁, u₂, u₁} (Discrete J) C)) F).map f)

Tactic:
obtain rfl : x = y := Discrete.eq_of_hom f

Premises used: CategoryTheory.Discrete.eq_of_hom, rfl