-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.Basic (goal)
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 }
⊢ 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)
have 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 := sorry, map_comp := sorry }
            { 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 := sorry,
              map_comp := sorry })
          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 := sorry, map_comp := sorry : 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 := sorry,
              map_comp := sorry : (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 := sorry, map_comp := sorry }
                      { 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 := sorry, map_comp := sorry })
                    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 := sorry, map_comp := sorry }
                      { 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 := sorry, map_comp := sorry })
                    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 := sorry, map_comp := sorry }
                      { 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 := sorry, map_comp := sorry })
                    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 := sorry, map_comp := sorry }
                      { 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 := sorry, map_comp := sorry })
                    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 := sorry, map_comp := sorry }
                      { 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 := sorry, map_comp := sorry })
                    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 := sorry, map_comp := sorry }
                      { 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 := sorry, map_comp := sorry })
                    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
Cleared hypotheses: y, f