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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
⊢ PreservesFiniteColimits G
have refine : ∀ (x x_1 : D) (f : x ⟶ x_1), PreservesColimit (parallelPair f 0) G
Tactic: refine ((Functor.preservesFiniteColimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
⊢ PreservesColimit (parallelPair f 0) G
have obtain : ∀ (f' : Arrow.{v, u} C) (iso : L.mapArrow.obj f' ≅ Arrow.mk f), PreservesColimit (parallelPair f 0) G
Tactic: obtain ⟨f', ⟨iso⟩⟩ :=
    (Localization.essSurj_mapArrow L P.isoModSerre).mem_essImage (Arrow.mk f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G : Functor.{v', v'', u', u''} D E
this_1 : Abelian.{v', u'} D := abelian L P
this_2 : PreservesFiniteColimits L
h : PreservesFiniteColimits (L ⋙ G)
this : G.Additive
x x_1 : D
f : x ⟶ x_1
f' : Arrow.{v, u} C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
⊢ PreservesColimit (parallelPair f 0) G
have this₁ : PreservesColimit (parallelPair (L.map f'.hom) 0) G
Tactic: have : PreservesColimit (parallelPair (L.map f'.hom) 0) G :=
    preservesColimit_of_preserves_colimit_cocone
      (CokernelCofork.isColimitMapCoconeEquiv _ _
        (isColimitOfPreserves L (cokernelIsCokernel f'.hom)))
          ((CokernelCofork.isColimitMapCoconeEquiv _ G).symm
            (CokernelCofork.isColimitMapCoconeEquiv _ (L ⋙ G)
              (isColimitOfPreserves (L ⋙ G) (cokernelIsCokernel f'.hom))))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
G_1 : Functor.{v', v'', u', u''} D E
G : ExactFunctor.{v', v'', u', u''} D E
⊢ exactFunctor C E (Functor.obj (ι (exactFunctor D E) ⋙ Functor.obj (Functor.whiskeringLeft C D E) L) G)
have dsimp : exactFunctor C E (L ⋙ G.obj (P := exactFunctor D E))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
⊢ Eq (α := ObjectProperty (ExactFunctor.{v, v'', u, u''} C E)) (Functor.essImage (whiskeringLeft L P E))
    fun (G : ExactFunctor.{v, v'', u, u''} C E) ↦ P.isoModSerre.IsInvertedBy (G.obj (P := exactFunctor C E))
have h : ∀ (F : ExactFunctor.{v, v'', u, u''} C E),
  Functor.essImage (whiskeringLeft L P E) F ↔ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
Tactic: ext F
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
⊢ Functor.essImage (whiskeringLeft L P E) F ↔ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
have h : Functor.essImage (whiskeringLeft L P E) F → P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
Tactic: refine ⟨?_, fun 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
h : Functor.essImage (whiskeringLeft L P E) F → P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ Functor.essImage (whiskeringLeft L P E) F ↔ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
have h₁ : ∀ (hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))), Functor.essImage (whiskeringLeft L P E) F
Tactic: refine ⟨?_, fun 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
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
G : ExactFunctor.{v', v'', u', u''} D E
e : Functor.obj (whiskeringLeft L P E) G ≅ F
⊢ P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
have h : P.isoModSerre.IsInvertedBy (L ⋙ G.obj (P := exactFunctor D E))
Tactic: rw [← MorphismProperty.IsInvertedBy.iff_of_iso _
      (show L ⋙ G.obj ≅ F.obj from (ObjectProperty.ι _).mapIso e)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ Functor.essImage (whiskeringLeft L P E) F
have h : exactFunctor D E (Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)
Tactic: refine ⟨⟨Localization.lift F.obj hF L, ?_⟩,
      ⟨ObjectProperty.isoMk _ (Localization.fac F.obj hF L)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
inst_6 : L.IsLocalization P.isoModSerre
inst_7 : Preadditive.{v', u'} D
inst_8 : L.Additive
F : ExactFunctor.{v, v'', u, u''} C E
hF : P.isoModSerre.IsInvertedBy (F.obj (P := exactFunctor C E))
⊢ exactFunctor D E (Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)
have h : exactFunctor C E (L ⋙ Localization.lift (W := P.isoModSerre) (F.obj (P := exactFunctor C E)) hF L)
Tactic: rw [← exactFunctor_comp_iff L P]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Mono f
⊢ P.isoModSerre f ↔ P.epiModSerre f
have this : P.monoModSerre f
Tactic: have := P.monoModSerre_of_mono f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Mono f
this : P.monoModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
have mp : P.monoModSerre f ∧ P.epiModSerre f → P.epiModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Mono f
this : P.monoModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
have mpr : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Mono f
this : P.monoModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.epiModSerre f
mpr : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
have mp₁ : P.monoModSerre f → P.epiModSerre f → P.epiModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Mono f
this : P.monoModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.epiModSerre f
mpr : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mp₁ mp₂ mp₃ : P.monoModSerre f → P.epiModSerre f → P.epiModSerre f
mpr₁ mpr₂ : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
have mpr₃ : P.epiModSerre f → P.monoModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Mono f
this : P.monoModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.epiModSerre f
mpr : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mp₁ mp₂ mp₃ : P.monoModSerre f → P.epiModSerre f → P.epiModSerre f
mpr₁ mpr₂ : P.epiModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mpr₃ : P.epiModSerre f → P.monoModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
have mpr₄ : P.epiModSerre f → P.epiModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Epi f
⊢ P.isoModSerre f ↔ P.monoModSerre f
have this : P.epiModSerre f
Tactic: have := P.epiModSerre_of_epi f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Epi f
this : P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
have mp : P.monoModSerre f ∧ P.epiModSerre f → P.monoModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Epi f
this : P.epiModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.monoModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
have mpr : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Epi f
this : P.epiModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.monoModSerre f
mpr : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
have mp₁ : P.monoModSerre f → P.epiModSerre f → P.monoModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Epi f
this : P.epiModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.monoModSerre f
mpr : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mp₁ mp₂ mp₃ : P.monoModSerre f → P.epiModSerre f → P.monoModSerre f
mpr₁ mpr₂ : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
have mpr₃ : P.monoModSerre f → P.monoModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst_3 : Epi f
this : P.epiModSerre f
mp : P.monoModSerre f ∧ P.epiModSerre f → P.monoModSerre f
mpr : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mp₁ mp₂ mp₃ : P.monoModSerre f → P.epiModSerre f → P.monoModSerre f
mpr₁ mpr₂ : P.monoModSerre f → P.monoModSerre f ∧ P.epiModSerre f
mpr₃ : P.monoModSerre f → P.monoModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
have mpr₄ : P.monoModSerre f → P.epiModSerre f
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (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
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
hX : P X
f : 0 ⟶ X := 0
⊢ F.kernel X
have this : IsIso (F.map f)
Tactic: have := hF _ ((P.isoModSerre_iff_of_mono f).2
    ((P.prop_iff_of_iso cokernelZeroIsoTarget).2 hX))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (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
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
⊢ P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel
have refine : ∀ (hF : P ≤ F.kernel) (X Y : C) (f : X ⟶ Y),
  P.isoModSerre f → ∀ (h₁ : P.monoModSerre f) (h₂ : P.epiModSerre f), IsIso (F.map f)
Tactic: refine ⟨P.le_kernel_of_isoModSerre_isInvertedBy F, fun hF X Y f ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (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
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
h : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
⊢ IsIso (F.map f)
have this : Mono (F.map f)
Tactic: have : Mono (F.map f) :=
    (((ShortComplex.mk _ _ (kernel.condition f)).exact_of_f_is_kernel
      (kernelIsKernel f)).map F).mono_g (((hF _ h₁).eq_of_src _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty (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
inst_3 : Abelian.{v', u'} D
P : ObjectProperty.{v, u} C
inst_4 : P.IsSerreClass
F : Functor.{v, v', u, u'} C D
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
h : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
this : Mono (F.map f)
⊢ IsIso (F.map f)
have this₁ : Epi (F.map f)
Tactic: have : Epi (F.map f) :=
    (((ShortComplex.mk _ _ (cokernel.condition f)).exact_of_g_is_cokernel
      (cokernelIsCokernel f)).map F).epi_f (((hF _ h₂).eq_of_tgt _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ Subobject.{v, u} X ≃o (Subobject.{v, u} (op X))ᵒᵈ
have refine_1 : Eq (α := (Subobject.{v, u} (op X))ᵒᵈ →o (Subobject.{v, u} (op X))ᵒᵈ)
  (OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) OrderHom.id
Tactic: refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
refine_1 :
  Eq (α := (Subobject.{v, u} (op X))ᵒᵈ →o (Subobject.{v, u} (op X))ᵒᵈ)
    (OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) OrderHom.id
⊢ Subobject.{v, u} X ≃o (Subobject.{v, u} (op X))ᵒᵈ
have refine_2 : Eq (α := Subobject.{v, u} X →o Subobject.{v, u} X) (OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) OrderHom.id
Tactic: refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ →o (Subobject.{v, u} (op X))ᵒᵈ)
    (OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) OrderHom.id
have refine_1 : ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst_2 : Mono f],
  Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X) : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ)
        (Subobject.mk f) :
      (Subobject.{v, u} (op X))ᵒᵈ)
    ((OrderHom.id : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ) (Subobject.mk f) : (Subobject.{v, u} (op X))ᵒᵈ)
Tactic: refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X) : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ)
        (Subobject.mk f) :
      (Subobject.{v, u} (op X))ᵒᵈ)
    ((OrderHom.id : (a : (Subobject (op X))ᵒᵈ) → (Subobject (op X))ᵒᵈ) (Subobject.mk f) : (Subobject.{v, u} (op X))ᵒᵈ)
have refine_1 : Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
    (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
  Subobject.mk f
Tactic: dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk,
      cokernelOrderHom_coe, OrderHom.id_coe, id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f
have refine_1 : op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A
Tactic: refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 : op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f
have refine_1₁ : A ⟶ op (cokernel (X := kernel f.unop) (kernel.ι f.unop))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 : op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A
refine_1₁ : A ⟶ op (cokernel (X := kernel f.unop) (kernel.ι f.unop))
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f
have refine_1₂ : Eq.{v + 1} (α :=
  unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))) ⟶
    unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
  (Quiver.Hom.unop
    (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) sorry) ≫
      Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop sorry)))
  (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 : op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A
refine_1₁ : A ⟶ op (cokernel (X := kernel f.unop) (kernel.ι f.unop))
refine_1₂ :
  Eq.{v + 1} (α :=
    unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))) ⟶
      unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
        Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯)))
    (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))))
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f
have refine_1₃ : Eq.{v + 1} (α := unop A ⟶ unop A)
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop sorry))
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) sorry))))
  (Quiver.Hom.unop (𝟙 A))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_