-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : D ⥤ Functor.{v_1, v_2, u_1, u_2} C D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst_5 : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
inst_7 : (((mapBifunctor F J I).obj X').obj (Functor.obj (single₀ I) Y)).HasMap p
rw :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
        (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')) ≫
      Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₁ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
      (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
    ((Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ) ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₂ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
      (Iso.hom (mapBifunctorRightUnitor F Y e p hp X') ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₃ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)) ≫
      𝟙 (mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y)))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₄ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ ≫ Iso.inv (mapBifunctorRightUnitor F Y e p hp X'))
rw₅ :
  Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
    (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫
      CategoryStruct.comp (Y := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y))
        (Iso.inv (mapBifunctorRightUnitor F Y e p hp X)) (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))))
⊢ Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ X')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
      (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (Iso.hom (mapBifunctorRightUnitor F Y e p hp X')))
    (Iso.hom (mapBifunctorRightUnitor F Y e p hp X) ≫ φ)
have rw₆ : Eq (α := mapBifunctorMapObj F p X (Functor.obj (single₀ I) Y) ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y))
  (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y))) (mapBifunctorMapMap F p φ (𝟙 (Functor.obj (single₀ I) Y)))
Tactic: rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]