awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : L.EssSurj
h : Mono (L.map f)
rw : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) (0 ≫ L.map f)
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
have rw₁ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) 0
Tactic: rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
-- 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 : L.EssSurj
h : Mono (L.map f)
rw : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) (0 ≫ L.map f)
rw₁ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) 0
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
have rw₂ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f ≫ f)) 0
Tactic: rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
-- 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 : L.EssSurj
h : Mono (L.map f)
rw : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) (0 ≫ L.map f)
rw₁ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) 0
rw₂ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f ≫ f)) 0
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
have rw₃ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map 0) 0
Tactic: rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
-- 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 : L.EssSurj
h : Mono (L.map f)
rw : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) (0 ≫ L.map f)
rw₁ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) 0
rw₂ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f ≫ f)) 0
rw₃ : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map 0) 0
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
have rw₄ : Eq.{v' + 1} (α := L.obj (kernel f) ⟶ L.obj Y) 0 0
Tactic: rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
-- 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 : C
f : X ⟶ Y
this : L.EssSurj
h : Mono (L.map f)
⊢ P.monoModSerre f
have hf : Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
Tactic: have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
-- 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 : C
f : X ⟶ Y
this : L.EssSurj
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE
have tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
Tactic: tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
    simpa [hf] using map_comp_eq_zero_iff_of_epi_mono L P (𝟙 _) (kernel.ι f)
-- 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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : L.map z ≫ L.map f = 0
⊢ L.map z = 0
have hz₁ : L.map (z ≫ f) = 0
Tactic: rw [← L.map_comp] at hz
Cleared hypotheses: hz
-- 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : L.map (z ≫ f) = 0
⊢ L.map z = 0
have rw : ∀ (hz : ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), (z ≫ f) ≫ s = 0),
  ∃ (Y' : C) (s : X ⟶ Y') (_ : P.monoModSerre s), z ≫ s = 0
Tactic: rw [map_eq_zero_iff L P, ← exists_comp_monoModSerre_eq_zero_iff P] at hz ⊢
Cleared hypotheses: hz
-- 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), (z ≫ f) ≫ s = 0
⊢ ∃ (Y' : C) (s : X ⟶ Y') (_ : P.monoModSerre s), z ≫ s = 0
have obtain : ∀ (W : C) (s : Y ⟶ W) (hs : P.monoModSerre s) (eq : (z ≫ f) ≫ s = 0),
  ∃ (Y' : C) (s : X ⟶ Y') (_ : P.monoModSerre s), z ≫ s = 0
Tactic: obtain ⟨W, s, hs, eq⟩ := hz
Cleared hypotheses: hz
-- 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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE
have tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
Tactic: tfae_have 2 → 3 := fun hf ↦ by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_comp_monoModSerre_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    exact ⟨W, f ≫ s, MorphismProperty.comp_mem _ _ _ hf hs, by simpa using eq⟩
-- 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
⊢ Mono (L.map f)
have rw : ∀ (P : D) (g : P ⟶ L.obj X), g ≫ L.map f = 0 → g = 0
Tactic: rw [Preadditive.mono_iff_cancel_zero]
-- 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
⊢ z = 0
have obtain : ∀ (φ : P.isoModSerre.RightFraction (L.objPreimage W) X)
  (hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L sorry), z = 0
Tactic: obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ z)
-- 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
⊢ z = 0
have rw : L.map (φ.f (W := P.isoModSerre)) = 0
Tactic: rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]
-- 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 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map (φ.f (W := P.isoModSerre)) = 0
have apply : L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
Tactic: apply hf φ.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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have this₁ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
Tactic: have : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f := by cat_disch
-- 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_1 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
Tactic: rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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_1 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
Tactic: rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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_1 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z ≫ L.map f = 0
Tactic: rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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_1 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z ≫ L.map f = 0
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have rw₃ : Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y)
  (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ 0) 0
Tactic: rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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_1 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z ≫ L.map f = 0
rw₃ :
  Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y)
    (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ 0) 0
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have rw₄ : Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y) (L.map (φ.s (W := P.isoModSerre)) ≫ 0) 0
Tactic: rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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_1 : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ z = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ z) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ z ≫ L.map f = 0
rw₃ :
  Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y)
    (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ 0) 0
rw₄ : Eq (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y) (L.map (φ.s (W := P.isoModSerre)) ≫ 0) 0
⊢ L.map (φ.f (W := P.isoModSerre)) ≫ L.map f = 0
have rw₅ : Eq.{v' + 1} (α := L.obj (φ.X' (W := P.isoModSerre)) ⟶ L.obj Y) 0 0
Tactic: rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Mono (L.map f)), P.monoModSerre f
tfae_2_to_3 : ∀ (a : P.monoModSerre f) ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE
have tfae_3_to_1 : ∀ (a : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0), Mono (L.map f)
Tactic: tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.mono_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ z)
    rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]
    apply hf φ.f
    have : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f := by cat_disch
    rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
-- 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 : C
f : X ⟶ Y
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE
have this : L.EssSurj
Tactic: have := Localization.essSurj L P.isoModSerre
-- 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 : L.EssSurj
h : Epi (L.map f)
⊢ Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0
have rw : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) (L.map f ≫ 0)
Tactic: rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]
-- 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 : L.EssSurj
h : Epi (L.map f)
rw : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) (L.map f ≫ 0)
⊢ Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0
have rw₁ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) 0
Tactic: rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]