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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
⊢ exactFunctor C E (L ⋙ G) ↔ exactFunctor D E G

Tactic:
simp [preservesFiniteLimits_comp_iff L P, preservesFiniteColimits_comp_iff L P]

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits_comp_iff, CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits_comp_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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G_1 : Functor.{v', v'', u', u''} D E
G : ExactFunctor.{v', v'', u', u''} D E
dsimp : exactFunctor C E (L ⋙ G.obj (P := exactFunctor D E))
⊢ exactFunctor C E (Functor.obj (ι (exactFunctor D E) ⋙ Functor.obj (Functor.whiskeringLeft C D E) L) G)

Tactic:
dsimp
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G_1 : Functor.{v', v'', u', u''} D E
G : ExactFunctor.{v', v'', u', u''} D E
⊢ exactFunctor C E (L ⋙ G.obj (P := exactFunctor D E))

Tactic:
simpa only [exactFunctor_comp_iff L P] using G.property

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.exactFunctor_comp_iff, CategoryTheory.ObjectProperty.FullSubcategory.property
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : ExactFunctor.{v', v'', u', u''} D E
⊢ (Functor.obj (whiskeringLeft L P E) G).obj (P := exactFunctor C E) = L ⋙ G.obj (P := exactFunctor D E)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
⊢ Functor.Faithful (C := ExactFunctor.{v', v'', u', u''} D E) (whiskeringLeft L P E)

Tactic:
(fullyFaithfulWhiskeringLeft L P E).faithful

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.fullyFaithfulWhiskeringLeft, CategoryTheory.Functor.FullyFaithful.faithful
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
⊢ Functor.Full (C := ExactFunctor.{v', v'', u', u''} D E) (whiskeringLeft L P E)

Tactic:
(fullyFaithfulWhiskeringLeft L P E).full

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.fullyFaithfulWhiskeringLeft, CategoryTheory.Functor.FullyFaithful.full
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
h :
  ∀ (F : ExactFunctor.{v, v'', u, u''} C E),
    Functor.essImage (whiskeringLeft L P E) F ↔ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ Eq (α := ObjectProperty (ExactFunctor.{v, v'', u, u''} C E)) (Functor.essImage (whiskeringLeft L P E))
    fun (G : ExactFunctor.{v, v'', u, u''} C E) ↦ P.isoModSerre.IsInvertedBy (G.obj (P := exactFunctor C E))

Tactic:
ext 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
⊢ Functor.essImage (whiskeringLeft L P E) F ↔ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))

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
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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
h : Functor.essImage (whiskeringLeft L P E) F → P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
h₁ : ∀ (hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))), Functor.essImage (whiskeringLeft L P E) F
⊢ Functor.essImage (whiskeringLeft L P E) F ↔ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))

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
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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
G : ExactFunctor.{v', v'', u', u''} D E
e : Functor.obj (whiskeringLeft L P E) G ≅ F
h : P.isoModSerre.IsInvertedBy (L ⋙ G.obj (P := exactFunctor D E))
⊢ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))

Tactic:
rw [← MorphismProperty.IsInvertedBy.iff_of_iso _
      (show L ⋙ G.obj ≅ F.obj from (ObjectProperty.ι _).mapIso e)]

Premises used: CategoryTheory.exactFunctor, CategoryTheory.ObjectProperty.ι, CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso, CategoryTheory.Functor.mapIso
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
G : ExactFunctor.{v', v'', u', u''} D E
e : Functor.obj (whiskeringLeft L P E) G ≅ F
⊢ P.isoModSerre.IsInvertedBy (L ⋙ G.obj (P := exactFunctor D E))

Tactic:
MorphismProperty.IsInvertedBy.of_comp _ _ (Localization.inverts L _) _

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_comp, CategoryTheory.Localization.inverts
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
G : ExactFunctor.{v', v'', u', u''} D E
e : Functor.obj (whiskeringLeft L P E) G ≅ F
⊢ P.isoModSerre.IsInvertedBy (L ⋙ G.obj (P := exactFunctor D E))

Tactic:
exact MorphismProperty.IsInvertedBy.of_comp _ _ (Localization.inverts L _) _

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_comp, CategoryTheory.Localization.inverts
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ Functor.essImage (whiskeringLeft L P E) F

Tactic:
⟨⟨Localization.lift F.obj hF L, ?_⟩,
      ⟨ObjectProperty.isoMk _ (Localization.fac F.obj hF L)⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.ObjectProperty.isoMk, Exists.intro, CategoryTheory.Localization.lift, CategoryTheory.Localization.fac
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
h : exactFunctor D E (Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)
⊢ Functor.essImage (whiskeringLeft L P E) F

Tactic:
refine ⟨⟨Localization.lift F.obj hF L, ?_⟩,
      ⟨ObjectProperty.isoMk _ (Localization.fac F.obj hF L)⟩⟩
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
h : exactFunctor C E (L ⋙ Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)
⊢ exactFunctor D E (Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)

Tactic:
rw [← exactFunctor_comp_iff L P]

Premises used: CategoryTheory.ObjectProperty.SerreClassLocalization.exactFunctor_comp_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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ exactFunctor C E (L ⋙ Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)

Tactic:
ObjectProperty.prop_of_iso _ (Localization.fac F.obj hF L).symm F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Iso.symm, CategoryTheory.Localization.fac
-- 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
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ exactFunctor C E (L ⋙ Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)

