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
X Y : D
f : X ⟶ Y
g : Arrow.{v, u} C
e : L.mapArrow.obj g ≅ Arrow.mk f
⊢ PreservesColimit (parallelPair g.hom 0) L

Tactic:
have := preservesCokernel L P g.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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
g : Arrow.{v, u} C
e : L.mapArrow.obj g ≅ Arrow.mk f
this : PreservesColimit (parallelPair g.hom 0) L
⊢ HasColimit (parallelPair (L.map g.hom) 0)

Tactic:
have : HasColimit (parallelPair (L.map g.hom) 0) :=
      ⟨_, (CokernelCofork.isColimitMapCoconeEquiv _ L).1
        (isColimitOfPreserves L (cokernelIsCokernel g.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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
g : Arrow.{v, u} C
e : L.mapArrow.obj g ≅ Arrow.mk f
this_1 : PreservesColimit (parallelPair g.hom 0) L
this : HasColimit (parallelPair (L.map g.hom) 0)
⊢ HasCokernel f

Tactic:
hasColimit_of_iso (show _ ≅ parallelPair (L.map g.hom) 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso e.symm) (Arrow.rightFunc.mapIso e.symm))

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Arrow.leftFunc, CategoryTheory.Iso.symm, 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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
g : Arrow.{v, u} C
e : L.mapArrow.obj g ≅ Arrow.mk f
this_1 : PreservesColimit (parallelPair g.hom 0) L
this : HasColimit (parallelPair (L.map g.hom) 0)
⊢ HasCokernel f

Tactic:
exact hasColimit_of_iso (show _ ≅ parallelPair (L.map g.hom) 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso e.symm) (Arrow.rightFunc.mapIso e.symm))

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.parallelPair.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
⊢ HasEqualizers.{v', u'} D

Tactic:
have := hasKernels L P
  have {X Y : D} (f g : X ⟶ Y) : HasEqualizer f g :=
    Preadditive.hasEqualizer_of_hasKernel _ _
  hasEqualizers_of_hasLimit_parallelPair _

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.hasKernels, CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair, CategoryTheory.Preadditive.hasEqualizer_of_hasKernel
-- 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
⊢ HasCoequalizers.{v', u'} D

Tactic:
have := hasCokernels L P
  have {X Y : D} (f g : X ⟶ Y) : HasCoequalizer f g :=
    Preadditive.hasCoequalizer_of_hasCokernel _ _
  hasCoequalizers_of_hasColimit_parallelPair _

Premises used: CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel, CategoryTheory.ObjectProperty.SerreClassLocalization.hasCokernels, CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
-- 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
⊢ HasBinaryProducts.{v', u'} D

Tactic:
have := Localization.essSurj L P.isoModSerre
  have (X Y : D) : HasBinaryProduct X Y :=
    hasLimit_of_iso (show Limits.pair _ _ ≅ _ from
      mapPairIso (L.objObjPreimageIso X) (L.objObjPreimageIso Y))
  hasBinaryProducts_of_hasLimit_pair D

Premises used: CategoryTheory.Localization.essSurj, CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.ObjectProperty.isoModSerre, CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair, CategoryTheory.Limits.mapPairIso
-- 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
⊢ HasFiniteProducts.{v', u'} D

