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 : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
⊢ ∀ (a : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0), Mono (L.map f)

Tactic:
tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.mono_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ z)
    rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]
    apply hf φ.f
    have : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f := by cat_disch
    rw [← this, Category.assoc, Category.assoc, hz, comp_zero, 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
tfae_3_to_1 : ∀ (a : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0), Mono (L.map f)
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 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
⊢ Mono (L.map f) ↔ P.monoModSerre f

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

Premises used: List.TFAE.out, OfNat.ofNat, CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_tfae
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
⊢ Epi (L.map f)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ P.epiModSerre f

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (a : Epi (L.map f)), P.epiModSerre f

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
h : Epi (L.map f)
rw : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) (L.map f ≫ 0)
rw₁ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) 0
rw₂ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map (f ≫ cokernel.π f)) 0
rw₃ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map 0) 0
rw₄ rw₅ : Eq.{v' + 1} (α := L.obj X ⟶ L.obj (cokernel f)) 0 0
⊢ Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0

Tactic:
rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi
-- 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
h : Epi (L.map f)
⊢ Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0

Tactic:
have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_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 : L.EssSurj
h : Epi (L.map f)
hf : Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0
⊢ P.epiModSerre f

Tactic:
simpa [hf] using map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π f) (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.SerreClassLocalization.map_comp_eq_zero_iff_of_epi_mono, CategoryTheory.Limits.cokernel.π
-- 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
⊢ ∀ (a : Epi (L.map f)), P.epiModSerre f

Tactic:
tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]
    simpa [hf] using map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π 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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Epi (L.map f)), P.epiModSerre f
⊢ P.epiModSerre f

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : L.map f ≫ L.map z = 0
⊢ L.map (f ≫ z) = 0

Tactic:
rw [← L.map_comp] at hz

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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Epi (L.map f)), P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : L.map (f ≫ z) = 0
rw :
  ∀ (hz : ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f ≫ z = 0),
    ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 0
⊢ L.map z = 0

Tactic:
rw [map_eq_zero_iff L P, ← exists_epiModSerre_comp_eq_zero_iff P] at hz ⊢

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff, CategoryTheory.ObjectProperty.exists_epiModSerre_comp_eq_zero_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
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Epi (L.map f)), P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f ≫ z = 0
obtain :
  ∀ (W : C) (s : W ⟶ X) (hs : P.epiModSerre s) (eq : s ≫ f ≫ z = 0),
    ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 0
⊢ ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 0

Tactic:
obtain ⟨W, s, hs, eq⟩ := hz
-- 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
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
W : C
s : W ⟶ X
hs : P.epiModSerre s
eq : s ≫ f ≫ z = 0
⊢ (s ≫ f) ≫ z = 0

Tactic:
simpa
-- 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
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
W : C
s : W ⟶ X
hs : P.epiModSerre s
eq : s ≫ f ≫ z = 0
⊢ ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 0

Tactic:
refine ⟨_, s ≫ f, MorphismProperty.comp_mem _ _ _ hs hf, by simpa⟩
-- 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
⊢ ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0

Tactic:
tfae_have 2 → 3 := fun hf ↦ by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_epiModSerre_comp_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    refine ⟨_, s ≫ f, MorphismProperty.comp_mem _ _ _ hs hf, by simpa⟩
-- 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
⊢ ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ Epi (L.map f)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (a : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0), Epi (L.map f)

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
rw : ∀ (R : D) (g : L.obj Y ⟶ R), L.map f ≫ g = 0 → g = 0
⊢ Epi (L.map f)

Tactic:
rw [Preadditive.epi_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.epi_iff_cancel_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 : 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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
obtain :
  ∀ (φ : P.isoModSerre.LeftFraction Y (L.objPreimage W))
    (hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯), z = 0
⊢ z = 0

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (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 : 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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
rw : L.map (φ.f (W := P.isoModSerre)) = 0
⊢ z = 0

Tactic:
rw [← cancel_mono (L.objObjPreimageIso W).inv, zero_comp, hφ,
      ← cancel_mono (L.map φ.s), zero_comp,
      MorphismProperty.LeftFraction.map_comp_map_s]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.Limits.zero_comp, 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 : 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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
apply : L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 0
⊢ L.map (φ.f (W := P.isoModSerre)) = 0

Tactic:
apply hf φ.f

Premises used: CategoryTheory.MorphismProperty.LeftFraction.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 : 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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))

Tactic:
simp [reassoc_of% 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 : 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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))

Tactic:
have : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s := by
      simp [reassoc_of% 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.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
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))
rw : L.map f ≫ z ≫ 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 [this, reassoc_of% hz, 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 : 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
⊢ ∀ (a : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0), Epi (L.map f)

Tactic:
tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.epi_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (L.objObjPreimageIso W).inv)
    rw [← cancel_mono (L.objObjPreimageIso W).inv, zero_comp, hφ,
      ← cancel_mono (L.map φ.s), zero_comp,
      MorphismProperty.LeftFraction.map_comp_map_s]
    apply hf φ.f
    have : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s := by
      simp [reassoc_of% hφ]
    rw [this, reassoc_of% hz, zero_comp]