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
rw : (∃ (X_1 : C) (s : X_1 ⟶ X) (_ : P.isoModSerre s), s ≫ f = s ≫ 0) ↔ P (Abelian.image f)
⊢ L.map f = 0 ↔ P (Abelian.image f)

Tactic:
rw [← L.map_zero, MorphismProperty.map_eq_iff_precomp L P.isoModSerre]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.ObjectProperty.isoModSerre, CategoryTheory.MorphismProperty.map_eq_iff_precomp
-- 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
⊢ (∃ (X_1 : C) (s : X_1 ⟶ X) (_ : P.isoModSerre s), s ≫ f = s ≫ 0) ↔ P (Abelian.image f)

Tactic:
simp [← exists_isoModSerre_comp_eq_zero_iff P]

Premises used: CategoryTheory.ObjectProperty.exists_isoModSerre_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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst_7 : Epi f
inst_8 : Mono g
rw : P (Abelian.image (f ≫ g)) ↔ P Z
⊢ L.map f ≫ L.map g = 0 ↔ P Z

Tactic:
rw [← L.map_comp, map_eq_zero_iff L P]

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff, 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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst_7 : Epi f
inst_8 : Mono g
⊢ StrongEpi f

Tactic:
have := strongEpi_of_epi 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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst_7 : Epi f
inst_8 : Mono g
this : StrongEpi f
⊢ P (Abelian.image (f ≫ g)) ↔ P Z

Tactic:
P.prop_iff_of_iso (Abelian.imageIsoImage _ ≪≫ (image.isoStrongEpiMono f g rfl).symm)

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Limits.image.isoStrongEpiMono, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Abelian.imageIsoImage, 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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst_7 : Epi f
inst_8 : Mono g
this : StrongEpi f
⊢ P (Abelian.image (f ≫ g)) ↔ P Z

Tactic:
exact P.prop_iff_of_iso (Abelian.imageIsoImage _ ≪≫ (image.isoStrongEpiMono f g rfl).symm)

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Limits.image.isoStrongEpiMono, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Abelian.imageIsoImage, 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
⊢ 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 : L.EssSurj
⊢ Mono (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.monoModSerre 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 : Mono (L.map f)), P.monoModSerre 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 : Mono (L.map f)
rw : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) (0 ≫ L.map f)
rw₁ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) 0
rw₂ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f ≫ f)) 0
rw₃ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map 0) 0
rw₄ rw₅ : Eq.{v' + 1} (α := L.obj (kernel f) ⟶ L.obj Y) 0 0
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0

Tactic:
rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.condition, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, 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
h : Mono (L.map f)
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0

Tactic:
have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.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 : Mono (L.map f)
hf : Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
⊢ P.monoModSerre f

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

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.SerreClassLocalization.map_comp_eq_zero_iff_of_epi_mono, CategoryTheory.Limits.kernel.ι
-- 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 : Mono (L.map f)), P.monoModSerre f

Tactic:
tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
    simpa [hf] using map_comp_eq_zero_iff_of_epi_mono L P (𝟙 _) (kernel.ι 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 : Mono (L.map f)), P.monoModSerre f
⊢ P.monoModSerre 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 : Mono (L.map f)), P.monoModSerre f
⊢ ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 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 : Mono (L.map f)), P.monoModSerre f
⊢ ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 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 : Mono (L.map f)), P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : L.map z ≫ L.map f = 0
⊢ L.map (z ≫ f) = 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 : Mono (L.map f)), P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : L.map (z ≫ f) = 0
rw :
  ∀ (hz : ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), (z ≫ f) ≫ s = 0),
    ∃ (Y' : C) (s : X ⟶ Y') (_ : P.monoModSerre s), z ≫ s = 0
⊢ L.map z = 0

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

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

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

Tactic:
exact ⟨W, f ≫ s, MorphismProperty.comp_mem _ _ _ hf hs, by simpa using eq⟩
-- 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
⊢ ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 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_comp_monoModSerre_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    exact ⟨W, f ≫ s, MorphismProperty.comp_mem _ _ _ hf hs, by simpa using eq⟩
-- 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
⊢ ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 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 : 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
⊢ Mono (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 : 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:
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 : 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
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
rw : ∀ (P : D) (g : P ⟶ L.obj X), g ≫ L.map f = 0 → g = 0
⊢ Mono (L.map f)

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

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

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

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 : 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
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
rw : L.map (φ.f (W := P.isoModSerre)) = 0
⊢ z = 0

Tactic:
rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, 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 : 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
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
apply : L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
⊢ L.map (φ.f (W := P.isoModSerre)) = 0

Tactic:
apply hf φ.f

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

Tactic:
have : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f := by cat_disch
-- 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 : 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
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z ≫ 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 [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero