awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
⊢ 𝟙 (colimit (pullback c.ι (Functor.map (Functor.const J) z))) ≫ f z =
    CategoryStruct.comp (Y := colimit.{w, w, v, u} (Functor.obj (Functor.const J) X))
      (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) z)))
      (Iso.hom
        (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
          (isColimitConstCocone J X)))
have refine_1 : ∀ (j : J),
  colimit.ι (pullback c.ι (Functor.map (Functor.const J) z)) j ≫
      𝟙 (colimit (pullback c.ι (Functor.map (Functor.const J) z))) ≫ f z =
    CategoryStruct.comp (Y := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
      (colimit.ι (pullback c.ι (Functor.map (Functor.const J) z)) j)
      (CategoryStruct.comp (Y := colimit.{w, w, v, u} (Functor.obj (Functor.const J) X))
        (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) z)))
        (Iso.hom
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
            (isColimitConstCocone J X))))
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι (Functor.map (Functor.const J) z)) j ≫
      𝟙 (colimit (pullback c.ι (Functor.map (Functor.const J) z))) ≫ f z =
    CategoryStruct.comp (Y := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
      (colimit.ι (pullback c.ι (Functor.map (Functor.const J) z)) j)
      (CategoryStruct.comp (Y := colimit.{w, w, v, u} (Functor.obj (Functor.const J) X))
        (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) z)))
        (Iso.hom
          (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
            (isColimitConstCocone J X))))
have refine_1 : CategoryStruct.comp (Y := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (colimit.ι (pullback c.ι (Functor.map (Functor.const J) z)) j :
      (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X) =
  NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j
Tactic: rw [Category.id_comp, ι_colimMap_assoc, colimit.comp_coconePointUniqueUpToIso_hom,
      constCocone_ι, NatTrans.id_app, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
⊢ MorphismProperty.isomorphisms C (X := Functor.obj colim Y) (Functor.map colim c.ι)
have refine_2 : Arrow.mk (X := Functor.obj colim Y) (Functor.map colim c.ι) ≅ Arrow.mk (𝟙 c.pt)
Tactic: refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).2
      ((inferInstance : IsIso (𝟙 c.pt)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst_4 : IsFiltered J
⊢ Epi (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
have this : IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
  (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
Tactic: have := isIso_f hc z
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
⊢ ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this : IsFiltered J
⊢ ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀
have this₁ : ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
  [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
Tactic: have := hc.mono_ι_app_of_isFiltered
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
⊢ ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀
have this₁ : Mono c.ι
Tactic: have := NatTrans.mono_of_mono_app c.ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
⊢ ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀
have refine : z =
  (inv ((F z).obj j).obj (P := Over.isMono X).hom ≫
      NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
    c.ι.app j
Tactic: refine ⟨j, inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι _).app j, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
⊢ z =
    (inv ((F z).obj j).obj (P := Over.isMono X).hom ≫
        NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have dsimp : z =
  CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
      (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
      (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
    c.ι.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
⊢ z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
        (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
        (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have rw : z =
  CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
    (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
Tactic: rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
rw :
  z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
      (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
      (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
⊢ z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
        (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
        (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have rw₁ : Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
  (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
Tactic: rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
rw :
  z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
      (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
      (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₁ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
⊢ z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
        (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
        (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have rw₂ : Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
  (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z) ≫ c.ι) j)
Tactic: rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
rw :
  z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
      (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
      (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₁ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₂ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z) ≫ c.ι) j)
⊢ z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
        (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
        (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have rw₃ : Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z) ≫ Functor.map (Functor.const J) z) j)
Tactic: rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
rw :
  z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
      (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
      (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₁ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₂ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z) ≫ c.ι) j)
rw₃ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z) ≫ Functor.map (Functor.const J) z) j)
⊢ z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
        (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
        (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have rw₄ : Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫
    NatTrans.app (Functor.map (Functor.const J) z) j)
Tactic: rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
c : Cocone Y
hc : IsColimit c
inst_4 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_5 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
z : X ⟶ c.pt
this_1 : IsFiltered J
this_2 :
  ∀ (j₀ : J) [inst_6 : HasColimitsOfShape.{w, w, v, u} (Under j₀) C]
    [Functor.PreservesMonomorphisms (C := Functor.{w, v, w, u} (Under j₀) C) colim], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h : IsIso ((F z).obj j).obj (P := Over.isMono X).hom
rw :
  z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
      (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
      (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₁ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j ≫ c.ι.app j)
rw₂ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z) ≫ c.ι) j)
rw₃ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z) ≫ Functor.map (Functor.const J) z) j)
rw₄ :
  Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
    (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫
      NatTrans.app (Functor.map (Functor.const J) z) j)
⊢ z =
    CategoryStruct.comp (Y := (pullback c.ι (Functor.map (Functor.const J) z)).obj j)
        (inv (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j))
        (NatTrans.app (pullback.fst c.ι (Functor.map (Functor.const J) z)) j) ≫
      c.ι.app j
have rw₅ : Eq (α := (pullback c.ι (Functor.map (Functor.const J) z)).obj j ⟶ c.pt)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
  (NatTrans.app (pullback.snd c.ι (Functor.map (Functor.const J) z)) j ≫ z)
Tactic: rw [Category.assoc, IsIso.eq_inv_comp, ← NatTrans.comp_app, pullback.condition,
    NatTrans.comp_app, Functor.const_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst_3 : SmallCategory J
Y : Functor.{w, v, w, u} J C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
inst_5 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
⊢ IsColimit (F := Y ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator.{v, u} C
have suffices : HasCoseparator.{w, u} (ShrinkHoms.{u} C)
Tactic: suffices HasCoseparator (ShrinkHoms C) from
    HasCoseparator.of_equivalence (ShrinkHoms.equivalence.{w} C).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasCoseparator.{w, u} (ShrinkHoms.{u} C)
have obtain : ∀ (G : ShrinkHoms.{u} C) (hG : IsCoseparator.{w, u} G), HasCoseparator.{w, u} (ShrinkHoms.{u} C)
Tactic: obtain ⟨G, -, hG⟩ := Abelian.has_injective_coseparator (separator (ShrinkHoms C))
    (isSeparator_separator _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
hG : IsSeparator.{v, u} G
X Y : C
p : X ⟶ Y
inst_2 : Mono p
hp : ¬IsIso p
⊢ ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : MorphismProperty.pushouts (generatingMonomorphisms G) i) (_ : ¬IsIso i) (_
    : Mono p'), i ≫ p' = p
have hp₁ : ¬∀ (G_1 : C),
    ObjectProperty.singleton.{v, u} G G_1 →
      Function.Surjective (α := (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op G_1)) X)) (β :=
        (fun (X : Type v) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op G_1)) Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (Opposite.op G_1)) p)) :
          (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (Opposite.op G_1)).obj X)) →
            (fun (X : Type v) ↦ X) ((coyoneda.obj (Opposite.op G_1)).obj Y))
Tactic: rw [hG.isDetector.isIso_iff_of_mono] at hp
Cleared hypotheses: hp