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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
tfae_3_to_1 : ∀ (a : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0), Epi (L.map f)
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE

Tactic:
tfae_finish
-- 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
⊢ Epi (L.map f) ↔ P.epiModSerre f

Tactic:
(epi_map_tfae L P f).out 0 1

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.inverseImage (MorphismProperty.monomorphisms D) L f ↔ P.monoModSerre f
⊢ MorphismProperty.inverseImage (MorphismProperty.monomorphisms D) L = P.monoModSerre

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.monomorphisms D) L f ↔ P.monoModSerre f

Tactic:
simp [mono_map_iff L P]

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.mono_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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.inverseImage (MorphismProperty.epimorphisms D) L f ↔ P.epiModSerre f
⊢ MorphismProperty.inverseImage (MorphismProperty.epimorphisms D) L = P.epiModSerre

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.epimorphisms D) L f ↔ P.epiModSerre f

Tactic:
simp [epi_map_iff L P]

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 Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono (L.map f)

Tactic:
simpa only [mono_map_iff _ P] using P.monoModSerre_of_mono f

Premises used: CategoryTheory.ObjectProperty.monoModSerre_of_mono, CategoryTheory.ObjectProperty.SerreClassLocalization.mono_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 Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi (L.map f)

Tactic:
simpa only [epi_map_iff _ P] using P.epiModSerre_of_epi f

Premises used: CategoryTheory.ObjectProperty.epiModSerre_of_epi, 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 Y : D
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 : D
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ L.mapArrow.EssSurj

Tactic:
have := Localization.essSurj_mapArrow 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 : D
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

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

Premises used: Iff.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 Y : D
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
refine_1 :
  Mono f → ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
refine_2 :
  (∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f
⊢ Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
refine ⟨fun _ ↦ ?_, ?_⟩
-- 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.PreservesMonomorphisms
this_2 : L.mapArrow.EssSurj
h : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) →
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
obtain :
  ∀ (X' Y' : C) (f' : X' ⟶ Y'),
    Mono f' →
      ∀ (e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)),
        ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.monomorphisms, CategoryTheory.MorphismProperty.monomorphisms.infer_property, CategoryTheory.MorphismProperty.arrow_iso_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
this_1 : L.PreservesMonomorphisms
this_2 : L.mapArrow.EssSurj
h : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) →
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩

Premises used: inferInstance, Nonempty.intro, CategoryTheory.Iso.trans, 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 Y : D
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this_2 : L.mapArrow.EssSurj
h : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) →
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

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

Tactic:
suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Mono (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono 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.monomorphisms 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.PreservesMonomorphisms
this : L.mapArrow.EssSurj
h : Mono f_1
X Y : C
f : X ⟶ Y
hf : Mono (L.map f)
⊢ P.monoModSerre f

Tactic:
rw [mono_map_iff L P] at hf

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.mono_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.PreservesMonomorphisms
this : L.mapArrow.EssSurj
h : Mono f_1
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
⟨_, _, Abelian.image.ι f, inferInstance, ⟨Iso.symm ?_⟩⟩

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

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

Tactic:
have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_factorThruImage
-- 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.PreservesMonomorphisms
this_2 : L.mapArrow.EssSurj
h : Mono f_1
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
this : IsIso (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f))
⊢ Iso.hom (asIso (L.map (Abelian.factorThruImage f))) ≫
      (Arrow.mk (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))).hom =
    (Arrow.mk (L.map f)).hom ≫ Iso.hom (Iso.refl (Arrow.mk (L.map f)).right)

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.PreservesMonomorphisms
this_2 : L.mapArrow.EssSurj
h : Mono f_1
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
this : IsIso (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f))
⊢ Arrow.mk (L.map f) ≅ Arrow.mk (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))

Tactic:
exact Arrow.isoMk (asIso (L.map (Abelian.factorThruImage f))) (Iso.refl _)
      (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.PreservesMonomorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ MorphismProperty.monomorphisms D (L.map f')

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

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

Premises used: CategoryTheory.MorphismProperty.monomorphisms, 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 : D
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 : D
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ L.mapArrow.EssSurj

Tactic:
have := Localization.essSurj_mapArrow 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 : D
f : X ⟶ Y
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ Epi f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

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

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

Tactic:
refine ⟨fun _ ↦ ?_, ?_⟩
-- 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_2 : L.mapArrow.EssSurj
h : Epi f
this :
  ∀ ⦃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))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
obtain :
  ∀ (X' Y' : C) (f' : X' ⟶ Y'),
    Epi f' →
      ∀ (e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)),
        ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.epimorphisms D).arrow_iso_iff e).2 (.infer_property f))

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.epimorphisms.infer_property, CategoryTheory.MorphismProperty.arrow_iso_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
this_1 : L.PreservesEpimorphisms
this_2 : L.mapArrow.EssSurj
h : Epi f
this :
  ∀ ⦃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))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩

Premises used: inferInstance, Nonempty.intro, CategoryTheory.Iso.trans, 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 Y : D
f : X ⟶ Y
this_1 : L.PreservesEpimorphisms
this_2 : L.mapArrow.EssSurj
h : Epi f
this :
  ∀ ⦃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))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