awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
s : Cone F
j : J
rw :
  CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (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)) =
    s.π.app j
rw₁ :
  Eq (α := s.pt ⟶ F.obj j)
    (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
          (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)) :
      s.pt ⟶ F.obj j)
    (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (F.map (minToRight i₀ j)) :
      s.pt ⟶ F.obj j)
⊢ s.π.app i₀ ≫
      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)) =
    s.π.app j
have rw₂ : Eq (α := s.pt ⟶ F.obj j)
  (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
      (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) sorry))
          (F.map (minToRight i₀ j))) :
    s.pt ⟶ F.obj j)
  (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
      (F.map (minToRight i₀ j)) :
    s.pt ⟶ F.obj j)
Tactic: rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
s : Cone F
j : J
rw :
  CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (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)) =
    s.π.app j
rw₁ :
  Eq (α := s.pt ⟶ F.obj j)
    (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
          (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)) :
      s.pt ⟶ F.obj j)
    (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (F.map (minToRight i₀ j)) :
      s.pt ⟶ F.obj j)
rw₂ :
  Eq (α := s.pt ⟶ F.obj j)
    (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (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))) :
      s.pt ⟶ F.obj j)
    (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (F.map (minToRight i₀ j)) :
      s.pt ⟶ F.obj j)
⊢ s.π.app i₀ ≫
      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)) =
    s.π.app j
have rw₃ : Eq (α := s.pt ⟶ F.obj j)
  (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
      (F.map (minToRight i₀ j)) :
    s.pt ⟶ F.obj j)
  (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
      (F.map (minToRight i₀ j)) :
    s.pt ⟶ F.obj j)
Tactic: rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
hc : IsLimit c
⊢ IsIso (c.π.app i₀)
have simp : IsIso (Y := F.obj i₀) (Iso.hom (hc.conePointUniqueUpToIso h.isLimitCone) : c.pt ⟶ F.obj i₀)
Tactic: simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀,
    cone_π_app, coneπApp_eq_id, cone_pt, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
⊢ h.cone ≅ c
have refine : ∀ (j : J), h.cone.π.app j = (asIso (c.π.app i₀)).symm.hom ≫ c.π.app j
Tactic: refine Cone.ext (asIso (c.π.app i₀)).symm (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.cone.π.app j = (asIso (c.π.app i₀)).symm.hom ≫ c.π.app j
have dsimp : h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
have rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
Tactic: rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
have rw₁ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j
Tactic: rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
rw₁ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
have rw₂ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β
Tactic: rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
rw₁ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j
rw₂ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
have rw₃ : (c.π.app i ≫ F.map α) ≫ (h.isoMap α sorry).inv ≫ F.map β = c.π.app i ≫ F.map β
Tactic: rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
rw₁ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j
rw₂ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β
rw₃ : (c.π.app i ≫ F.map α) ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
have rw₄ : c.π.app i ≫ F.map α ≫ (h.isoMap α sorry).inv ≫ F.map β = c.π.app i ≫ F.map β
Tactic: rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
rw₁ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j
rw₂ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β
rw₃ : (c.π.app i ≫ F.map α) ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
rw₄ : c.π.app i ≫ F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
have rw₅ : c.π.app i ≫ F.map β = c.π.app i ≫ F.map β
Tactic: rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (hypothesis)
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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map φ)
have this : IsIso (F.map ι)
Tactic: have := h ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (hypothesis)
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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this : IsIso (F.map ι)
⊢ IsIso (F.map φ)
have this₁ : IsIso (F.map (ι ≫ φ))
Tactic: have := h (ι ≫ φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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'
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv
have obtain : ∀ (s : J) (γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s) (δ : j' ⟶ s) (h₁ : leftToMax i₀ j ≫ γ = β ≫ δ)
  (h₂ : rightToMax i₀ j ≫ γ = α ≫ δ), h.coconeιApp j = F.map α ≫ (h.isoMap β sorry).inv
Tactic: obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie
    (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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 ≫ γ = α ≫ δ
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv
have dsimp : 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) sorry)) =
  F.map α ≫ (h.isoMap β sorry).inv
Tactic: dsimp [coconeιApp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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 ≫ γ = α ≫ δ
⊢ 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
have 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) sorry)) ≫
    (h.isoMap β sorry).hom =
  (F.map α ≫ (h.isoMap β sorry).inv) ≫ (h.isoMap β sorry).hom
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ 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
have 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) sorry) ≫ (h.isoMap β sorry).hom) =
  (F.map α ≫ (h.isoMap β sorry).inv) ≫ (h.isoMap β sorry).hom
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ 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
have 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) sorry) ≫ (h.isoMap β sorry).hom) =
  F.map α ≫ (h.isoMap β sorry).inv ≫ (h.isoMap β sorry).hom
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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
⊢ 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
have 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) sorry) ≫ F.map β) =
  F.map α ≫ (h.isoMap β sorry).inv ≫ F.map β
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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 β
⊢ 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
have 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) sorry) ≫ F.map β) =
  F.map α ≫ 𝟙 (F.obj j')
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
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')
⊢ 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
have 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) sorry) ≫ F.map β) =
  F.map α
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]