-- 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 : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
X : C
e : F.obj X ≅ 𝟭 D
inst_5 : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst_6 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y).HasMap p
inst_7 : (((mapBifunctor F I J).obj (Functor.obj (single₀ I) X)).obj Y').HasMap p
rw :
  Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
        (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ) (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y')) ≫
      Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
    ((Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫ φ) ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
rw₁ :
  Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
      (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ)
      (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y') ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y')))
    ((Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫ φ) ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
rw₂ :
  Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
      (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ)
      (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y') ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y')))
    (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫ φ ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
rw₃ :
  Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ ≫
      𝟙 (mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y'))
    (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫ φ ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
rw₄ :
  Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ)
    (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫ φ ≫ Iso.inv (mapBifunctorLeftUnitor F X e p hp Y'))
rw₅ :
  Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
    (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ)
    (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫
      CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y)
        (Iso.inv (mapBifunctorLeftUnitor F X e p hp Y)) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ))
⊢ Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ Y')
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
      (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ) (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y')))
    (Iso.hom (mapBifunctorLeftUnitor F X e p hp Y) ≫ φ)
have rw₆ : Eq (α := mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y ⟶ mapBifunctorMapObj F p (Functor.obj (single₀ I) X) Y')
  (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ) (mapBifunctorMapMap F p (𝟙 (Functor.obj (single₀ I) X)) φ)
Tactic: rw [← cancel_mono (mapBifunctorLeftUnitor F X e p hp Y').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorLeftUnitor_inv_naturality, Iso.hom_inv_id_assoc]