awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Goal:
C : Type u
A : Type u₁
K : Type u₂
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} A
inst_2 : Category.{v₂, u₂} K
J : GrothendieckTopology.{v, u} C
inst_3 : HasFiniteLimits.{v₁, u₁} A
inst_4 : HasSheafify.{v, v₁, u, u₁} J A
inst_5 : HasColimitsOfShape.{v₂, u₂, v₁, u₁} K A
inst_6 : HasExactColimitsOfShape.{v₁, v₂, u₁, u₂} K A
⊢ HasExactColimitsOfShape K (Sheaf.{v, v₁, u, u₁} J A)

Tactic:
(sheafificationAdjunction J A).hasExactColimitsOfShape K

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.hasExactColimitsOfShape
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Goal:
C : Type u
A : Type u₁
K_1 : Type u₂
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} A
inst_2 : Category.{v₂, u₂} K_1
J : GrothendieckTopology.{v, u} C
inst_3 : HasFiniteLimits.{v₁, u₁} A
inst_4 : HasSheafify.{v, v₁, u, u₁} J A
inst_5 : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A
inst_6 : AB5OfSize.{v₂, u₂, v₁, u₁} A
K : Type u₂
x : Category.{v₂, u₂} K
h : IsFiltered.{v₂, u₂} K
⊢ HasExactColimitsOfShape K (Sheaf.{v, v₁, u, u₁} J A)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : EssentiallySmall.{v, v₂, u₂} C
J : GrothendieckTopology.{v₂, u₂} C
A : Type u₁
inst_2 : Category.{v₁, u₁} A
inst_3 : Abelian.{v₁, u₁} A
inst_4 : IsGrothendieckAbelian.{v, v₁, u₁} A
inst_5 :
  ∀ (X : Cᵒᵖ),
    HasLimitsOfShape
      (StructuredArrow.{v, v₂, v, u₂} (C := (SmallModel.{v, v₂, u₂} C)ᵒᵖ) X
        (Functor.op (Equivalence.inverse (equivSmallModel C))))
      A
inst_6 :
  HasSheafify.{v, v₁, v, u₁} (C := SmallModel.{v, v₂, u₂} C)
    (Functor.inducedTopology (Equivalence.inverse (equivSmallModel C)) J) A
⊢ IsGrothendieckAbelian.{v, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂} (Sheaf.{v₂, v₁, u₂, u₁} J A)

Tactic:
IsGrothendieckAbelian.of_equivalence
    ((equivSmallModel C).inverse.sheafInducedTopologyEquivOfIsCoverDense J A)

Premises used: CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense, CategoryTheory.IsGrothendieckAbelian.of_equivalence, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
⊢ HasFilteredColimitsOfSize.{w, w, v₂, u₂} D

Tactic:
have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
    ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D

Tactic:
⟨?_, hasFilteredColimits, ?_, ?_⟩

Premises used: CategoryTheory.IsGrothendieckAbelian.mk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
refine_1 : LocallySmall.{w, v₂, u₂} D
refine_2 : AB5OfSize.{w, w, v₂, u₂} D
refine_3 : HasSeparator.{v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D

Tactic:
refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ LocallySmall.{w, v₂, u₂} D

Tactic:
locallySmall_of_faithful α.inverse

Premises used: CategoryTheory.locallySmall_of_faithful, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ LocallySmall.{w, v₂, u₂} D

Tactic:
exact locallySmall_of_faithful α.inverse

Premises used: CategoryTheory.locallySmall_of_faithful, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

Tactic:
⟨fun _ _ _ => ?_⟩

Premises used: CategoryTheory.AB5OfSize.mk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
refine_2 : ∀ (x : Type w) (x_1 : Category.{w, w} x) (x_2 : IsFiltered x), HasExactColimitsOfShape.{v₂, w, u₂, w} x D
⊢ AB5OfSize.{w, w, v₂, u₂} D

Tactic:
refine ⟨fun _ _ _ => ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
x : Type w
x_1 : Category.{w, w} x
h : IsFiltered x
⊢ HasExactColimitsOfShape.{v₂, w, u₂, w} x D

Tactic:
HasExactColimitsOfShape.of_codomain_equivalence _ α

Premises used: CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
x : Type w
x_1 : Category.{w, w} x
h : IsFiltered x
⊢ HasExactColimitsOfShape.{v₂, w, u₂, w} x D

Tactic:
exact HasExactColimitsOfShape.of_codomain_equivalence _ α

Premises used: CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator.{v₂, u₂} D

Tactic:
HasSeparator.of_equivalence α

Premises used: CategoryTheory.HasSeparator.of_equivalence
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : Abelian.{v₂, u₂} D
inst_4 : IsGrothendieckAbelian.{w, v, u} C
α : Equivalence.{v, v₂, u, u₂} C D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator.{v₂, u₂} D

Tactic:
exact HasSeparator.of_equivalence α

Premises used: CategoryTheory.HasSeparator.of_equivalence
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
⊢ IsGrothendieckAbelian.{w, w, u} (ShrinkHoms.{u} C)

Tactic:
IsGrothendieckAbelian.of_equivalence <| ShrinkHoms.equivalence C

Premises used: CategoryTheory.IsGrothendieckAbelian.of_equivalence, CategoryTheory.ShrinkHoms.equivalence
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasColimitsOfSize.{w, w, v, u} C

Tactic:
has_colimits_of_finite_and_filtered

Premises used: CategoryTheory.Limits.has_colimits_of_finite_and_filtered
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasLimitsOfSize.{w, w, v, u} C

Tactic:
have : HasLimits.{w, u} (ShrinkHoms C) := hasLimits_of_hasColimits_of_hasSeparator
  Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence C |>.functor)