Tactic:
have := hasZeroObject L P
  have := hasBinaryProducts L P
  hasFiniteProducts_of_has_binary_and_terminal

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.hasZeroObject, CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal, CategoryTheory.ObjectProperty.SerreClassLocalization.hasBinaryProducts
-- 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 : D
f : X ⟶ Y
hf : Mono f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
rw [mono_iff L P] at hf

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.mono_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
X Y : D
f : X ⟶ Y
hf : ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
obtain : ∀ (X' Y' : C) (f' : X' ⟶ Y'), Mono f' → ∀ (e : Arrow.mk (L.map f') ≅ Arrow.mk f), Nonempty (NormalMono f)
⊢ Nonempty (NormalMono f)

Tactic:
obtain ⟨X', Y', f', _, ⟨e⟩⟩ := hf
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
⊢ PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L

Tactic:
have := preservesKernel L P hf'.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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
⊢ Nonempty (NormalMono f)

Tactic:
⟨NormalMono.ofArrowIso ?_ e⟩

Premises used: Nonempty.intro, CategoryTheory.NormalMono.ofArrowIso
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
refine : NormalMono (L.map f')
⊢ Nonempty (NormalMono f)

Tactic:
refine ⟨NormalMono.ofArrowIso ?_ e⟩
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
rw :
  Eq (α := L.obj X' ⟶ L.obj (@NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _))
    (L.map (f' ≫ NormalMono.g)) 0
⊢ Eq (α := L.obj X' ⟶ L.obj (@NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _))
    (L.map f' ≫ L.map NormalMono.g) 0

Tactic:
rw [← L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
⊢ Eq (α := L.obj X' ⟶ L.obj (@NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _))
    (L.map (f' ≫ NormalMono.g)) 0

Tactic:
simp [hf'.w]

Premises used: CategoryTheory.NormalMono.w
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
⊢ NormalMono (L.map f')

Tactic:
exact {
      Z := L.obj hf'.Z
      g := L.map hf'.g
      w := by rw [← L.map_comp]; simp [hf'.w]
      isLimit :=
        (KernelFork.isLimitMapConeEquiv _ L).1
          (isLimitOfPreserves L hf'.isLimit) }
-- 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 : D
f : X ⟶ Y
hf : Epi f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
rw [epi_iff L P] at hf

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.epi_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
X Y : D
f : X ⟶ Y
hf : ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
obtain : ∀ (X' Y' : C) (f' : X' ⟶ Y'), Epi f' → ∀ (e : Arrow.mk (L.map f') ≅ Arrow.mk f), Nonempty (NormalEpi f)
⊢ Nonempty (NormalEpi f)

Tactic:
obtain ⟨X', Y', f', _, ⟨e⟩⟩ := hf
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
⊢ PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L

Tactic:
have := preservesCokernel L P hf'.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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
⊢ Nonempty (NormalEpi f)

Tactic:
⟨NormalEpi.ofArrowIso ?_ e⟩

Premises used: Nonempty.intro, CategoryTheory.NormalEpi.ofArrowIso
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
refine : NormalEpi (L.map f')
⊢ Nonempty (NormalEpi f)

Tactic:
refine ⟨NormalEpi.ofArrowIso ?_ e⟩
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
rw :
  Eq (α := L.obj (@NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) ⟶ L.obj Y')
    (L.map (NormalEpi.g ≫ f')) 0
⊢ Eq (α := L.obj (@NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) ⟶ L.obj Y')
    (L.map NormalEpi.g ≫ L.map f') 0

Tactic:
rw [← L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
⊢ Eq (α := L.obj (@NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) ⟶ L.obj Y')
    (L.map (NormalEpi.g ≫ f')) 0

Tactic:
simp [hf'.w]

Premises used: CategoryTheory.NormalEpi.w
-- 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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
⊢ NormalEpi (L.map f')

Tactic:
exact {
      W := L.obj hf'.W
      g := L.map hf'.g
      w := by rw [← L.map_comp]; simp [hf'.w]
      isColimit :=
        (CokernelCofork.isColimitMapCoconeEquiv _ L).1
          (isColimitOfPreserves L hf'.isColimit) }
-- 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
⊢ HasFiniteProducts.{v', u'} D

Tactic:
have := hasFiniteProducts 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
this : HasFiniteProducts.{v', u'} D
⊢ HasKernels.{v', u'} D

Tactic:
have := hasKernels 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
this_1 : HasFiniteProducts.{v', u'} D
this : HasKernels.{v', u'} D
⊢ HasCokernels.{v', u'} D

Tactic:
have := hasCokernels 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
this_1 : HasFiniteProducts.{v', u'} D
this_2 : HasKernels.{v', u'} D
this : HasCokernels.{v', u'} D
⊢ IsNormalMonoCategory.{v', u'} D

Tactic:
have := isNormalMonoCategory 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
this_1 : HasFiniteProducts.{v', u'} D
this_2 : HasKernels.{v', u'} D
this_3 : HasCokernels.{v', u'} D
this : IsNormalMonoCategory.{v', u'} D
⊢ IsNormalEpiCategory.{v', u'} D

Tactic:
have := isNormalEpiCategory 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
this_1 : HasFiniteProducts.{v', u'} D
this_2 : HasKernels.{v', u'} D
this_3 : HasCokernels.{v', u'} D
this_4 : IsNormalMonoCategory.{v', u'} D
this : IsNormalEpiCategory.{v', u'} D
⊢ Abelian.{v', u'} D

Tactic:
constructor
-- 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), PreservesLimit (parallelPair f 0) L
⊢ PreservesFiniteLimits L

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

Premises used: CategoryTheory.Functor.preservesFiniteLimits_tfae, List.TFAE.out, 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
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), PreservesLimit (parallelPair f 0) L
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), PreservesLimit (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
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
preservesKernel L P f

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernel
-- 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
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
exact preservesKernel L P f

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernel