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 : C
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this_2 : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : t ≫ z ≫ f = 0
this : IsIso (L.map t)
fac₁ : (t ≫ z) ≫ f = 0
⊢ IsIso (L.map t)

Tactic:
rw [← Category.assoc] at fac

Premises used: CategoryTheory.Category.assoc
-- 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_1 : L.PreservesMonomorphisms
this_2 : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : (t ≫ z) ≫ f = 0
this : IsIso (L.map t)
⊢ CategoryStruct.comp (Y := L.obj (kernel f)) (inv (L.map t) ≫ L.map (kernel.lift f (t ≫ z) fac)) (L.map (kernel.ι f)) =
    eqToHom ⋯ ≫ L.map z

Tactic:
simp [← Functor.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 : C
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this_2 : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : (t ≫ z) ≫ f = 0
this : IsIso (L.map t)
⊢ ∃ (l : L.obj Z ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z

Tactic:
exact ⟨inv (L.map t) ≫ L.map (kernel.lift _ _ fac), by simp [← 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 : C
f : X ⟶ Y
⊢ L.PreservesEpimorphisms

Tactic:
have := preservesEpimorphisms 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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L P.isoModSerre
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
this : ∀ (W : D) (z : L.obj Y ⟶ W) (hz : L.map f ≫ z = 0), ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = z
s : Cofork (L.map f) 0
x x_1 :
  Cocone.pt (F := parallelPair (L.map f) 0) (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) L) ⟶
    s.pt
h₁ : Cofork.π (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) L) ≫ x = s.π
h₂ : Cofork.π (CokernelCofork.map (Cofork.ofπ (P := cokernel f) (cokernel.π f) ⋯) L) ≫ x_1 = s.π
⊢ x = x_1

Tactic:
simpa [cancel_epi] using h₁.trans h₂.symm

Premises used: Eq.symm, CategoryTheory.cancel_epi, Eq.trans
-- 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_1 : L.PreservesEpimorphisms
this : L.EssSurj
suffices :
  ∀ (W : D) (z : L.obj Y ⟶ W) (hz : L.map f ≫ z = 0), ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = z
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
suffices ∀ (W : D) (z : L.obj Y ⟶ W) (hz : L.map f ≫ z = 0),
      ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = z from
    preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
      ((CokernelCofork.isColimitMapCoconeEquiv _ L).2
        (Cofork.IsColimit.ofExistsUnique
          (fun s ↦ existsUnique_of_exists_of_unique
            (this _ _ (CokernelCofork.condition s))
            (fun _ _ h₁ h₂ ↦ by simpa [cancel_epi] using h₁.trans h₂.symm))))
-- 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_1 : L.PreservesEpimorphisms
this : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
inr :
  ∀
    (this :
      ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
        (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
        ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w)
    (hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
wlog :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
⊢ ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w

Tactic:
wlog hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
      generalizing 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 : C
f : X ⟶ Y
this_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
inr :
  ∀ (φ : P.isoModSerre.LeftFraction Y (L.objPreimage W))
    (hφ : w ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
⊢ ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (w ≫ (L.objObjPreimageIso W).inv)

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Localization.exists_leftFraction, CategoryTheory.CategoryStruct.comp, CategoryTheory.ObjectProperty.isoModSerre, CategoryTheory.Iso.inv
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
⊢ w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = L.map (φ.f (W := P.isoModSerre))

Tactic:
rw [← cancel_mono (L.map φ.s), Category.assoc,
      MorphismProperty.LeftFraction.map_comp_map_s] at hφ

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = L.map (φ.f (W := P.isoModSerre))
rw : L.map f ≫ w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = 0
rw₁ :
  Eq (α := L.obj X ⟶ L.obj (φ.Y' (W := P.isoModSerre)))
    (0 ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))) 0
rw₂ rw₃ : Eq.{v' + 1} (α := L.obj X ⟶ L.obj (φ.Y' (W := P.isoModSerre))) 0 0
⊢ L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 0

Tactic:
rw [← hφ, reassoc_of% hw, zero_comp]

Premises used: CategoryTheory.Limits.zero_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 : C
f : X ⟶ Y
this_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = L.map (φ.f (W := P.isoModSerre))
⊢ ∃ (z : Y ⟶ φ.Y' (W := P.isoModSerre)), L.map (φ.f (W := P.isoModSerre)) = L.map z ≫ eqToHom ⋯

Tactic:
simp
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = L.map (φ.f (W := P.isoModSerre))
inr :
  ∀ (l : L.obj (cokernel f) ⟶ L.obj (φ.Y' (W := P.isoModSerre)))
    (hl : L.map (cokernel.π f) ≫ l = L.map (φ.f (W := P.isoModSerre))),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
⊢ ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w

Tactic:
obtain ⟨l, hl⟩ := this _ (L.map φ.f) (by rw [← hφ, reassoc_of% hw, zero_comp]) ⟨_, rfl, by simp⟩

Premises used: CategoryTheory.Functor.map, Exists.intro, CategoryTheory.MorphismProperty.LeftFraction.f, rfl
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = L.map (φ.f (W := P.isoModSerre))
l : L.obj (cokernel f) ⟶ L.obj (φ.Y' (W := P.isoModSerre))
hl : L.map (cokernel.π f) ≫ l = L.map (φ.f (W := P.isoModSerre))
⊢ L.map (cokernel.π f) ≫ l ≫ inv (L.map (φ.s (W := P.isoModSerre))) ≫ Iso.hom (L.objObjPreimageIso W) = w

Tactic:
simp [reassoc_of% hl, ← hφ]
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W) (hw : L.map f ≫ w = 0)
    (hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ),
    ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = L.map (φ.f (W := P.isoModSerre))
l : L.obj (cokernel f) ⟶ L.obj (φ.Y' (W := P.isoModSerre))
hl : L.map (cokernel.π f) ≫ l = L.map (φ.f (W := P.isoModSerre))
⊢ ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w

Tactic:
exact ⟨l ≫ inv (L.map φ.s) ≫ (L.objObjPreimageIso W).hom, by simp [reassoc_of% hl, ← hφ]⟩
-- 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_1 : L.PreservesEpimorphisms
this : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
obtain :
  ∀ (Z : C) (z : Y ⟶ Z) (hw : L.map f ≫ L.map z ≫ eqToHom ⋯ = 0),
    ∃ (l : L.obj (cokernel f) ⟶ L.obj Z), L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯
⊢ ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = w

Tactic:
obtain ⟨Z, rfl, z, rfl⟩ := hw'

Premises used: rfl
-- 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_1 : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
hw : L.map f ≫ L.map z ≫ eqToHom ⋯ = 0
⊢ ∃ (Y' : C) (s : Z ⟶ Y') (_ : P.isoModSerre s), (f ≫ z) ≫ s = 0

Tactic:
simp only [eqToHom_refl, Category.comp_id, ← L.map_comp,
    map_eq_zero_iff L P, ← exists_comp_isoModSerre_eq_zero_iff P] at hw

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff, CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, 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 : C
f : X ⟶ Y
this_1 : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
hw : ∃ (Y' : C) (s : Z ⟶ Y') (_ : P.isoModSerre s), (f ≫ z) ≫ s = 0
obtain :
  ∀ (Z' : C) (t : Z ⟶ Z') (ht : P.isoModSerre t) (fac : (f ≫ z) ≫ t = 0),
    ∃ (l : L.obj (cokernel f) ⟶ L.obj Z), L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯
⊢ ∃ (l : L.obj (cokernel f) ⟶ L.obj Z), L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯

Tactic:
obtain ⟨Z', t, ht, fac⟩ := hw
-- 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_1 : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : (f ≫ z) ≫ t = 0
⊢ f ≫ z ≫ t = 0

Tactic:
rw [Category.assoc] at fac

Premises used: CategoryTheory.Category.assoc
-- 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_1 : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
⊢ IsIso (L.map t)

Tactic:
have := Localization.inverts L P.isoModSerre t ht
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
this : IsIso (L.map t)
⊢ CategoryStruct.comp (Y := L.obj (cokernel f)) (L.map (cokernel.π f))
      (L.map (cokernel.desc f (z ≫ t) fac) ≫ inv (L.map t)) =
    L.map z ≫ eqToHom ⋯

Tactic:
simp [← L.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- 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_1 : L.PreservesEpimorphisms
this_2 : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
this : IsIso (L.map t)
⊢ ∃ (l : L.obj (cokernel f) ⟶ L.obj Z), L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯

Tactic:
exact ⟨L.map (cokernel.desc _ _ fac) ≫ inv (L.map t), by simp [← L.map_comp_assoc]⟩
-- 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
obtain : ∀ (g : Arrow.{v, u} C) (e : L.mapArrow.obj g ≅ Arrow.mk f), HasKernel f
⊢ HasKernel f

Tactic:
obtain ⟨g, ⟨e⟩⟩ :=
      (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
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
⊢ PreservesLimit (parallelPair g.hom 0) L

Tactic:
have := preservesKernel 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 : PreservesLimit (parallelPair g.hom 0) L
⊢ HasLimit (parallelPair (L.map g.hom) 0)

Tactic:
have : HasLimit (parallelPair (L.map g.hom) 0) :=
      ⟨_, (KernelFork.isLimitMapConeEquiv _ L).1
        (isLimitOfPreserves L (kernelIsKernel 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 : PreservesLimit (parallelPair g.hom 0) L
this : HasLimit (parallelPair (L.map g.hom) 0)
⊢ HasKernel f

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

Premises used: CategoryTheory.Limits.hasLimit_of_iso, 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
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 : PreservesLimit (parallelPair g.hom 0) L
this : HasLimit (parallelPair (L.map g.hom) 0)
⊢ HasKernel f

Tactic:
exact hasLimit_of_iso (show parallelPair (L.map g.hom) 0 ≅ _ from
      parallelPair.ext (Arrow.leftFunc.mapIso e) (Arrow.rightFunc.mapIso 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
obtain : ∀ (g : Arrow.{v, u} C) (e : L.mapArrow.obj g ≅ Arrow.mk f), HasCokernel f
⊢ HasCokernel f

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

Premises used: CategoryTheory.Functor.EssSurj.mem_essImage, CategoryTheory.Arrow.mk