awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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 : D
f : X ⟶ Y
g : Arrow.{v, u} C
e : L.mapArrow.obj g ≅ Arrow.mk f
this : PreservesColimit (parallelPair g.hom 0) L
⊢ HasCokernel f
have this₁ : HasColimit (parallelPair (L.map g.hom) 0)
Tactic: have : HasColimit (parallelPair (L.map g.hom) 0) :=
      ⟨_, (CokernelCofork.isColimitMapCoconeEquiv _ L).1
        (isColimitOfPreserves L (cokernelIsCokernel g.hom))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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 : D
f : X ⟶ Y
hf : Mono f
⊢ Nonempty (NormalMono f)
have hf₁ : ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
Tactic: rw [mono_iff L P] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : D
f : X ⟶ Y
hf : ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ Nonempty (NormalMono f)
have obtain : ∀ (X' Y' : C) (f' : X' ⟶ Y'), Mono f' → ∀ (e : Arrow.mk (L.map f') ≅ Arrow.mk f), Nonempty (NormalMono f)
Tactic: obtain ⟨X', Y', f', _, ⟨e⟩⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
⊢ Nonempty (NormalMono f)
have this : PreservesLimit
  (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
Tactic: have := preservesKernel L P hf'.g
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
⊢ Nonempty (NormalMono f)
have refine : NormalMono (L.map f')
Tactic: refine ⟨NormalMono.ofArrowIso ?_ e⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this :
  PreservesLimit
    (parallelPair (X := Y') (Y := @NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalMono.g 0) L
⊢ Eq (α := L.obj X' ⟶ L.obj (@NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _))
    (L.map f' ≫ L.map NormalMono.g) 0
have rw : Eq (α := L.obj X' ⟶ L.obj (@NormalMono.Z _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _))
  (L.map (f' ≫ NormalMono.g)) 0
Tactic: rw [← L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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 : D
f : X ⟶ Y
hf : Epi f
⊢ Nonempty (NormalEpi f)
have hf₁ : ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
Tactic: rw [epi_iff L P] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : D
f : X ⟶ Y
hf : ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ Nonempty (NormalEpi f)
have obtain : ∀ (X' Y' : C) (f' : X' ⟶ Y'), Epi f' → ∀ (e : Arrow.mk (L.map f') ≅ Arrow.mk f), Nonempty (NormalEpi f)
Tactic: obtain ⟨X', Y', f', _, ⟨e⟩⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
⊢ Nonempty (NormalEpi f)
have this : PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0) L
Tactic: have := preservesCokernel L P hf'.g
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
⊢ Nonempty (NormalEpi f)
have refine : NormalEpi (L.map f')
Tactic: refine ⟨NormalEpi.ofArrowIso ?_ e⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
w : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this :
  PreservesColimit (parallelPair (X := @NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) NormalEpi.g 0)
    L
⊢ Eq (α := L.obj (@NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) ⟶ L.obj Y')
    (L.map NormalEpi.g ≫ L.map f') 0
have rw : Eq (α := L.obj (@NormalEpi.W _ _ _ _ Preadditive.preadditiveHasZeroMorphisms f' _) ⟶ L.obj Y')
  (L.map (NormalEpi.g ≫ f')) 0
Tactic: rw [← L.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
⊢ Abelian.{v', u'} D
have this : HasFiniteProducts.{v', u'} D
Tactic: have := hasFiniteProducts L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this : HasFiniteProducts.{v', u'} D
⊢ Abelian.{v', u'} D
have this₁ : HasKernels.{v', u'} D
Tactic: have := hasKernels L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : HasFiniteProducts.{v', u'} D
this : HasKernels.{v', u'} D
⊢ Abelian.{v', u'} D
have this₁ : HasCokernels.{v', u'} D
Tactic: have := hasCokernels L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : HasFiniteProducts.{v', u'} D
this_2 : HasKernels.{v', u'} D
this : HasCokernels.{v', u'} D
⊢ Abelian.{v', u'} D
have this₁ : IsNormalMonoCategory.{v', u'} D
Tactic: have := isNormalMonoCategory L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : HasFiniteProducts.{v', u'} D
this_2 : HasKernels.{v', u'} D
this_3 : HasCokernels.{v', u'} D
this : IsNormalMonoCategory.{v', u'} D
⊢ Abelian.{v', u'} D
have this₁ : IsNormalEpiCategory.{v', u'} D
Tactic: have := isNormalEpiCategory L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
this : Abelian.{v', u'} D := abelian L P
⊢ PreservesFiniteLimits L
have rw : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
Tactic: rw [((Functor.preservesFiniteLimits_tfae L).out 3 2 :)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
this : Abelian.{v', u'} D := abelian L P
⊢ PreservesFiniteColimits L
have rw : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
Tactic: rw [((Functor.preservesFiniteColimits_tfae L).out 3 2 :)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : Abelian.{v', u'} D := abelian L P
⊢ IsIso (L.map f) ↔ P.isoModSerre f
have rw : Mono (L.map f) ∧ Epi (L.map f) ↔ P.isoModSerre f
Tactic: rw [isIso_iff_mono_and_epi, mono_map_iff L P, epi_map_iff L P, isoModSerre_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : Abelian.{v', u'} D := abelian L P
rw : Mono (L.map f) ∧ Epi (L.map f) ↔ P.isoModSerre f
⊢ IsIso (L.map f) ↔ P.isoModSerre f
have rw₁ : P.monoModSerre f ∧ Epi (L.map f) ↔ P.isoModSerre f
Tactic: rw [isIso_iff_mono_and_epi, mono_map_iff L P, epi_map_iff L P, isoModSerre_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : Abelian.{v', u'} D := abelian L P
rw : Mono (L.map f) ∧ Epi (L.map f) ↔ P.isoModSerre f
rw₁ : P.monoModSerre f ∧ Epi (L.map f) ↔ P.isoModSerre f
⊢ IsIso (L.map f) ↔ P.isoModSerre f
have rw₂ : P.monoModSerre f ∧ P.epiModSerre f ↔ P.isoModSerre f
Tactic: rw [isIso_iff_mono_and_epi, mono_map_iff L P, epi_map_iff L P, isoModSerre_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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 : Abelian.{v', u'} D := abelian L P
rw : Mono (L.map f) ∧ Epi (L.map f) ↔ P.isoModSerre f
rw₁ : P.monoModSerre f ∧ Epi (L.map f) ↔ P.isoModSerre f
rw₂ : P.monoModSerre f ∧ P.epiModSerre f ↔ P.isoModSerre f
⊢ IsIso (L.map f) ↔ P.isoModSerre f
have rw₃ : P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f
Tactic: rw [isIso_iff_mono_and_epi, mono_map_iff L P, epi_map_iff L P, isoModSerre_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
⊢ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) L = P.isoModSerre
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) L f ↔ P.isoModSerre f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this : Abelian.{v', u'} D := abelian L P
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits G
have this₁ : PreservesFiniteLimits L
Tactic: have := preservesFiniteLimits L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteLimits L
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits G
have refine : PreservesFiniteLimits (L ⋙ G) → PreservesFiniteLimits G
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteLimits _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
⊢ PreservesFiniteLimits G
have this₁ : G.Additive
Tactic: have := (Localization.functor_additive_iff L P.isoModSerre G).mpr
    (L ⋙ G).additive_of_preserves_binary_products
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
⊢ PreservesFiniteLimits G
have refine : ∀ (x x_1 : D) (f : x ⟶ x_1), PreservesLimit (parallelPair f 0) G
Tactic: refine ((Functor.preservesFiniteLimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
⊢ PreservesLimit (parallelPair f 0) G
have obtain : ∀ (f' : Arrow.{v, u} C) (iso : L.mapArrow.obj f' ≅ Arrow.mk f), PreservesLimit (parallelPair f 0) G
Tactic: obtain ⟨f', ⟨iso⟩⟩ :=
    (Localization.essSurj_mapArrow L P.isoModSerre).mem_essImage (Arrow.mk f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteLimits L
h : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
⊢ PreservesLimit (parallelPair f 0) G
have this₁ : PreservesLimit (parallelPair (L.map f'.hom) 0) G
Tactic: have : PreservesLimit (parallelPair (L.map f'.hom) 0) G :=
    preservesLimit_of_preserves_limit_cone
      (KernelFork.isLimitMapConeEquiv _ _
        (isLimitOfPreserves L (kernelIsKernel f'.hom)))
          ((KernelFork.isLimitMapConeEquiv _ G).symm
            (KernelFork.isLimitMapConeEquiv _ (L ⋙ G)
              (isLimitOfPreserves (L ⋙ G) (kernelIsKernel f'.hom))))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this : Abelian.{v', u'} D := abelian L P
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G
have this₁ : PreservesFiniteColimits L
Tactic: have := preservesFiniteColimits L P
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
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
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G
have refine : PreservesFiniteColimits (L ⋙ G) → PreservesFiniteColimits G
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteColimits _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
⊢ (L ⋙ G).Additive
have this₁ : PreservesBinaryBiproducts (L ⋙ G)
Tactic: have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
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
this_1 : Abelian.{v', u'} D := abelian L P
this : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
⊢ PreservesFiniteColimits G
have this₁ : G.Additive
Tactic: have := (Localization.functor_additive_iff L P.isoModSerre G).mpr (by
    have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)
    exact Functor.additive_of_preservesBinaryBiproducts _)