Premises used: CategoryTheory.Adjunction.has_limits_of_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
⊢ WellPowered.{w, v, u} C

Tactic:
wellPowered_of_equiv.{w} (ShrinkHoms.equivalence.{w} C).symm

Premises used: CategoryTheory.wellPowered_of_equiv, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasFiniteBiproducts.{v, u} C

Tactic:
have : HasFiniteBiproducts C := HasFiniteBiproducts.of_hasFiniteProducts
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{w, v, u} C
this : HasFiniteBiproducts.{v, u} C
⊢ AB4OfSize.{w, v, u} C

Tactic:
apply AB4.of_AB5

Premises used: CategoryTheory.AB4.of_AB5
-- 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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
dsimp : 𝟙 X ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ Y.map (Under.Hom.right f)
⊢ Functor.map (Functor.obj (Functor.const (Under j₀)) X) f ≫ y ≫ Y.map t₂.hom =
    (y ≫ Y.map t₁.hom) ≫ (Under.forget j₀ ⋙ Y).map f

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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ 𝟙 X ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ Y.map (Under.Hom.right f)

Tactic:
simp only [Category.id_comp, Category.assoc, ← Functor.map_comp, Under.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Under.w, 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
j₀ : J
y : X ⟶ Y.obj j₀
j : Under j₀
⊢ Eq (α := (kernel (g y)).obj j ⟶ Cocone.pt.{w, v, w, u} (J := Under j₀) (constCocone (Under j₀) X))
    (NatTrans.app (kernel.ι (g y)) j ≫ NatTrans.app (Cocone.ι (constCocone (Under j₀) X)) j :
      (kernel (g y)).obj j ⟶
        Functor.obj.{w, v, w, u}
          (Functor.obj (Functor.const (Under j₀)) (Cocone.pt.{w, v, w, u} (J := Under j₀) (constCocone (Under j₀) X)))
          j)
    (NatTrans.app (kernel.ι (g y)) j)

Tactic:
simp
-- 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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst_4 : IsFiltered J
j : Under j₀
⊢ (colimit.cocone (ShortComplex.X₁ (ShortComplex.mk (X₁ := kernel (g y)) (kernel.ι (g y)) (g y) ⋯))).ι.app j ≫ f y =
    NatTrans.app (ShortComplex.f (ShortComplex.mk (X₁ := kernel (g y)) (kernel.ι (g y)) (g y) ⋯)) j ≫
      NatTrans.app (Cocone.ι (constCocone (Under j₀) X)) j

Tactic:
simpa using hf y j

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst_4 : IsFiltered J
x : Under j₀
⊢ Eq.{v + 1} (α :=
    (ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel (g y)) (kernel.ι (g y)) (g y) ⋯)).obj x ⟶
      Cocone.pt (F := ShortComplex.X₃ (ShortComplex.mk (X₁ := kernel (g y)) (kernel.ι (g y)) (g y) ⋯))
        (Cocone.whisker (Under.forget j₀) c))
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Under j₀)) (Cocone.pt.{w, v, w, u} (J := Under j₀) (constCocone (Under j₀) X))) x)
      (NatTrans.app (Cocone.ι (constCocone (Under j₀) X)) x) 0)
    (NatTrans.app (ShortComplex.g (ShortComplex.mk (X₁ := kernel (g y)) (kernel.ι (g y)) (g y) ⋯)) x ≫
      NatTrans.app (Cocone.ι (Cocone.whisker (Under.forget j₀) c)) x)

