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
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f
refine_1 :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) →
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Epi (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Epi f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.epimorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ 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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : Epi (L.map f)
⊢ P.epiModSerre f

Tactic:
rw [epi_map_iff L P] at hf

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.epi_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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
⟨_, _, Abelian.factorThruImage f, inferInstance, ⟨?_⟩⟩

Premises used: CategoryTheory.Abelian.factorThruImage, inferInstance, Nonempty.intro, Exists.intro
-- 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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
refine_1 : Arrow.mk (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f)) ≅ Arrow.mk (L.map f)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
refine ⟨_, _, Abelian.factorThruImage f, inferInstance, ⟨?_⟩⟩
-- 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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ IsIso (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))

Tactic:
have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_image_ι
-- 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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this_2 : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
this : IsIso (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))
⊢ Iso.hom (Iso.refl (Arrow.mk (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f))).left) ≫
      (Arrow.mk (L.map f)).hom =
    (Arrow.mk (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f))).hom ≫
      Iso.hom (asIso (L.map (Abelian.image.ι f)))

Tactic:
simp [← 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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this_2 : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
this : IsIso (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))
⊢ Arrow.mk (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f)) ≅ Arrow.mk (L.map f)

Tactic:
refine Arrow.isoMk (Iso.refl _) (asIso (L.map (Abelian.image.ι f))) (by simp [← L.map_comp])

Premises used: CategoryTheory.Iso.refl, CategoryTheory.asIso, CategoryTheory.Arrow.isoMk
-- 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
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ MorphismProperty.epimorphisms D (L.map f')

Tactic:
simpa using inferInstanceAs (Epi (L.map f'))
-- 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
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ Epi f

Tactic:
exact ((MorphismProperty.epimorphisms D).arrow_mk_iso_iff e).1
      (by simpa using inferInstanceAs (Epi (L.map f')))

Premises used: CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- 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.PreservesMonomorphisms

Tactic:
have := preservesMonomorphisms 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.PreservesMonomorphisms
⊢ 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.PreservesMonomorphisms
this_2 : L.EssSurj
this : ∀ (W : D) (z : W ⟶ L.obj X) (hz : z ≫ L.map f = 0), ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = z
s : Fork (L.map f) 0
x x_1 : s.pt ⟶ Cone.pt (F := parallelPair (L.map f) 0) (KernelFork.map (Fork.ofι (P := kernel f) (kernel.ι f) ⋯) L)
h₁ : x ≫ Fork.ι (KernelFork.map (Fork.ofι (P := kernel f) (kernel.ι f) ⋯) L) = s.ι
h₂ : x_1 ≫ Fork.ι (KernelFork.map (Fork.ofι (P := kernel f) (kernel.ι f) ⋯) L) = s.ι
⊢ x = x_1

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

Premises used: CategoryTheory.cancel_mono, Eq.symm, 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.PreservesMonomorphisms
this : L.EssSurj
suffices : ∀ (W : D) (z : W ⟶ L.obj X) (hz : z ≫ L.map f = 0), ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = z
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
suffices ∀ (W : D) (z : W ⟶ L.obj X) (hz : z ≫ L.map f = 0),
      ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = z from
    preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
      ((KernelFork.isLimitMapConeEquiv _ L).2
        (Fork.IsLimit.ofExistsUnique
          (fun s ↦ existsUnique_of_exists_of_unique
            (this _ _ (KernelFork.condition s))
            (fun _ _ h₁ h₂ ↦ by simpa [cancel_mono] 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.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
inr :
  ∀
    (this :
      ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
        (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
        ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w)
    (hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
wlog :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w

Tactic:
wlog hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
      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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
inr :
  ∀ (φ : P.isoModSerre.RightFraction (L.objPreimage W) X)
    (hφ : Iso.hom (L.objObjPreimageIso W) ≫ w = φ.map (W := P.isoModSerre) L ⋯),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w

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

Premises used: CategoryTheory.Localization.exists_rightFraction, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.ObjectProperty.isoModSerre, CategoryTheory.Iso.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 : C
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ w = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))

Tactic:
rw [← cancel_epi (L.map φ.s),
      MorphismProperty.RightFraction.map_s_comp_map] at hφ

Premises used: CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map, CategoryTheory.Functor.map, CategoryTheory.cancel_epi, CategoryTheory.MorphismProperty.RightFraction.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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w ≫ L.map f = 0
rw₃ :
  Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y)
    (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ 0) 0
rw₄ : Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y) (L.map (φ.s (W := P.isoModSerre)) ≫ 0) 0
rw₅ rw₆ : Eq.{v' + 1} (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y) 0 0
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0

Tactic:
rw [← hφ, Category.assoc, Category.assoc, hw, comp_zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero
-- 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
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
⊢ ∃ (z : φ.X' (W := P.isoModSerre) ⟶ X), L.map (φ.f (W := P.isoModSerre)) = eqToHom ⋯ ≫ L.map z

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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
inr :
  ∀ (l : L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj (kernel f))
    (hl : l ≫ L.map (kernel.ι f) = L.map (φ.f (W := P.isoModSerre))),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w

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

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

Tactic:
simp [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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
l : L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj (kernel f)
hl : l ≫ L.map (kernel.ι f) = L.map (φ.f (W := P.isoModSerre))
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w

Tactic:
exact ⟨(L.objObjPreimageIso W).inv ≫ inv (L.map φ.s) ≫ l, by simp [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.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
obtain :
  ∀ (Z : C) (z : Z ⟶ X) (hw : (eqToHom ⋯ ≫ L.map z) ≫ L.map f = 0),
    ∃ (l : L.obj Z ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = 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.PreservesMonomorphisms
this : L.EssSurj
Z : C
z : Z ⟶ X
hw : (eqToHom ⋯ ≫ L.map z) ≫ L.map f = 0
⊢ ∃ (X' : C) (s : X' ⟶ Z) (_ : P.isoModSerre s), s ≫ z ≫ f = 0

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

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff, CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff, CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_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 : L.EssSurj
Z : C
z : Z ⟶ X
hw : ∃ (X' : C) (s : X' ⟶ Z) (_ : P.isoModSerre s), s ≫ z ≫ f = 0
obtain :
  ∀ (Z' : C) (t : Z' ⟶ Z) (ht : P.isoModSerre t) (fac : t ≫ z ≫ f = 0),
    ∃ (l : L.obj Z ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z
⊢ ∃ (l : L.obj Z ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z

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

Tactic:
rw [← Category.assoc] at fac

Premises used: CategoryTheory.Category.assoc