-- 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 : J
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)
have obtain : 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)
      (𝟙 { as := x : Discrete J }) ≫
    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 (𝟙 { as := x : Discrete J }))
Tactic: obtain rfl : f = 𝟙 _ := rfl
Cleared hypotheses: f