-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
rw₄ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map δ ≫ F.map β
rw₅ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (δ ≫ β)
rw₆ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (γ ≫ minToRight i₀ j)
rw₇ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
rw₈ :
  F.map (δ ≫ α) ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
rw₉ :
  F.map (γ ≫ minToLeft i₀ j) ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
rw₁₀ :
  F.map γ ≫
      F.map (minToLeft i₀ j) ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
rw₁₁ rw₁₂ : F.map γ ≫ F.map (minToRight i₀ j) = F.map γ ≫ F.map (minToRight i₀ j)
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom, CategoryTheory.CategoryStruct.id, Nonempty.intro, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap