-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
Goal:
C : Type u
inst : Category.{v, u} C
x : Functor.{u_2, v, u_1, u} (↑chosenTerminal : Type u_1) C
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 := ⋯ } } } =
    x.map
      {
        down :=
          {
            down :=
              { down := ⋯ :
                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 }) }
⊢ 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 ⋯)

Tactic:
simp only [eqToHom_refl, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp