awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
this : Abelian.{v', u'} D := abelian L P
rw : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ PreservesFiniteColimits L

Tactic:
rw [((Functor.preservesFiniteColimits_tfae L).out 3 2 :)]

Premises used: List.TFAE.out, OfNat.ofNat, CategoryTheory.Functor.preservesFiniteColimits_tfae
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
this : Abelian.{v', u'} D := abelian L P
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L

Tactic:
_
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
this : Abelian.{v', u'} D := abelian L P
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
preservesCokernel L P f

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernel
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
this : Abelian.{v', u'} D := abelian L P
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
exact preservesCokernel L P f

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernel
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
this : Abelian.{v', u'} D := abelian L P
rw : Mono (L.map f) ∧ Epi (L.map f) ↔ P.isoModSerre f
rw₁ : P.monoModSerre f ∧ Epi (L.map f) ↔ P.isoModSerre f
rw₂ : P.monoModSerre f ∧ P.epiModSerre f ↔ P.isoModSerre f
rw₃ rw₄ : P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f
⊢ IsIso (L.map f) ↔ P.isoModSerre f

Tactic:
rw [isIso_iff_mono_and_epi, mono_map_iff L P, epi_map_iff L P, isoModSerre_iff]

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_iff, CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_iff, CategoryTheory.isIso_iff_mono_and_epi, CategoryTheory.ObjectProperty.isoModSerre_iff
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) L f ↔ P.isoModSerre f
⊢ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) L = P.isoModSerre

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
⊢ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) L f ↔ P.isoModSerre f

Tactic:
simp [isIso_map_iff L P]

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.isIso_map_iff
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this : Abelian.{v', u'} D := abelian L P
⊢ PreservesFiniteLimits L

Tactic:
have := preservesFiniteLimits L P
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteLimits L
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits G

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteLimits _ _⟩

Premises used: Iff.intro, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteLimits L
refine : PreservesFiniteLimits (L ⋙ G) → PreservesFiniteLimits G
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits G

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteLimits _ _⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
⊢ G.Additive

Tactic:
have := (Localization.functor_additive_iff L P.isoModSerre G).mpr
    (L ⋙ G).additive_of_preserves_binary_products
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
⊢ PreservesFiniteLimits G

