awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
⊢ Eq (α :=
    Functor.obj.{0, v', 0, u'} (pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      c.pt)
    (CategoryStruct.comp (Y :=
      Functor.obj.{0, v', 0, u'}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
            (BinaryCofan.mk (P :=
              G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero))) (G.map coprod.inl)
              (G.map coprod.inr))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (P := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
            (G.map coprod.inl) (G.map coprod.inr)))
        { as := WalkingPair.right })
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one))
    (CategoryStruct.comp (Y :=
      Functor.obj.{0, v', 0, u'}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
            (BinaryCofan.mk (P :=
              G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero))) (G.map coprod.inl)
              (G.map coprod.inr))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (NatTrans.app
        (Cocone.ι
          (BinaryCofan.mk (P := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
            (G.map coprod.inl) (G.map coprod.inr)))
        { as := WalkingPair.right })
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one))
have refine_3 : G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one =
  G.map (K.map WalkingParallelPairHom.right) ≫ c.ι.app WalkingParallelPair.one
Tactic: simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, ←
              G.map_comp_assoc, coprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
j : WalkingParallelPair
⊢ (G.mapCocone (coequalizerCocone K)).ι.app j ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app j
have zero : (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.inv
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) sorry) =
  c.ι.app WalkingParallelPair.zero
Tactic: rcases j with (_ | _)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
j : WalkingParallelPair
zero :
  (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app WalkingParallelPair.zero
⊢ (G.mapCocone (coequalizerCocone K)).ι.app j ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app j
have one : (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.inv
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) sorry) =
  c.ι.app WalkingParallelPair.one
Tactic: rcases j with (_ | _)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app WalkingParallelPair.zero
have zero : G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero
Tactic: simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp,
              eqToHom_refl, Category.assoc, Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc,
              PreservesPushout.inl_iso_inv_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
⊢ m =
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.inv
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)
have rw : Eq (α :=
  pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ⟶
    s.pt)
  (Iso.hom
      (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
    m)
  (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) sorry)
Tactic: rw [Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
⊢ Eq (α :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ⟶
      s.pt)
    (Iso.hom
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
      m)
    (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)
have this : (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫ m = s.ι.app WalkingParallelPair.one
Tactic: have := h WalkingParallelPair.one
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = s.ι.app WalkingParallelPair.one
⊢ Eq (α :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ⟶
      s.pt)
    (Iso.hom
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
      m)
    (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)
have h₀ : CategoryStruct.comp (Y :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (pushout.inl (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (Iso.hom
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
      m) =
  CategoryStruct.comp (Y :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (pushout.inl (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
    (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) sorry)
Tactic: ext
-- 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.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ 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.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ 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.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β
have obtain : ∀ (s : J) (γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j) (δ : s ⟶ j') (h₁ : γ ≫ minToRight i₀ j = δ ≫ β)
  (h₂ : γ ≫ minToLeft i₀ j = δ ≫ α), h.coneπApp j = (h.isoMap α sorry).inv ≫ F.map β
Tactic: obtain ⟨s, γ, δ, h₁, h₂⟩ := IsCofiltered.bowtie
    (IsCofiltered.minToRight i₀ j) β (IsCofiltered.minToLeft 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.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 = δ ≫ α
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β
have dsimp : 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)) =
  (h.isoMap α sorry).inv ≫ F.map β
Tactic: dsimp [coneπ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.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 = δ ≫ α
⊢ 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 β
have rw : (h.isoMap α sorry).hom ≫
    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)) =
  (h.isoMap α sorry).hom ≫ (h.isoMap α sorry).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]
-- 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
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 β
⊢ 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 β
have rw₁ : F.map α ≫
    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)) =
  F.map α ≫ (h.isoMap α sorry).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]
-- 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
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 β
⊢ 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 β
have rw₂ : F.map α ≫
    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)) =
  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]
-- 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
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 β
⊢ 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 β
have rw₃ : (h.isoMap δ sorry).hom ≫
    F.map α ≫
      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)) =
  (h.isoMap δ sorry).hom ≫ 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]