-- 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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
rw₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β
rw₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ 𝟙 (F.obj j')
rw₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α
rw₆ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      (h.isoMap δ ⋯).hom =
    F.map α ≫ (h.isoMap δ ⋯).hom
rw₇ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      F.map δ =
    F.map α ≫ F.map δ
rw₈ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      ((Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫ F.map δ) =
    F.map α ≫ F.map δ
rw₉ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β ≫ F.map δ) =
    F.map α ≫ F.map δ
rw₁₀ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β ≫ F.map δ) =
    F.map (α ≫ δ)
rw₁₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β ≫ F.map δ) =
    F.map (rightToMax i₀ j ≫ γ)
rw₁₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β ≫ F.map δ) =
    F.map (rightToMax i₀ j) ≫ F.map γ
rw₁₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map (β ≫ δ)) =
    F.map (rightToMax i₀ j) ≫ F.map γ
rw₁₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map (leftToMax i₀ j ≫ γ)) =
    F.map (rightToMax i₀ j) ≫ F.map γ
rw₁₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map (leftToMax i₀ j) ≫ F.map γ) =
    F.map (rightToMax i₀ j) ≫ F.map γ
rw₁₆ rw₁₇ : F.map (rightToMax i₀ j) ≫ F.map γ = F.map (rightToMax i₀ j) ≫ F.map γ
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id_assoc, CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, Nonempty.intro, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap