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
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0

Tactic:
exact ⟨_, kernel.ι f, P.prop_of_iso (Abelian.coimageIsoImage f).symm hf, by simp⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)

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

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
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) → P (Abelian.image f)
refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)

Tactic:
refine ⟨?_, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
refine_1 : ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0
⊢ P (Abelian.image f)

Tactic:
rw [← exists_epiModSerre_comp_eq_zero_iff P]

Premises used: 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
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
⊢ ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0

Tactic:
⟨Y', s, hs.2, eq⟩

Premises used: And.right, Exists.intro
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
⊢ ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0

Tactic:
exact ⟨Y', s, hs.2, eq⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
refine_2 : P.isoModSerre (X := kernel f) (kernel.ι f)
⊢ ∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0

Tactic:
refine ⟨_, kernel.ι f, ?_, by simp⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ P.isoModSerre (X := kernel f) (kernel.ι f)

Tactic:
simpa only [isoModSerre_iff_of_mono] using
      P.prop_of_iso (Abelian.coimageIsoImage f).symm hf

Premises used: CategoryTheory.Abelian.coimageIsoImage, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)

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

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
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) → P (Abelian.image f)
refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)

Tactic:
refine ⟨?_, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
refine_1 : P (Abelian.coimage f)
⊢ P (Abelian.image f)

Tactic:
apply P.prop_of_iso (Abelian.coimageIsoImage f)

Premises used: CategoryTheory.Abelian.coimageIsoImage, CategoryTheory.ObjectProperty.prop_of_iso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
refine_1 : ∀ (this : P.monoModSerre (X := Abelian.coimage f) (Abelian.factorThruCoimage f ≫ s)), P (Abelian.coimage f)
⊢ P (Abelian.coimage f)

Tactic:
have := P.monoModSerre.comp_mem (Abelian.factorThruCoimage f) s
      (monoModSerre_of_mono _ _) hs
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
this : P.monoModSerre (X := Abelian.coimage f) (Abelian.factorThruCoimage f ≫ s)
refine_1 : ∀ (this : P.monoModSerre (X := Abelian.coimage f) (Y := Y') 0), P (Abelian.coimage f)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (this : P (Abelian.coimage f)), P (Abelian.coimage f)
⊢ P (Abelian.coimage f)

Tactic:
rwa [show Abelian.factorThruCoimage f ≫ s = 0 by cat_disch,
      monoModSerre_zero_iff] at this

Premises used: CategoryTheory.ObjectProperty.monoModSerre_zero_iff
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
exact ⟨_, cokernel.π f, hf, by simp⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)

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

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
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) → P (Abelian.image f)
refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)

Tactic:
refine ⟨?_, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
refine_1 : ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0
⊢ P (Abelian.image f)

Tactic:
rw [← exists_comp_monoModSerre_eq_zero_iff P]

Premises used: 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
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
⟨Y', s, hs.1, eq⟩

Premises used: And.left, Exists.intro
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
exact ⟨Y', s, hs.1, eq⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
rwa rwa₁ rwa₂ rwa₃ : P.monoModSerre (Y := cokernel f) (cokernel.π f)
⊢ P.isoModSerre (Y := cokernel f) (cokernel.π f)

Tactic:
rwa [isoModSerre_iff_of_epi]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0

Tactic:
refine ⟨_, cokernel.π f, by rwa [isoModSerre_iff_of_epi], by simp⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
rw : P.monoModSerre (Y := Abelian.image f) (Abelian.factorThruImage f)
⊢ P.isoModSerre (Y := Abelian.image f) (Abelian.factorThruImage f)

Tactic:
rw [isoModSerre_iff_of_epi]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f) = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ P.monoModSerre (Y := Abelian.image f) (Abelian.factorThruImage f)

Tactic:
exact P.prop_of_iso
    (asIso (kernel.map _ f (𝟙 _) (Abelian.image.ι f) (by simp))).symm hf

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.image.ι, CategoryTheory.Iso.symm, CategoryTheory.Limits.kernel.map, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
rw : P.epiModSerre (X := Abelian.image f) (Abelian.image.ι f)
⊢ P.isoModSerre (X := Abelian.image f) (Abelian.image.ι f)

Tactic:
rw [isoModSerre_iff_of_mono]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
dsimp : P (cokernel (X := Abelian.image f) (kernel.ι (cokernel.π f)))
⊢ P.epiModSerre (X := Abelian.image f) (Abelian.image.ι f)

Tactic:
dsimp [epiModSerre] at hf ⊢

Premises used: CategoryTheory.ObjectProperty.epiModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (cokernel f)
⊢ f ≫ 𝟙 Y = CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (kernel.ι (cokernel.π f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (cokernel f)
⊢ P (cokernel (X := Abelian.image f) (kernel.ι (cokernel.π f)))

Tactic:
exact P.prop_of_iso
    (asIso (cokernel.map f _ (Abelian.factorThruImage f) (𝟙 Y) (by simp))) hf

Premises used: CategoryTheory.Limits.cokernel.map, CategoryTheory.Abelian.factorThruImage, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.CategoryStruct.id, CategoryTheory.asIso
-- 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.isoModSerre t), f₁ ≫ t = f₂ ≫ t

Tactic:
⟨_, cokernel.π (f₁ - f₂), ?_, ?_⟩

Premises used: HSub.hSub, Exists.intro, 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
refine_1 : P.isoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))
refine_2 : Eq (α := X ⟶ cokernel (f₁ - f₂)) (f₁ ≫ cokernel.π (f₁ - f₂)) (f₂ ≫ cokernel.π (f₁ - f₂))
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.isoModSerre t), f₁ ≫ t = f₂ ≫ t

Tactic:
refine ⟨_, cokernel.π (f₁ - 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
refine_1 : P.monoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))
⊢ P.isoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))

Tactic:
rw [isoModSerre_iff_of_epi]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ s ≫ (f₁ - f₂) = 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.monoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))

Tactic:
exact (exists_isoModSerre_comp_eq_zero_iff P _).1 ⟨_, s, hs, by simpa [sub_eq_zero]⟩

Premises used: CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff, Exists.intro, 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ Eq (α := X ⟶ cokernel (f₁ - f₂)) (f₁ ≫ cokernel.π (f₁ - f₂)) (f₂ ≫ cokernel.π (f₁ - f₂))

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using cokernel.condition (f₁ - f₂)

Premises used: sub_eq_zero, HSub.hSub, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Preadditive.sub_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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : P.isoModSerre t), t ≫ f₁ = t ≫ f₂

Tactic:
⟨_, kernel.ι (f₁ - f₂), ?_, ?_⟩

Premises used: HSub.hSub, Exists.intro, 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
refine_1 : P.isoModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))
refine_2 : Eq (α := kernel (f₁ - f₂) ⟶ Y) (kernel.ι (f₁ - f₂) ≫ f₁) (kernel.ι (f₁ - f₂) ≫ f₂)
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : P.isoModSerre t), t ≫ f₁ = t ≫ f₂

Tactic:
refine ⟨_, kernel.ι (f₁ - 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
refine_1 : P.epiModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))
⊢ P.isoModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))

Tactic:
rw [isoModSerre_iff_of_mono]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono
-- 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ (f₁ - f₂) ≫ s = 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.epiModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))

Tactic:
exact P.prop_of_iso (Abelian.coimageIsoImage (f₁ - f₂)).symm
        ((exists_comp_isoModSerre_eq_zero_iff P _).1 ⟨_ ,s, hs, by simpa [sub_eq_zero]⟩)

Premises used: CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff, HSub.hSub, CategoryTheory.Abelian.coimageIsoImage, CategoryTheory.ObjectProperty.prop_of_iso, Exists.intro, CategoryTheory.Iso.symm, 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ Eq (α := kernel (f₁ - f₂) ⟶ Y) (kernel.ι (f₁ - f₂) ≫ f₁) (kernel.ι (f₁ - f₂) ≫ f₂)

Tactic:
simpa only [Preadditive.comp_sub, sub_eq_zero] using kernel.condition (f₁ - f₂)

Premises used: sub_eq_zero, HSub.hSub, CategoryTheory.Limits.kernel.condition, CategoryTheory.Preadditive.comp_sub
-- 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
⊢ P.isoModSerre.Q.Additive

Tactic:
inferInstance

Premises used: 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 : C
simp : (∃ (X_1 : C), P.isoModSerre (X := X_1) (Y := X) 0) ↔ P X
⊢ IsZero.{v', u'} (L.obj X) ↔ P X

Tactic:
simp only [IsZero.iff_id_eq_zero, ← L.map_id, ← L.map_zero,
    MorphismProperty.map_eq_iff_precomp L P.isoModSerre,
    Category.comp_id, comp_zero, exists_prop, exists_eq_right]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, exists_eq_right, CategoryTheory.Category.comp_id, exists_prop, CategoryTheory.Functor.map_id, CategoryTheory.ObjectProperty.isoModSerre, CategoryTheory.Limits.IsZero.iff_id_eq_zero, 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 : C
h : P X
⊢ P.isoModSerre (X := X) (Y := X) 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 : C
refine : (∃ (X_1 : C), P.isoModSerre (X := X_1) (Y := X) 0) → P X
⊢ (∃ (X_1 : C), P.isoModSerre (X := X_1) (Y := X) 0) ↔ P X

Tactic:
refine ⟨?_, fun _ ↦ ⟨X, 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
h : P.isoModSerre (X := Y) (Y := X) 0
⊢ P X

Tactic:
simpa using h.2

Premises used: And.right
-- 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
⊢ IsZero.{v', u'} (L.obj 0)

Tactic:
simpa [isZero_obj_iff L P] using P.prop_zero

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.isZero_obj_iff, CategoryTheory.ObjectProperty.prop_zero