-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Cat (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{u_2, v, u_1, u}
        (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
          ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
        { down := { as := PUnit.unit : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) })
      (Functor.obj.{u_2, v, u_1, u}
        (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
          ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
        { down := { as := PUnit.unit : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) }))
    (Functor.map
      (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
        ((fun (F : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C) ↦ F.obj { down := { as := () } }) x))
      { down := { down := { down := ⋯ } } })
    (eqToHom ⋯ ≫
      x.map
          {
            down :=
              {
                down :=
                  { down := ⋯ :
                    PLift
                      ((ULiftHom.objDown.{0, u_2}
                            (ULift.down.{u_1, 0}
                              { down := { as := PUnit.unit : Discrete Unit } :
                                ULift.{u_1, 0} (ULiftHom (Discrete Unit)) })).as =
                        (ULiftHom.objDown.{0, u_2}
                            (ULift.down.{u_1, 0}
                              { down := { as := PUnit.unit : Discrete Unit } :
                                ULift.{u_1, 0} (ULiftHom (Discrete Unit)) })).as) } :
                ULift.{0, 0}
                  (PLift
                    ((ULiftHom.objDown.{0, u_2}
                          (ULift.down.{u_1, 0}
                            { down := { as := PUnit.unit : Discrete Unit } :
                              ULift.{u_1, 0} (ULiftHom (Discrete Unit)) })).as =
                      (ULiftHom.objDown.{0, u_2}
                          (ULift.down.{u_1, 0}
                            { down := { as := PUnit.unit : Discrete Unit } :
                              ULift.{u_1, 0} (ULiftHom (Discrete Unit)) })).as)) } :
            ULift.{u_2, 0}
              (ULiftHom.objDown.{0, u_2}
                  (ULift.down.{u_1, 0}
                    { down := { as := PUnit.unit : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) }) ⟶
                ULiftHom.objDown.{0, u_2}
                  (ULift.down.{u_1, 0}
                    { down := { as := PUnit.unit : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) })) } ≫
        eqToHom ⋯)
have h_map : Functor.map
    (Functor.obj (Functor.const (↑chosenTerminal : Type u_1))
      (x.obj { down := { as := () : Discrete Unit } : ULift.{u_1, 0} (ULiftHom (Discrete Unit)) }))
    { down := { down := { down := sorry } } } =
  x.map
    {
      down :=
        {
          down :=
            { down := sorry :
              PLift
                ((ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as =
                  (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as) } :
          ULift.{0, 0}
            (PLift
              ((ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as =
                (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }).as)) } :
      ULift.{u_2, 0}
        (ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit } ⟶
          ULiftHom.objDown.{0, u_2} { as := PUnit.unit : Discrete Unit }) }
Tactic: simp only [eqToHom_refl, Category.comp_id, Category.id_comp]