awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
X : C
P : InjectiveResolution.{v, u} X
⊢ Nonempty
    (IsLimit (F :=
      parallelPair (X :=
        ShortComplex.X₂
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        (ShortComplex.g
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        0)
      (KernelFork.ofι
        (ShortComplex.f
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        ⋯))

Tactic:
⟨KernelFork.mapIsLimit _ (P.isLimitKernelFork) F⟩

Premises used: CategoryTheory.InjectiveResolution.isLimitKernelFork, CategoryTheory.Limits.KernelFork.mapIsLimit, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
X : C
P : InjectiveResolution.{v, u} X
⊢ Nonempty
    (IsLimit (F :=
      parallelPair (X :=
        ShortComplex.X₂
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        (ShortComplex.g
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        0)
      (KernelFork.ofι
        (ShortComplex.f
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        ⋯))

Tactic:
exact ⟨KernelFork.mapIsLimit _ (P.isLimitKernelFork) F⟩
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
X : C
dsimp :
  IsIso (Y := (F.rightDerived 0).obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
          0)
        (InjectiveResolution.toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.homologyπ
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
              0 ≫
            NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X))) :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
              0 ⟶
            (F.rightDerived 0).obj X) :
      F.obj X ⟶ (F.rightDerived 0).obj X)
⊢ IsIso (Y := (F.rightDerived 0).obj X) (NatTrans.app F.toRightDerivedZero X)

Tactic:
dsimp [Functor.toRightDerivedZero]

Premises used: CategoryTheory.Functor.toRightDerivedZero
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
X : C
⊢ IsIso (Y := (F.rightDerived 0).obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
          0)
        (InjectiveResolution.toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.homologyπ
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
              0 ≫
            NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X))) :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
              0 ⟶
            (F.rightDerived 0).obj X) :
      F.obj X ⟶ (F.rightDerived 0).obj X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
⊢ IsIso (Y := F.rightDerived 0) F.toRightDerivedZero

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
⊢ Iso.hom F.rightDerivedZeroIsoSelf ≫ F.toRightDerivedZero = 𝟙 (F.rightDerived 0)

Tactic:
F.rightDerivedZeroIsoSelf.hom_inv_id

Premises used: CategoryTheory.Functor.toRightDerivedZero, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.rightDerivedZeroIsoSelf
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
⊢ CategoryStruct.comp (Y := F.rightDerived 0) F.toRightDerivedZero (Iso.hom F.rightDerivedZeroIsoSelf) = 𝟙 F

Tactic:
F.rightDerivedZeroIsoSelf.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.toRightDerivedZero, CategoryTheory.Functor.rightDerivedZeroIsoSelf
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
X : C
⊢ NatTrans.app (Iso.hom F.rightDerivedZeroIsoSelf) X ≫ NatTrans.app F.toRightDerivedZero X =
    𝟙 ((F.rightDerived 0).obj X)

Tactic:
F.rightDerivedZeroIsoSelf.hom_inv_id_app X

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.rightDerivedZeroIsoSelf
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteLimits F
X : C
⊢ CategoryStruct.comp (Y := (F.rightDerived 0).obj X) (NatTrans.app F.toRightDerivedZero X)
      (NatTrans.app (Iso.hom F.rightDerivedZeroIsoSelf) X) =
    𝟙 (F.obj X)

Tactic:
F.rightDerivedZeroIsoSelf.inv_hom_id_app X

Premises used: CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.rightDerivedZeroIsoSelf
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
inst_4 : P.IsSerreClass
⊢ P.IsClosedUnderIsomorphisms

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.ShortExact
⊢ P S.X₂ ↔ P S.X₁ ∧ P S.X₃

Tactic:
⟨fun h ↦ ⟨P.prop_X₁_of_shortExact hS h, P.prop_X₃_of_shortExact hS h⟩,
    fun h ↦ P.prop_X₂_of_shortExact hS h.1 h.2⟩

Premises used: CategoryTheory.ObjectProperty.prop_X₂_of_shortExact, And.right, And.left, And.intro, Iff.intro, CategoryTheory.ObjectProperty.prop_X₃_of_shortExact, CategoryTheory.ObjectProperty.prop_X₁_of_shortExact
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
let : P S.X₂
⊢ P S.X₂

Tactic:
let d := S.homologyData
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
⊢ Epi d.left.f'

Tactic:
have := hS.epi_f' d.left
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this : Epi d.left.f'
⊢ Mono d.right.g'

Tactic:
have := hS.mono_g' d.right
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this_1 : Epi d.left.f'
this : Mono d.right.g'
⊢ P S.X₂

