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 : Epi (L.map f)
rw : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) (L.map f ≫ 0)
rw₁ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π 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 ≫ cokernel.π 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)
rw₁ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) 0
rw₂ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map (f ≫ cokernel.π 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 0) 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)
rw₁ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map f ≫ L.map (cokernel.π f)) 0
rw₂ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map (f ≫ cokernel.π f)) 0
rw₃ : Eq (α := L.obj X ⟶ L.obj (cokernel f)) (L.map 0) 0
⊢ Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0
have rw₄ : Eq.{v' + 1} (α := L.obj X ⟶ L.obj (cokernel f)) 0 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 (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 : Epi (L.map f)
⊢ P.epiModSerre f
have hf : Eq (α := L.obj Y ⟶ L.obj (cokernel f)) (L.map (cokernel.π f)) 0
Tactic: have hf : L.map (cokernel.π f) = 0 := by
      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 (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
⊢ [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 tfae_1_to_2 : ∀ (a : Epi (L.map f)), P.epiModSerre f
Tactic: tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]
    simpa [hf] using map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π 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 : Epi (L.map f)), P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : L.map f ≫ L.map z = 0
⊢ L.map z = 0
have hz₁ : L.map (f ≫ z) = 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 : Epi (L.map f)), P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : L.map (f ≫ z) = 0
⊢ L.map z = 0
have rw : ∀ (hz : ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f ≫ z = 0),
  ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 0
Tactic: rw [map_eq_zero_iff L P, ← exists_epiModSerre_comp_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 : Epi (L.map f)), P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f ≫ z = 0
⊢ ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 0
have obtain : ∀ (W : C) (s : W ⟶ X) (hs : P.epiModSerre s) (eq : s ≫ f ≫ z = 0),
  ∃ (X' : C) (s : X' ⟶ Y) (_ : P.epiModSerre s), s ≫ z = 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 : Epi (L.map f)), P.epiModSerre f
⊢ [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 tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 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_epiModSerre_comp_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    refine ⟨_, s ≫ f, MorphismProperty.comp_mem _ _ _ hs hf, by simpa⟩
-- 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ Epi (L.map f)
have rw : ∀ (R : D) (g : L.obj Y ⟶ R), L.map f ≫ g = 0 → g = 0
Tactic: rw [Preadditive.epi_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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
⊢ z = 0
have obtain : ∀ (φ : P.isoModSerre.LeftFraction Y (L.objPreimage W))
  (hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L sorry), z = 0
Tactic: obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (L.objObjPreimageIso W).inv)
-- 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
⊢ z = 0
have rw : L.map (φ.f (W := P.isoModSerre)) = 0
Tactic: rw [← cancel_mono (L.objObjPreimageIso W).inv, zero_comp, hφ,
      ← cancel_mono (L.map φ.s), zero_comp,
      MorphismProperty.LeftFraction.map_comp_map_s]
-- 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map (φ.f (W := P.isoModSerre)) = 0
have apply : L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
⊢ L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 0
have this₁ : L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))
Tactic: have : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s := by
      simp [reassoc_of% hφ]
-- 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))
⊢ L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 0
have rw : L.map f ≫ z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = 0
Tactic: rw [this, reassoc_of% hz, zero_comp]
-- 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))
rw : L.map f ≫ z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = 0
⊢ L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 0
have rw₁ : Eq (α := L.obj X ⟶ L.obj (φ.Y' (W := P.isoModSerre)))
  (0 ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))) 0
Tactic: rw [this, reassoc_of% hz, zero_comp]
-- 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 : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ Iso.inv (L.objObjPreimageIso W) = φ.map (W := P.isoModSerre) L ⋯
this : L.map (φ.f (W := P.isoModSerre)) = z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))
rw : L.map f ≫ z ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre)) = 0
rw₁ :
  Eq (α := L.obj X ⟶ L.obj (φ.Y' (W := P.isoModSerre)))
    (0 ≫ Iso.inv (L.objObjPreimageIso W) ≫ L.map (φ.s (W := P.isoModSerre))) 0
⊢ L.map f ≫ L.map (φ.f (W := P.isoModSerre)) = 0
have rw₂ : Eq.{v' + 1} (α := L.obj X ⟶ L.obj (φ.Y' (W := P.isoModSerre))) 0 0
Tactic: rw [this, reassoc_of% hz, zero_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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : ∀ (a : Epi (L.map f)), P.epiModSerre f
tfae_2_to_3 : ∀ (a : P.epiModSerre f) ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ [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 tfae_3_to_1 : ∀ (a : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0), Epi (L.map f)
Tactic: tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.epi_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (L.objObjPreimageIso W).inv)
    rw [← cancel_mono (L.objObjPreimageIso W).inv, zero_comp, hφ,
      ← cancel_mono (L.map φ.s), zero_comp,
      MorphismProperty.LeftFraction.map_comp_map_s]
    apply hf φ.f
    have : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s := by
      simp [reassoc_of% hφ]
    rw [this, reassoc_of% hz, zero_comp]
-- 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.monomorphisms D) L = P.monoModSerre
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.inverseImage (MorphismProperty.monomorphisms D) L f ↔ P.monoModSerre f
Tactic: ext
-- 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.epimorphisms D) L = P.epiModSerre
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.inverseImage (MorphismProperty.epimorphisms D) L f ↔ P.epiModSerre 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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
⊢ Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have this : L.PreservesMonomorphisms
Tactic: have := preservesMonomorphisms 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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have this₁ : L.mapArrow.EssSurj
Tactic: have := Localization.essSurj_mapArrow 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 : D
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have refine_1 : Mono f → ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
Tactic: refine ⟨fun _ ↦ ?_, ?_⟩
-- 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
this_1 : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
refine_1 :
  Mono f → ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have refine_2 : (∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f
Tactic: refine ⟨fun _ ↦ ?_, ?_⟩
-- 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
this_1 : L.PreservesMonomorphisms
this_2 : L.mapArrow.EssSurj
h : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) →
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have obtain : ∀ (X' Y' : C) (f' : X' ⟶ Y'),
  Mono f' →
    ∀ (e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)),
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
Tactic: obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property 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
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : D
f : X ⟶ Y
this_1 : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
h : Mono f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have refine_1 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
  Mono (L.map f) →
    ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
Tactic: suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Mono (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩
-- 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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
h : Mono f_1
X Y : C
f : X ⟶ Y
hf : Mono (L.map f)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
have hf₁ : P.monoModSerre f
Tactic: rw [mono_map_iff L P] at hf
Cleared hypotheses: hf