awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)

Tactic:
((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
    (MorphismProperty.of_isPullback
      ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.colim, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Limits.Cocone.ι, CategoryTheory.IsPullback.of_hasPullback, Iff.mp, CategoryTheory.Functor.const, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
refine_1 :
  Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
      (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z))) ≅
    Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
      (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
refine_2 : MorphismProperty.isomorphisms C (X := Functor.obj colim Y) (Functor.map colim c.ι)
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)

Tactic:
refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).1
    (MorphismProperty.of_isPullback
      ((IsPullback.of_hasPullback c.ι ((Functor.const _).map z)).map colim) ?_)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.colim, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Limits.Cocone.ι, CategoryTheory.IsPullback.of_hasPullback, Iff.mp, CategoryTheory.Functor.const, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
refine_1 :
  Iso.hom
        (Iso.refl
          (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
              (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).left) ≫
      (Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
          (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)).hom =
    (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
          (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).hom ≫
      Iso.hom
        (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
          (isColimitConstCocone J X))
⊢ Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
      (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z))) ≅
    Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
      (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)

Tactic:
refine Arrow.isoMk (Iso.refl _)
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isColimitConstCocone J X)) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
refine_1 :
  𝟙 (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)))
⊢ Iso.hom
        (Iso.refl
          (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
              (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).left) ≫
      (Arrow.mk (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
          (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)).hom =
    (Arrow.mk (X := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) z)))
          (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) z)))).hom ≫
      Iso.hom
        (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) X))
          (isColimitConstCocone J X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
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))))
⊢ 𝟙 (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)))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
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
⊢ 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:
rw [Category.id_comp, ι_colimMap_assoc, colimit.comp_coconePointUniqueUpToIso_hom,
      constCocone_ι, NatTrans.id_app, Category.comp_id]

Premises used: CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.NatTrans.id_app, CategoryTheory.Limits.constCocone_ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
⊢ 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:
apply hf

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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.ι)

Tactic:
((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).2
      ((inferInstance : IsIso (𝟙 c.pt)))

Premises used: Iff.mpr, inferInstance, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
refine_2 : Arrow.mk (X := Functor.obj colim Y) (Functor.map colim c.ι) ≅ Arrow.mk (𝟙 c.pt)
⊢ MorphismProperty.isomorphisms C (X := Functor.obj colim Y) (Functor.map colim c.ι)

Tactic:
refine ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ?_).2
      ((inferInstance : IsIso (𝟙 c.pt)))

Premises used: Iff.mpr, inferInstance, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
⊢ Arrow.mk (X := Functor.obj colim Y) (Functor.map colim c.ι) ≅ Arrow.mk (𝟙 c.pt)

Tactic:
exact Arrow.isoMk (IsColimit.coconePointUniqueUpToIso (colimit.isColimit Y) hc)
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
        (isColimitConstCocone J c.pt))

Premises used: CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
this :
  IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)
⊢ Epi (X := colimit (pullback c.ι (Functor.map (Functor.const J) z)))
    (f z : colimit (pullback c.ι (Functor.map (Functor.const J) z)) ⟶ X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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) [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
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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₀)
⊢ Mono c.ι

Tactic:
have := NatTrans.mono_of_mono_app c.ι
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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₀

Tactic:
⟨j, inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι _).app j, ?_⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F, CategoryTheory.Over.hom, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
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
⊢ ∃ (j₀ : J) (y : X ⟶ Y.obj j₀), z = y ≫ c.ι.app j₀

Tactic:
refine ⟨j, inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι _).app j, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
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
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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)
rw₅ 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)
⊢ 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Functor.const_map_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
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
this : IsFiltered J
⊢ IsColimit (F := Y ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)

Tactic:
exact Types.FilteredColimit.isColimitOf' _ _
      (surjectivity hc hXκ) (injectivity hc hXκ)

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
suffices : HasCoseparator.{w, u} (ShrinkHoms.{u} C)
⊢ HasCoseparator.{v, u} C

Tactic:
suffices HasCoseparator (ShrinkHoms C) from
    HasCoseparator.of_equivalence (ShrinkHoms.equivalence.{w} C).symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
obtain : ∀ (G : ShrinkHoms.{u} C) (hG : IsCoseparator.{w, u} G), HasCoseparator.{w, u} (ShrinkHoms.{u} C)
⊢ HasCoseparator.{w, u} (ShrinkHoms.{u} C)

Tactic:
obtain ⟨G, -, hG⟩ := Abelian.has_injective_coseparator (separator (ShrinkHoms C))
    (isSeparator_separator _)

Premises used: CategoryTheory.separator, CategoryTheory.Abelian.has_injective_coseparator, CategoryTheory.isSeparator_separator, CategoryTheory.ShrinkHoms
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
G : ShrinkHoms.{u} C
hG : IsCoseparator.{w, u} G
⊢ HasCoseparator.{w, u} (ShrinkHoms.{u} C)

Tactic:
⟨G, hG⟩

Premises used: CategoryTheory.HasCoseparator.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
G : ShrinkHoms.{u} C
hG : IsCoseparator.{w, u} G
⊢ HasCoseparator.{w, u} (ShrinkHoms.{u} C)

Tactic:
exact ⟨G, hG⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Small.{w, max u v} (Subobject.{v, u} G)
⊢ MorphismProperty.IsSmall.{w, v, u} (C := C)
    (MorphismProperty.ofHoms (X := Functor.obj Subobject.underlying) (Y := fun (X : Subobject.{v, u} G) ↦ G)
      fun (X : Subobject.{v, u} G) ↦ X.arrow)

Tactic:
infer_instance