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_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 : P.monoModSerre f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
have refine_1 : Arrow.mk (L.map f) ≅ Arrow.mk (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))
Tactic: refine ⟨_, _, Abelian.image.ι f, inferInstance, ⟨Iso.symm ?_⟩⟩
-- 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 : P.monoModSerre f
⊢ Arrow.mk (L.map f) ≅ Arrow.mk (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))
have this₁ : IsIso (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f))
Tactic: have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_factorThruImage
-- 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
⊢ Epi f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have this : L.PreservesEpimorphisms
Tactic: have := preservesEpimorphisms 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.PreservesEpimorphisms
⊢ Epi f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi 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.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ Epi f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have refine_1 : Epi f → ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi 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.PreservesEpimorphisms
this : L.mapArrow.EssSurj
refine_1 : Epi f → ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ Epi f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have refine_2 : (∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Epi 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.PreservesEpimorphisms
this_2 : L.mapArrow.EssSurj
h : Epi f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) →
      ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi 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') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have obtain : ∀ (X' Y' : C) (f' : X' ⟶ Y'),
  Epi 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') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
Tactic: obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.epimorphisms 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.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk f)
have refine_1 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
  Epi (L.map f) →
    ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
Tactic: suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Epi (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Epi 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.epimorphisms 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.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : Epi (L.map f)
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
have hf₁ : P.epiModSerre f
Tactic: rw [epi_map_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_1 Y_1 : D
f_1 : X_1 ⟶ Y_1
this_1 : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty.{v' + 1} (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
have refine_1 : Arrow.mk (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f)) ≅ Arrow.mk (L.map f)
Tactic: refine ⟨_, _, Abelian.factorThruImage f, inferInstance, ⟨?_⟩⟩
-- 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.PreservesEpimorphisms
this : L.mapArrow.EssSurj
h : Epi f_1
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ Arrow.mk (Y := L.obj (Abelian.image f)) (L.map (Abelian.factorThruImage f)) ≅ Arrow.mk (L.map f)
have this₁ : IsIso (X := L.obj (Abelian.image f)) (L.map (Abelian.image.ι f))
Tactic: have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_image_ι
-- 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
⊢ PreservesLimit (parallelPair f 0) L
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 : C
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ PreservesLimit (parallelPair f 0) L
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_1 : L.PreservesMonomorphisms
this : L.EssSurj
⊢ PreservesLimit (parallelPair f 0) L
have suffices : ∀ (W : D) (z : W ⟶ L.obj X) (hz : z ≫ L.map f = 0), ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = z
Tactic: suffices ∀ (W : D) (z : W ⟶ L.obj X) (hz : z ≫ L.map f = 0),
      ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = z from
    preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
      ((KernelFork.isLimitMapConeEquiv _ L).2
        (Fork.IsLimit.ofExistsUnique
          (fun s ↦ existsUnique_of_exists_of_unique
            (this _ _ (KernelFork.condition s))
            (fun _ _ h₁ h₂ ↦ by simpa [cancel_mono] using h₁.trans h₂.symm))))
-- 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.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
have inr : ∀
  (this :
    ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
      (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
      ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w)
  (hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
  ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
Tactic: wlog hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
      generalizing W
-- 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.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
inr :
  ∀
    (this :
      ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
        (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
        ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w)
    (hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
have wlog : ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
  (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
  ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
Tactic: wlog hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
      generalizing W
Cleared hypotheses: W, w, hw
-- 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
have inr : ∀ (φ : P.isoModSerre.RightFraction (L.objPreimage W) X)
  (hφ : Iso.hom (L.objObjPreimageIso W) ≫ w = φ.map (W := P.isoModSerre) L sorry),
  ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
Tactic: obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ w)
-- 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_1 : L.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : Iso.hom (L.objObjPreimageIso W) ≫ w = φ.map (W := P.isoModSerre) L ⋯
⊢ ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
have hφ₁ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
Tactic: rw [← cancel_epi (L.map φ.s),
      MorphismProperty.RightFraction.map_s_comp_map] at hφ
Cleared hypotheses: 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = 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) ≫ w) ≫ L.map f = 0
Tactic: rw [← hφ, Category.assoc, Category.assoc, hw, 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ 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) ≫ w) ≫ L.map f = 0
Tactic: rw [← hφ, Category.assoc, Category.assoc, hw, 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ 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) ≫ w ≫ L.map f = 0
Tactic: rw [← hφ, Category.assoc, Category.assoc, hw, 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w ≫ 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 [← hφ, Category.assoc, Category.assoc, hw, 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w ≫ 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 [← hφ, Category.assoc, Category.assoc, hw, 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.PreservesMonomorphisms
this_2 : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X) (hw : w ≫ L.map f = 0)
    (hw' : ∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z),
    ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ (Z : C) (hZ : W = L.obj Z) (z : Z ⟶ X), w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w = L.map (φ.f (W := P.isoModSerre))
rw : (L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₁ : L.map (φ.s (W := P.isoModSerre)) ≫ (Iso.hom (L.objObjPreimageIso W) ≫ w) ≫ L.map f = 0
rw₂ : L.map (φ.s (W := P.isoModSerre)) ≫ Iso.hom (L.objObjPreimageIso W) ≫ w ≫ 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 [← hφ, Category.assoc, Category.assoc, hw, comp_zero, comp_zero]