awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
ofShape :
  ∀ (J : Type w') [inst_5 : Category.{w, w'} J] [inst_6 : IsCofiltered.{w, w'} J],
    HasExactLimitsOfShape.{v, w, u, w'} J C
⊢ AB5StarOfSize.{w, w', v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
ofShape : ∀ [inst_5 : Category.{w, w'} J] [inst_6 : IsCofiltered.{w, w'} J], HasExactLimitsOfShape.{v, w, u, w'} J C
⊢ ∀ [inst_5 : Category.{w, w'} J] [inst_6 : IsCofiltered.{w, w'} J], HasExactLimitsOfShape.{v, w, u, w'} J C

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
ofShape : ∀ [inst_6 : IsCofiltered.{w, w'} J], HasExactLimitsOfShape.{v, w, u, w'} J C
⊢ ∀ [inst_6 : IsCofiltered.{w, w'} J], HasExactLimitsOfShape.{v, w, u, w'} J C

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsCofiltered.{w, w'} J
⊢ IsCofiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))

Tactic:
haveI := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
this_1 : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsCofiltered.{w, w'} J
this : IsCofiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactLimitsOfShape.{v, w, u, w'} J C

Tactic:
HasExactLimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm

Premises used: CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Shrink.equivalence, CategoryTheory.Equivalence.trans, CategoryTheory.ShrinkHoms, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5StarOfSize.{w₂, w₂', v, u} C
this_1 : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsCofiltered.{w, w'} J
this : IsCofiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactLimitsOfShape.{v, w, u, w'} J C

Tactic:
exact HasExactLimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{max w w₂, max w' w₂', v, u} C
inst_2 : AB5StarOfSize.{max w w₂, max w' w₂', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C

Tactic:
AB5StarOfSize_of_univLE C

Premises used: CategoryTheory.AB5StarOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : HasFiniteLimits.{v, u} C
⊢ PreservesFiniteLimits (C := Functor.{w, v, w, u} (Discrete α) C) (liftToFinset C α)

Tactic:
preservesFiniteLimits_of_evaluation _ fun I =>
    letI : PreservesFiniteLimits (colim (J := Discrete I) (C := C)) :=
      preservesFiniteLimits_of_natIso HasBiproductsOfShape.colimIsoLim.symm
    letI : PreservesFiniteLimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj
        (Discrete.functor fun x ↦ ↑x)) :=
      ⟨fun J _ _ => whiskeringLeft_preservesLimitsOfShape J _⟩
    letI : PreservesFiniteLimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj
        (Discrete.functor (·.val)) ⋙ colim) :=
      comp_preservesFiniteLimits _ _
    preservesFiniteLimits_of_natIso (liftToFinsetEvaluationIso I).symm

Premises used: CategoryTheory.preservesFiniteLimits_of_evaluation, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetEvaluationIso, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : HasFiniteColimits.{v, u} C
⊢ PreservesFiniteColimits (C := Functor.{w, v, w, u} (Discrete α) C) (liftToFinset C α)

Tactic:
preservesFiniteColimits_of_evaluation _ fun ⟨I⟩ =>
    letI : PreservesFiniteColimits (lim (J := Discrete I) (C := C)) :=
      preservesFiniteColimits_of_natIso HasBiproductsOfShape.colimIsoLim
    letI : PreservesFiniteColimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj
        (Discrete.functor fun x ↦ ↑x)) := ⟨fun _ _ _ => inferInstance⟩
    letI : PreservesFiniteColimits ((whiskeringLeft (Discrete I) (Discrete α) C).obj
        (Discrete.functor (·.val)) ⋙ lim) :=
      comp_preservesFiniteColimits _ _
    preservesFiniteColimits_of_natIso (liftToFinsetEvaluationIso _ _ I).symm

Premises used: CategoryTheory.preservesFiniteColimits_of_evaluation, Opposite, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetEvaluationIso, Finset, CategoryTheory.Functor.comp, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset, _private.0.CategoryTheory.preservesFiniteColimits_liftToFinset.match_1, CategoryTheory.Limits.PreservesFiniteColimits, CategoryTheory.Iso.symm, CategoryTheory.evaluation, CategoryTheory.Functor.obj, CategoryTheory.Discrete, CategoryTheory.Limits.preservesFiniteColimits_of_natIso
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableCoproducts.{v, u} C
inst_2 : HasFiniteLimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_5 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
pos : ∀ [inst_5 : Countable J] (h : Finite J), HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
neg : ∀ [inst_5 : Countable J] (h : ¬Finite J), HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
⊢ ∀ [inst_5 : Countable J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
by_cases h : Finite J

Premises used: Finite
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableCoproducts.{v, u} C
inst_2 : HasFiniteLimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : Finite J
⊢ HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableCoproducts.{v, u} C
inst_2 : HasFiniteLimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : ¬Finite J
⊢ Infinite J

Tactic:
have : Infinite J := ⟨h⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableCoproducts.{v, u} C
inst_2 : HasFiniteLimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : ¬Finite J
this : Infinite J
x : Encodable J := Encodable.ofCountable J
x_1 : Denumerable J := Denumerable.ofEncodableOfInfinite J
⊢ HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
hasExactColimitsOfShape_of_final C (Discrete.equivalence (Denumerable.eqv J)).inverse

Premises used: Denumerable.eqv, CategoryTheory.hasExactColimitsOfShape_of_final, CategoryTheory.Discrete.equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableCoproducts.{v, u} C
inst_2 : HasFiniteLimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : ¬Finite J
this : Infinite J
x : Encodable J := Encodable.ofCountable J
x_1 : Denumerable J := Denumerable.ofEncodableOfInfinite J
⊢ HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
exact hasExactColimitsOfShape_of_final C (Discrete.equivalence (Denumerable.eqv J)).inverse

Premises used: Denumerable.eqv, CategoryTheory.hasExactColimitsOfShape_of_final, CategoryTheory.Discrete.equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableProducts.{v, u} C
inst_2 : HasFiniteColimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_5 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
pos : ∀ [inst_5 : Countable J] (h : Finite J), HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
neg : ∀ [inst_5 : Countable J] (h : ¬Finite J), HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
⊢ ∀ [inst_5 : Countable J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
by_cases h : Finite J

Premises used: Finite
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableProducts.{v, u} C
inst_2 : HasFiniteColimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : Finite J
⊢ HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableProducts.{v, u} C
inst_2 : HasFiniteColimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : ¬Finite J
⊢ Infinite J

Tactic:
have : Infinite J := ⟨h⟩
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableProducts.{v, u} C
inst_2 : HasFiniteColimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : ¬Finite J
this : Infinite J
x : Encodable J := Encodable.ofCountable J
x_1 : Denumerable J := Denumerable.ofEncodableOfInfinite J
⊢ HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
hasExactLimitsOfShape_of_initial C (Discrete.equivalence (Denumerable.eqv J)).inverse

Premises used: Denumerable.eqv, CategoryTheory.hasExactLimitsOfShape_of_initial, CategoryTheory.Discrete.equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCountableProducts.{v, u} C
inst_2 : HasFiniteColimits.{v, u} C
inst_3 : ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
inst_4 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
J : Type
inst_5 : Countable J
h : ¬Finite J
this : Infinite J
x : Encodable J := Encodable.ofCountable J
x_1 : Denumerable J := Denumerable.ofEncodableOfInfinite J
⊢ HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
exact hasExactLimitsOfShape_of_initial C (Discrete.equivalence (Denumerable.eqv J)).inverse

Premises used: Denumerable.eqv, CategoryTheory.hasExactLimitsOfShape_of_initial, CategoryTheory.Discrete.equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasCountableCoproducts.{v, u} C
inst_6 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
inst : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
⊢ CountableAB4.{v, u} C

Tactic:
apply +allowSynthFailures CountableAB4.of_hasExactColimitsOfShape_nat_and_finite

Premises used: CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : HasFiniteLimits.{v, u} C
inst_4 : HasCountableCoproducts.{v, u} C
inst_5 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
⊢ ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
fun _ ↦ inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : HasFiniteLimits.{v, u} C
inst_4 : HasCountableCoproducts.{v, u} C
inst_5 : HasExactColimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
⊢ ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
exact fun _ ↦ inferInstance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : HasFiniteColimits.{v, u} C
inst_5 : HasCountableProducts.{v, u} C
inst_6 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
inst : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
⊢ CountableAB4Star.{v, u} C

Tactic:
apply +allowSynthFailures CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite

Premises used: CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : HasFiniteColimits.{v, u} C
inst_4 : HasCountableProducts.{v, u} C
inst_5 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
⊢ ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
fun _ ↦ inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : HasFiniteColimits.{v, u} C
inst_4 : HasCountableProducts.{v, u} C
inst_5 : HasExactLimitsOfShape.{v, 0, u, 0} (Discrete ℕ) C
⊢ ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C

Tactic:
exact fun _ ↦ inferInstance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasColimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
inst : PreservesHomology (C := Functor.{v', v, u', u} J C) colim
inst₁ : Functor.Additive (C := Functor.{v', v, u', u} J C) colim
⊢ PreservesFiniteLimits (C := Functor.{v', v, u', u} J C) colim

Tactic:
apply +allowSynthFailures preservesFiniteLimits_of_preservesHomology

Premises used: CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasColimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
⊢ PreservesHomology (C := Functor.{v', v, u', u} J C) colim

Tactic:
preservesHomology_of_preservesMonos_and_cokernels _

Premises used: CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasColimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
⊢ PreservesHomology (C := Functor.{v', v, u', u} J C) colim

Tactic:
exact preservesHomology_of_preservesMonos_and_cokernels _

Premises used: CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasColimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
⊢ Functor.Additive (C := Functor.{v', v, u', u} J C) colim

Tactic:
additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasColimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
⊢ Functor.Additive (C := Functor.{v', v, u', u} J C) colim

Tactic:
exact additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesEpimorphisms (C := Functor.{v', v, u', u} J C) lim
inst : PreservesHomology (C := Functor.{v', v, u', u} J C) lim
inst₁ : Functor.Additive (C := Functor.{v', v, u', u} J C) lim
⊢ PreservesFiniteColimits (C := Functor.{v', v, u', u} J C) lim

Tactic:
apply +allowSynthFailures preservesFiniteColimits_of_preservesHomology

Premises used: CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasLimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesEpimorphisms (C := Functor.{v', v, u', u} J C) lim
⊢ PreservesHomology (C := Functor.{v', v, u', u} J C) lim

Tactic:
preservesHomology_of_preservesEpis_and_kernels _

Premises used: CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasLimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesEpimorphisms (C := Functor.{v', v, u', u} J C) lim
⊢ PreservesHomology (C := Functor.{v', v, u', u} J C) lim

Tactic:
exact preservesHomology_of_preservesEpis_and_kernels _

Premises used: CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasLimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesEpimorphisms (C := Functor.{v', v, u', u} J C) lim
⊢ Functor.Additive (C := Functor.{v', v, u', u} J C) lim

Tactic:
additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : HasLimitsOfShape.{v', u', v, u} J C
inst_4 : PreservesEpimorphisms (C := Functor.{v', v, u', u} J C) lim
⊢ Functor.Additive (C := Functor.{v', v, u', u} J C) lim

Tactic:
exact additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : Functor.PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
X₁ X₂ : Functor.{v', v, u', u} J C
φ : X₁ ⟶ X₂
inst_4 : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
⊢ Mono f

Tactic:
((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
    ((inferInstance : Mono (colim.map φ)))

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.monomorphisms, inferInstance, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : Functor.PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
X₁ X₂ : Functor.{v', v, u', u} J C
φ : X₁ ⟶ X₂
inst_4 : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
refine : Arrow.mk f ≅ Arrow.mk (X := Functor.obj colim X₁) (Functor.map colim φ)
⊢ Mono f

Tactic:
refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
    ((inferInstance : Mono (colim.map φ)))

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.monomorphisms, inferInstance, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : Functor.PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
X₁ X₂ : Functor.{v', v, u', u} J C
φ : X₁ ⟶ X₂
inst_4 : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
dsimp :
  Eq (α := X₁.obj j ⟶ colimit X₂)
    (c₁.ι.app j ≫
      CategoryStruct.comp (Y := colimit X₁) (Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit X₁)))
        (colimMap φ))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
⊢ c₁.ι.app j ≫
      Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit X₁)) ≫
        (Arrow.mk (X := Functor.obj colim X₁) (Functor.map colim φ)).hom =
    c₁.ι.app j ≫ (Arrow.mk f).hom ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂))

Tactic:
dsimp