mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.isoModSerre (cokernel.π (f₁ - f₂))

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ ≫ cokernel.π (f₁ - f₂) = f₂ ≫ cokernel.π (f₁ - f₂)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.isoModSerre (cokernel.π (f₁ - f₂))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ ≫ cokernel.π (f₁ - f₂) = f₂ ≫ cokernel.π (f₁ - f₂)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ ≫ cokernel.π (f₁ - f₂) = f₂ ≫ cokernel.π (f₁ - f₂)
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ Cone (parallelPair f 0 ⋙ P.ι)

pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit ?c

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P (Cone.pt ?c)

Tactic:
·

Goal state after:
case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ Cone (parallelPair f 0 ⋙ P.ι)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.isoModSerre (kernel.ι (f₁ - f₂))

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ kernel.ι (f₁ - f₂) ≫ f₁ = kernel.ι (f₁ - f₂) ≫ f₂

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.isoModSerre (kernel.ι (f₁ - f₂))
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯))

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt

Tactic:
·

Goal state after:
case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯))
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt

Tactic:
·

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ kernel.ι (f₁ - f₂) ≫ f₁ = kernel.ι (f₁ - f₂) ≫ f₂

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ kernel.ι (f₁ - f₂) ≫ f₁ = kernel.ι (f₁ - f₂) ≫ f₂
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ Cocone (parallelPair f 0 ⋙ P.ι)

pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ IsColimit ?c

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P (Cocone.pt ?c)

Tactic:
·

Goal state after:
case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ Cocone (parallelPair f 0 ⋙ P.ι)
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯))

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯)).pt

Tactic:
·

Goal state after:
case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯))
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯)).pt

Tactic:
·

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯)).pt
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
tfae_3_to_1 : (∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0) → Mono (L.map 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

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE

Tactic:
have := Localization.essSurj L P.isoModSerre
  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)
  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⟩
  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]
  tfae_finish

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩.left = left 1

pp: case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩.right = right 1

Tactic:
·

Goal state after:
case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩.left = left 1
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
g h : G
b : X
⊢ ⟨fun b ↦ F.map (homOfPair b (g * h)), g * h⟩.left b =
    (⟨fun b ↦ F.map (homOfPair b g), g⟩ * ⟨fun b ↦ F.map (homOfPair b h), h⟩).left b

pp: case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
g h : G
⊢ ⟨fun b ↦ F.map (homOfPair b (g * h)), g * h⟩.right =
    (⟨fun b ↦ F.map (homOfPair b g), g⟩ * ⟨fun b ↦ F.map (homOfPair b h), h⟩).right

Tactic:
·

Goal state after:
case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
g h : G
b : X
⊢ ⟨fun b ↦ F.map (homOfPair b (g * h)), g * h⟩.left b =
    (⟨fun b ↦ F.map (homOfPair b g), g⟩ * ⟨fun b ↦ F.map (homOfPair b h), h⟩).left b
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
tfae_3_to_1 : (∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0) → Epi (L.map 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

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
x✝ : Mono f
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
x✝ : Mono f
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
x✝ : Epi f
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Epi f

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
x✝ : Epi f
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Epi f

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Epi f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
hw' : ∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

Tactic:
·

Goal state after:
case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w

pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
hw' : ∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w

Tactic:
·

Goal state after:
case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w