Tactic:
((Functor.preservesFiniteLimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)

Premises used: CategoryTheory.Functor.preservesFiniteLimits_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
refine : ∀ (x x_1 : D) (f : x ⟶ x_1), PreservesLimit (parallelPair f 0) G
⊢ PreservesFiniteLimits G

Tactic:
refine ((Functor.preservesFiniteLimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)

Premises used: CategoryTheory.Functor.preservesFiniteLimits_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
obtain : ∀ (f' : Arrow.{v, u} C) (iso : L.mapArrow.obj f' ≅ Arrow.mk f), PreservesLimit (parallelPair f 0) G
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
obtain ⟨f', ⟨iso⟩⟩ :=
    (Localization.essSurj_mapArrow L P.isoModSerre).mem_essImage (Arrow.mk f)

Premises used: CategoryTheory.Functor.EssSurj.mem_essImage, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
⊢ PreservesLimit (parallelPair (L.map f'.hom) 0) G

Tactic:
have : PreservesLimit (parallelPair (L.map f'.hom) 0) G :=
    preservesLimit_of_preserves_limit_cone
      (KernelFork.isLimitMapConeEquiv _ _
        (isLimitOfPreserves L (kernelIsKernel f'.hom)))
          ((KernelFork.isLimitMapConeEquiv _ G).symm
            (KernelFork.isLimitMapConeEquiv _ (L ⋙ G)
              (isLimitOfPreserves (L ⋙ G) (kernelIsKernel f'.hom))))
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this_3 : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
this : PreservesLimit (parallelPair (L.map f'.hom) 0) G
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
preservesLimit_of_iso_diagram G
    (show parallelPair (L.map f'.hom) 0 ≅ parallelPair f 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso iso) (Arrow.rightFunc.mapIso iso))

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Arrow.leftFunc, CategoryTheory.Limits.parallelPair.ext, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this_3 : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
this : PreservesLimit (parallelPair (L.map f'.hom) 0) G
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
exact preservesLimit_of_iso_diagram G
    (show parallelPair (L.map f'.hom) 0 ≅ parallelPair f 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso iso) (Arrow.rightFunc.mapIso iso))

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Arrow.leftFunc, CategoryTheory.Limits.parallelPair.ext, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this : Abelian.{v', u'} D := abelian L P
⊢ PreservesFiniteColimits L

Tactic:
have := preservesFiniteColimits L P
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteColimits _ _⟩

Premises used: Iff.intro, CategoryTheory.Limits.comp_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
refine : PreservesFiniteColimits (L ⋙ G) → PreservesFiniteColimits G
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteColimits _ _⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
⊢ PreservesBinaryBiproducts (L ⋙ G)

Tactic:
have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : PreservesBinaryBiproducts (L ⋙ G)
⊢ (L ⋙ G).Additive

Tactic:
Functor.additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : PreservesBinaryBiproducts (L ⋙ G)
⊢ (L ⋙ G).Additive

Tactic:
exact Functor.additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
⊢ G.Additive

Tactic:
have := (Localization.functor_additive_iff L P.isoModSerre G).mpr (by
    have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)
    exact Functor.additive_of_preservesBinaryBiproducts _)
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
⊢ PreservesFiniteColimits G

Tactic:
((Functor.preservesFiniteColimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)

Premises used: List.TFAE.out, Iff.mp, OfNat.ofNat, CategoryTheory.Functor.preservesFiniteColimits_tfae
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
refine : ∀ (x x_1 : D) (f : x ⟶ x_1), PreservesColimit (parallelPair f 0) G
⊢ PreservesFiniteColimits G

Tactic:
refine ((Functor.preservesFiniteColimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)

Premises used: List.TFAE.out, Iff.mp, OfNat.ofNat, CategoryTheory.Functor.preservesFiniteColimits_tfae
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
obtain : ∀ (f' : Arrow.{v, u} C) (iso : L.mapArrow.obj f' ≅ Arrow.mk f), PreservesColimit (parallelPair f 0) G
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
obtain ⟨f', ⟨iso⟩⟩ :=
    (Localization.essSurj_mapArrow L P.isoModSerre).mem_essImage (Arrow.mk f)

Premises used: CategoryTheory.Functor.EssSurj.mem_essImage, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
⊢ PreservesColimit (parallelPair (L.map f'.hom) 0) G

Tactic:
have : PreservesColimit (parallelPair (L.map f'.hom) 0) G :=
    preservesColimit_of_preserves_colimit_cocone
      (CokernelCofork.isColimitMapCoconeEquiv _ _
        (isColimitOfPreserves L (cokernelIsCokernel f'.hom)))
          ((CokernelCofork.isColimitMapCoconeEquiv _ G).symm
            (CokernelCofork.isColimitMapCoconeEquiv _ (L ⋙ G)
              (isColimitOfPreserves (L ⋙ G) (cokernelIsCokernel f'.hom))))
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this_3 : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
this : PreservesColimit (parallelPair (L.map f'.hom) 0) G
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
preservesColimit_of_iso_diagram G
    (show parallelPair (L.map f'.hom) 0 ≅ parallelPair f 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso iso) (Arrow.rightFunc.mapIso iso))

Premises used: CategoryTheory.Arrow.leftFunc, CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Limits.parallelPair.ext, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this_3 : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
this : PreservesColimit (parallelPair (L.map f'.hom) 0) G
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
exact preservesColimit_of_iso_diagram G
    (show parallelPair (L.map f'.hom) 0 ≅ parallelPair f 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso iso) (Arrow.rightFunc.mapIso iso))

Premises used: CategoryTheory.Arrow.leftFunc, CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Limits.parallelPair.ext, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.mapIso