Tactic:
simpa using hy.symm

Premises used: Eq.symm
-- 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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst_4 : IsFiltered J
⊢ Epi (X := colimit (kernel (g y))) (f y : colimit (kernel (g y)) ⟶ X)

Tactic:
exact (colim.exact_mapShortComplex
    ((ShortComplex.mk _ _ (kernel.condition (g y))).exact_of_f_is_kernel
      (kernelIsKernel (g y)))
    (colimit.isColimit _) (isColimitConstCocone _ _)
    ((Functor.Final.isColimitWhiskerEquiv (Under.forget j₀) c).symm hc) (f y) 0
    (fun j ↦ by simpa using hf y j)
    (fun _ ↦ by simpa using hy.symm)).epi_f rfl

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f, CategoryTheory.ShortComplex.mk, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.kernel.condition, CategoryTheory.ShortComplex.Exact.epi_f, CategoryTheory.Under.forget, CategoryTheory.Limits.colim.exact_mapShortComplex, CategoryTheory.Limits.isColimitConstCocone, CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, CategoryTheory.Limits.kernelIsKernel, Equiv.symm, OfNat.ofNat, DFunLike.coe, rfl
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
⊢ 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
⊢ (colimit.cocone (kernel (g y))).ι.app j ≫ f y = ((F y).obj j).obj (P := Over.isMono X).hom

Tactic:
simpa using hf y j

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
obtain :
  ∀ (j : Under j₀) (h : IsIso ((F y).obj j).obj (P := Over.isMono X).hom), ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0

Tactic:
obtain ⟨j, h⟩ := exists_isIso_of_functor_from_monoOver (F y) hXκ _
      (colimit.isColimit (kernel (g y))) (f y) (fun j ↦ by simpa using hf y j)
      (epi_f hc hy)

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F, CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.kernel, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso (X := (kernel (g y)).obj j) (NatTrans.app (kernel.ι (g y)) j)
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0

Tactic:
⟨j.right, j.hom, ?_⟩

Premises used: CategoryTheory.Under.hom, CategoryTheory.Under.right, Exists.intro
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso (X := (kernel (g y)).obj j) (NatTrans.app (kernel.ι (g y)) j)
refine : y ≫ Y.map j.hom = 0
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y ≫ Y.map φ = 0

Tactic:
refine ⟨j.right, j.hom, ?_⟩
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso (X := (kernel (g y)).obj j) (NatTrans.app (kernel.ι (g y)) j)
⊢ y ≫ Y.map j.hom = 0

Tactic:
simpa only [← cancel_epi ((kernel.ι (g y)).app j), comp_zero]
    using NatTrans.congr_app (kernel.condition (g y)) j

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernel.condition, CategoryTheory.NatTrans.congr_app, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app, CategoryTheory.Limits.kernel.ι
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
rw : y₁ ≫ c.ι.app j₀ - y₂ ≫ c.ι.app j₀ = 0
rw₁ : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
rw₂ rw₃ : y₂ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ (y₁ - y₂) ≫ c.ι.app j₀ = 0

Tactic:
rw [Preadditive.sub_comp, sub_eq_zero, hy]

Premises used: sub_eq_zero, CategoryTheory.Preadditive.sub_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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
obtain : ∀ (j : J) (φ : j₀ ⟶ j) (hφ : (y₁ - y₂) ≫ Y.map φ = 0), ∃ (j : J) (φ : j₀ ⟶ j), y₁ ≫ Y.map φ = y₂ ≫ Y.map φ
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Tactic:
obtain ⟨j, φ, hφ⟩ := injectivity₀ hc hXκ (y₁ - y₂)
    (by rw [Preadditive.sub_comp, sub_eq_zero, hy])

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀, HSub.hSub
-- 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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
j : J
φ : j₀ ⟶ j
hφ : (y₁ - y₂) ≫ Y.map φ = 0
⊢ y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hφ

Premises used: sub_eq_zero, CategoryTheory.Preadditive.sub_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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_4 : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject.{v, u} X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
j : J
φ : j₀ ⟶ j
hφ : (y₁ - y₂) ≫ Y.map φ = 0
⊢ ∃ (j : J) (φ : j₀ ⟶ j), y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Tactic:
exact ⟨j, φ, by simpa only [Preadditive.sub_comp, sub_eq_zero] using hφ⟩
-- 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
z : X ⟶ c.pt
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:
colimit.ι_desc _ _

Premises used: CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.f, CategoryTheory.Limits.colimit.ι_desc