awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
this : HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D
x : Type
x_1 : SmallCategory x
x_2 : FinCategory x
K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D
⊢ PreservesLimit K colim
have refine : Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor) colim
Tactic: refine preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasColimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactColimitsOfShape.{v, v_1, u, u_1} J C
this : HasColimitsOfShape.{v_1, u_1, v_2, u_2} J D
x : Type
x_1 : SmallCategory x
x_2 : FinCategory x
K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor) colim
have apply : Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ C)
  (obj (Equivalence.functor e.symm.congrRight) (Equivalence.inverse e.congrRight ⋙ colim ⋙ e.functor))
  (obj (Equivalence.functor e.symm.congrRight) colim)
Tactic: apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
⊢ HasExactLimitsOfShape.{v_2, v_1, u_2, u_1} J D
have this : HasLimitsOfShape.{v_1, u_1, v_2, u_2} J D
Tactic: haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{v_1, u_1, v_2, u_2} J D
⊢ HasExactLimitsOfShape.{v_2, v_1, u_2, u_1} J D
have refine : ∀ (x : Type) (x_1 : SmallCategory x) (x_2 : FinCategory x) (K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D),
  PreservesColimit K lim
Tactic: refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{v_1, u_1, v_2, u_2} J D
x : Type
x_1 : SmallCategory x
x_2 : FinCategory x
K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D
⊢ PreservesColimit K lim
have refine : Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor) lim
Tactic: refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
D : Type u_2
inst_2 : Category.{v_2, u_2} D
e : Equivalence.{v, v_2, u, u_2} C D
inst_3 : HasLimitsOfShape.{v_1, u_1, v, u} J C
inst_4 : HasExactLimitsOfShape.{v, v_1, u, u_1} J C
this : HasLimitsOfShape.{v_1, u_1, v_2, u_2} J D
x : Type
x_1 : SmallCategory x
x_2 : FinCategory x
K : x ⥤ Functor.{v_1, v_2, u_1, u_2} J D
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ D) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor) lim
have apply : Iso (C := Functor.{v_1, v_2, u_1, u_2} J D ⥤ C)
  (obj (Equivalence.functor e.symm.congrRight) (Equivalence.inverse e.congrRight ⋙ lim ⋙ e.functor))
  (obj (Equivalence.functor e.symm.congrRight) lim)