Tactic:
exact ObjectProperty.prop_of_iso _ (Localization.fac F.obj hF L).symm F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Iso.symm, CategoryTheory.Localization.fac
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
⊢ P.monoModSerre f ↔ P (kernel f)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.monoModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
⊢ monomorphisms C ≤ P.monoModSerre

Tactic:
fun _ _ f (_ : Mono f) ↦ P.prop_of_isZero (isZero_kernel_of_mono f)

Premises used: CategoryTheory.Limits.isZero_kernel_of_mono, CategoryTheory.ObjectProperty.prop_of_isZero, CategoryTheory.ObjectProperty.monoModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Mono f
⊢ P.monoModSerre f

Tactic:
P.monomorphisms_le_monoModSerre f (monomorphisms.infer_property f)

Premises used: CategoryTheory.ObjectProperty.monomorphisms_le_monoModSerre, CategoryTheory.MorphismProperty.monomorphisms.infer_property
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
⊢ P.epiModSerre f ↔ P (cokernel f)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.epiModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
⊢ epimorphisms C ≤ P.epiModSerre

Tactic:
fun _ _ f (_ : Epi f) ↦ P.prop_of_isZero (isZero_cokernel_of_epi f)

Premises used: CategoryTheory.Limits.isZero_cokernel_of_epi, CategoryTheory.ObjectProperty.prop_of_isZero, CategoryTheory.ObjectProperty.epiModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Epi f
⊢ P.epiModSerre f

Tactic:
P.epimorphisms_le_epiModSerre f (epimorphisms.infer_property f)

Premises used: CategoryTheory.ObjectProperty.epimorphisms_le_epiModSerre, CategoryTheory.MorphismProperty.epimorphisms.infer_property
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
⊢ P.epiModSerre (X := X) (Y := Y) 0 ↔ P Y

Tactic:
P.prop_iff_of_iso cokernelZeroIsoTarget

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.ObjectProperty.epiModSerre, CategoryTheory.Limits.cokernelZeroIsoTarget
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
⊢ P.monoModSerre (X := X) (Y := Y) 0 ↔ P X

Tactic:
P.prop_iff_of_iso kernelZeroIsoSource

Premises used: CategoryTheory.Limits.kernelZeroIsoSource, CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.ObjectProperty.monoModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
⊢ P.isoModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.isoModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Mono f
⊢ P.monoModSerre f

Tactic:
have := P.monoModSerre_of_mono f
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Mono f
this : P.monoModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.epiModSerre f
mpr : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mp₁ mp₂ mp₃ : P.monoModSerre f → P.epiModSerre f → P.epiModSerre f
mpr₁ mpr₂ : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mpr₃ : P.epiModSerre f → P.monoModSerre f
mpr₄ : P.epiModSerre f → P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Epi f
⊢ P.epiModSerre f

Tactic:
have := P.epiModSerre_of_epi f
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Epi f
this : P.epiModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.monoModSerre f
mpr : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mp₁ mp₂ mp₃ : P.monoModSerre f → P.epiModSerre f → P.monoModSerre f
mpr₁ mpr₂ : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mpr₃ : P.monoModSerre f → P.monoModSerre f
mpr₄ : P.monoModSerre f → P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Mono f
hf rwa rwa₁ rwa₂ rwa₃ : P.epiModSerre f
⊢ P.isoModSerre f

Tactic:
rwa [isoModSerre_iff_of_mono]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : Epi f
hf rwa rwa₁ rwa₂ rwa₃ : P.monoModSerre f
⊢ P.isoModSerre f

Tactic:
rwa [isoModSerre_iff_of_epi]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
⊢ P.isoModSerre (X := X) (Y := Y) 0 ↔ P X ∧ P Y

Tactic:
simp [isoModSerre_iff]

Premises used: CategoryTheory.ObjectProperty.isoModSerre_iff
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
⊢ isomorphisms C ≤ P.isoModSerre

Tactic:
fun _ _ f (_ : IsIso f) ↦ ⟨P.monoModSerre_of_mono f, P.epiModSerre_of_epi f⟩

Premises used: CategoryTheory.ObjectProperty.monoModSerre_of_mono, CategoryTheory.ObjectProperty.epiModSerre_of_epi, And.intro, CategoryTheory.ObjectProperty.isoModSerre
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
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
inst_3 : IsIso f
⊢ P.isoModSerre f

Tactic:
P.isomorphisms_le_isoModSerre f (isomorphisms.infer_property f)

Premises used: CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre, CategoryTheory.MorphismProperty.isomorphisms.infer_property
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsMultiplicative

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
h : RetractArrow f' f
hf : P.monoModSerre f
⊢ f' ≫ h.right.i = h.left.i ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
h : RetractArrow f' f
hf : P.epiModSerre f
⊢ f ≫ h.right.r = h.left.r ≫ f'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
⊢ (P.monoModSerre ⊓ P.epiModSerre).IsStableUnderRetracts

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isoModSerre g
hfg : P.isoModSerre (f ≫ g)
⊢ f ≫ g = 𝟙 X ≫ f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.isoModSerre f
hfg : P.isoModSerre (f ≫ g)
⊢ (f ≫ g) ≫ 𝟙 Z = f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
hX : P X
f : 0 ⟶ X := 0
⊢ IsIso (F.map f)

Tactic:
have := hF _ ((P.isoModSerre_iff_of_mono f).2
    ((P.prop_iff_of_iso cokernelZeroIsoTarget).2 hX))