Tactic:
(P.prop_X₂_of_shortExact (hS.shortExact d)
    (P.prop_of_epi d.left.f' h₁) (P.prop_of_mono d.right.g' h₃) :)

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.Exact.shortExact, CategoryTheory.ObjectProperty.prop_X₂_of_shortExact, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ObjectProperty.prop_of_epi, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ObjectProperty.prop_of_mono, CategoryTheory.ShortComplex.HomologyData.right
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this_1 : Epi d.left.f'
this : Mono d.right.g'
⊢ P S.X₂

Tactic:
exact (P.prop_X₂_of_shortExact (hS.shortExact d)
    (P.prop_of_epi d.left.f' h₁) (P.prop_of_mono d.right.g' h₃) :)

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.Exact.shortExact, CategoryTheory.ObjectProperty.prop_X₂_of_shortExact, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ObjectProperty.prop_of_epi, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ObjectProperty.prop_of_mono, CategoryTheory.ShortComplex.HomologyData.right
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
h : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), G.kernel.isoModSerre f ↔ inverseImage (isomorphisms C) G f
⊢ G.kernel.isoModSerre = inverseImage (isomorphisms C) G

Tactic:
ext X Y f
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
⊢ G.kernel ≤ G.kernel

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
h : ∀ (hf : inverseImage (isomorphisms C) G f), G.kernel.isoModSerre f
⊢ G.kernel.isoModSerre f ↔ inverseImage (isomorphisms C) G f

Tactic:
refine ⟨(G.kernel.isoModSerre_isInvertedBy_iff G).2 (by rfl) _, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : inverseImage (isomorphisms C) G f
⊢ IsIso (G.map f)

Tactic:
simp only [inverseImage_iff, isomorphisms.iff] at hf

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
h : G.kernel.monoModSerre f
h₁ : G.kernel.epiModSerre f
⊢ G.kernel.isoModSerre f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.monoModSerre f

Tactic:
KernelFork.IsLimit.isZero_of_mono
      (KernelFork.mapIsLimit _ (kernelIsKernel f) G)

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Limits.KernelFork.mapIsLimit, CategoryTheory.Limits.limit, CategoryTheory.ObjectProperty.monoModSerre, CategoryTheory.Limits.kernelIsKernel, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.monoModSerre f

Tactic:
exact KernelFork.IsLimit.isZero_of_mono
      (KernelFork.mapIsLimit _ (kernelIsKernel f) G)

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Limits.KernelFork.mapIsLimit, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.epiModSerre f

Tactic:
CokernelCofork.IsColimit.isZero_of_epi
      (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.ObjectProperty.epiModSerre, CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi, CategoryTheory.Limits.CokernelCofork.mapIsColimit, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.epiModSerre f

Tactic:
exact CokernelCofork.IsColimit.isZero_of_epi
      (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi, CategoryTheory.Limits.CokernelCofork.mapIsColimit
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
rw : G.kernel.isoModSerre = inverseImage (isomorphisms C) G
rw₁ rw₂ : inverseImage (isomorphisms C) G = inverseImage (isomorphisms C) G
⊢ G.kernel.isoModSerre = ObjectProperty.isLocal fun (x : D) ↦ x ∈ Set.range F.obj

Tactic:
rw [ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj,
    isoModSerre_kernel_eq_inverseImage_isomorphisms]

Premises used: CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms, CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
rw : G.IsLocalization (inverseImage (isomorphisms C) G)
⊢ G.IsLocalization G.kernel.isoModSerre

Tactic:
rw [isoModSerre_kernel_eq_inverseImage_isomorphisms G]

Premises used: CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
⊢ G.IsLocalization (inverseImage (isomorphisms C) G)

Tactic:
adj.isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization
-- Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
⊢ G.IsLocalization (inverseImage (isomorphisms C) G)

Tactic:
exact adj.isLocalization

Premises used: CategoryTheory.Adjunction.isLocalization
-- 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.epiModSerre 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.epiModSerre s), s ≫ f = 0) → P (Abelian.image f)
refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre 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
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
refine_1 : ∀ (this : P.epiModSerre (Y := Abelian.image f) (s ≫ Abelian.factorThruImage f)), P (Abelian.image f)
⊢ P (Abelian.image f)

Tactic:
have := P.epiModSerre.comp_mem s (Abelian.factorThruImage f) hs
      (epiModSerre_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
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
this : P.epiModSerre (Y := Abelian.image f) (s ≫ Abelian.factorThruImage f)
refine_1 : ∀ (this : P.epiModSerre (X := X') (Y := Abelian.image f) 0), P (Abelian.image f)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (this : P (Abelian.image f)), P (Abelian.image f)
⊢ P (Abelian.image f)

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

Premises used: CategoryTheory.ObjectProperty.epiModSerre_zero_iff