Tactic: apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasColimitsOfShape.{v', u', v, u} J C
inst_6 : HasColimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_8 : HasFiniteLimits.{v'', u''} D
inst_9 : PreservesFiniteLimits F
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v'', u', u''} J D
⊢ PreservesLimit H colim
have this : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
Tactic: have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : G.Full
inst_3 : G.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasColimitsOfShape.{v', u', v, u} J C
inst_6 : HasColimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_8 : HasFiniteLimits.{v'', u''} D
inst_9 : PreservesFiniteLimits F
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v'', u', u''} J D
this : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
⊢ PreservesLimit H colim
have this₁ : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
Tactic: have : PreservesColimitsOfSize.{v', u'} F := adj.leftAdjoint_preservesColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasLimitsOfShape.{v', u', v, u} J C
inst_6 : HasLimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactLimitsOfShape.{v'', v', u'', u'} J D
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesFiniteColimits G
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v, u', u} J C
⊢ PreservesColimit H lim
have this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
Tactic: have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
G : Functor.{v'', v, u'', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
J : Type u'
inst_4 : Category.{v', u'} J
inst_5 : HasLimitsOfShape.{v', u', v, u} J C
inst_6 : HasLimitsOfShape.{v', u', v'', u''} J D
inst_7 : HasExactLimitsOfShape.{v'', v', u'', u'} J D
inst_8 : HasFiniteColimits.{v, u} C
inst_9 : PreservesFiniteColimits G
K : Type
x : SmallCategory K
x_1 : FinCategory K
H : K ⥤ Functor.{v', v, u', u} J C
this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
⊢ PreservesColimit H lim
have this₁ : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
Tactic: have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
⊢ AB5OfSize.{w, w', v, u} C
have this : HasFilteredColimitsOfSize.{w, w', v, u} C
Tactic: haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
⊢ AB5OfSize.{w, w', v, u} C
have ofShape : ∀ (J : Type w') [inst_5 : Category.{w, w'} J] [inst_6 : IsFiltered.{w, w'} J], HasExactColimitsOfShape.{v, w, u, w'} J C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst_2 : UnivLE.{w, w₂}
inst_3 : UnivLE.{w', w₂'}
inst_4 : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst_5 : Category.{w, w'} J
inst_6 : IsFiltered.{w, w'} J
⊢ HasExactColimitsOfShape.{v, w, u, w'} J C
have this₁ : IsFiltered.{w₂, w₂'} (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
Tactic: haveI := IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
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
⊢ AB5StarOfSize.{w, w', v, u} C
have this : HasCofilteredLimitsOfSize.{w, w', v, u} C
Tactic: haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ AB5StarOfSize.{w, w', v, u} C
have ofShape : ∀ (J : Type w') [inst_5 : Category.{w, w'} J] [inst_6 : IsCofiltered.{w, w'} J], HasExactLimitsOfShape.{v, w, u, w'} J C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
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
⊢ HasExactLimitsOfShape.{v, w, u, w'} J C
have this₁ : 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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ ∀ [inst_5 : Countable J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
have pos : ∀ [inst_5 : Countable J] (h : Finite J), HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
Tactic: by_cases h : Finite J
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ ∀ [inst_5 : Countable J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
have neg : ∀ [inst_5 : Countable J] (h : ¬Finite J), HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
Tactic: by_cases h : Finite J
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
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
have this : Infinite J
Tactic: have : Infinite J := ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ ∀ [inst_5 : Countable J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
have pos : ∀ [inst_5 : Countable J] (h : Finite J), HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
Tactic: by_cases h : Finite J
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ ∀ [inst_5 : Countable J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
have neg : ∀ [inst_5 : Countable J] (h : ¬Finite J), HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
Tactic: by_cases h : Finite J
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (hypothesis)
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
have this : Infinite J
Tactic: have : Infinite J := ⟨h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ CountableAB4.{v, u} C
have inst : ∀ (J : Type) [inst_6 : Finite J], HasExactColimitsOfShape.{v, 0, u, 0} (Discrete J) C
Tactic: apply +allowSynthFailures CountableAB4.of_hasExactColimitsOfShape_nat_and_finite
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ CountableAB4Star.{v, u} C
have inst : ∀ (J : Type) [inst_6 : Finite J], HasExactLimitsOfShape.{v, 0, u, 0} (Discrete J) C
Tactic: apply +allowSynthFailures CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ PreservesFiniteLimits (C := Functor.{v', v, u', u} J C) colim
have inst : PreservesHomology (C := Functor.{v', v, u', u} J C) colim
Tactic: apply +allowSynthFailures preservesFiniteLimits_of_preservesHomology
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ PreservesFiniteLimits (C := Functor.{v', v, u', u} J C) colim
have inst₁ : Functor.Additive (C := Functor.{v', v, u', u} J C) colim
Tactic: apply +allowSynthFailures preservesFiniteLimits_of_preservesHomology
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ PreservesFiniteColimits (C := Functor.{v', v, u', u} J C) lim
have inst : PreservesHomology (C := Functor.{v', v, u', u} J C) lim
Tactic: apply +allowSynthFailures preservesFiniteColimits_of_preservesHomology
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic (goal)
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
⊢ PreservesFiniteColimits (C := Functor.{v', v, u', u} J C) lim
have inst₁ : Functor.Additive (C := Functor.{v', v, u', u} J C) lim
Tactic: apply +allowSynthFailures preservesFiniteColimits_of_preservesHomology
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
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
have refine : Arrow.mk f ≅ Arrow.mk (X := Functor.obj colim X₁) (Functor.map colim φ)
Tactic: refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
    ((inferInstance : Mono (colim.map φ)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
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
⊢ 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₂))
have 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₂)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
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
⊢ 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₂)))
have rw : Eq (α := X₁.obj j ⟶ colimit X₂) ((colimit.cocone X₁).ι.app j ≫ colimMap φ)
  (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
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
rw :
  Eq (α := X₁.obj j ⟶ colimit X₂) ((colimit.cocone X₁).ι.app j ≫ colimMap φ)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
⊢ 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₂)))
have rw₁ : Eq (α := X₁.obj j ⟶ colimit X₂) (CategoryStruct.comp (Y := (colimit.cocone X₁).pt) (colimit.ι X₁ j) (colimMap φ))
  (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
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
rw :
  Eq (α := X₁.obj j ⟶ colimit X₂) ((colimit.cocone X₁).ι.app j ≫ colimMap φ)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
rw₁ :
  Eq (α := X₁.obj j ⟶ colimit X₂) (CategoryStruct.comp (Y := (colimit.cocone X₁).pt) (colimit.ι X₁ j) (colimMap φ))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
⊢ 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₂)))
have rw₂ : Eq (α := X₁.obj j ⟶ colimit X₂) (φ.app j ≫ colimit.ι X₂ j)
  (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]