awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
hS : S.Exact
⊢ Epi h.f'

Tactic:
exact hS.epi_f' h

Premises used: CategoryTheory.ShortComplex.Exact.epi_f'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
h_1 : Epi h.f'
⊢ S.Exact

Tactic:
simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_epi h.π, ← cancel_epi h.f',
      comp_id, h.f'_π, comp_zero]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.f'_π, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
mp : S.Exact → Mono h.g'
mpr : Mono h.g' → S.Exact
⊢ S.Exact ↔ Mono h.g'

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
hS : S.Exact
⊢ Mono h.g'

Tactic:
hS.mono_g' h

Premises used: CategoryTheory.ShortComplex.Exact.mono_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
hS : S.Exact
⊢ Mono h.g'

Tactic:
exact hS.mono_g' h

Premises used: CategoryTheory.ShortComplex.Exact.mono_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
h_1 : Mono h.g'
⊢ S.Exact

Tactic:
simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_mono h.ι, ← cancel_mono h.g',
      id_comp, h.ι_g', zero_comp]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ι_g', CategoryTheory.ShortComplex.RightHomologyData.exact_iff, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
⊢ Iso.hom (Iso.refl kf.pt) ≫ Fork.ι (KernelFork.ofι (Fork.ι kf) ⋯) = Fork.ι kf

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
⊢ S.HasHomology

Tactic:
have := hS.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ Epi (X := (KernelFork.ofι S.f ⋯).pt) ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))

Tactic:
((MorphismProperty.epimorphisms C).arrow_mk_iso_iff ?_).1
      hS.epi_toCycles

Premises used: CategoryTheory.ShortComplex.Exact.epi_toCycles, CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
refine :
  Arrow.mk (Y := S.cycles) S.toCycles ≅
    Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
      ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
⊢ Epi (X := (KernelFork.ofι S.f ⋯).pt) ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))

Tactic:
refine ((MorphismProperty.epimorphisms C).arrow_mk_iso_iff ?_).1
      hS.epi_toCycles

Premises used: CategoryTheory.ShortComplex.Exact.epi_toCycles, CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
refine :
  Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
      (Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
          ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom =
    (Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)
⊢ Arrow.mk (Y := S.cycles) S.toCycles ≅
    Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
      ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))

Tactic:
refine Arrow.isoMk (Iso.refl _)
      (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
apply :
  (Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
        (Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
            ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom) ≫
      Fork.ι kf =
    ((Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)) ≫
      Fork.ι kf
⊢ Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
      (Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
          ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom =
    (Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)

Tactic:
apply Fork.IsLimit.hom_ext hkf

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ (Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
        (Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
            ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom) ≫
      Fork.ι kf =
    ((Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)) ≫
      Fork.ι kf

Tactic:
simp [IsLimit.conePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ Cofork.π cc ≫ Iso.hom (Iso.refl cc.pt) = Cofork.π (CokernelCofork.ofπ (Cofork.π cc) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ S.HasHomology

Tactic:
have := hS.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Mono (Y := (CokernelCofork.ofπ S.g ⋯).pt)
    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))

Tactic:
((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
      hS.mono_fromOpcycles

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.monomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ShortComplex.Exact.mono_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
refine :
  Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
      ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) ≅
    Arrow.mk (X := S.opcycles) S.fromOpcycles
⊢ Mono (Y := (CokernelCofork.ofπ S.g ⋯).pt)
    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))

Tactic:
refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
      hS.mono_fromOpcycles

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.monomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ShortComplex.Exact.mono_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
refine :
  Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
    (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
          ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
      Iso.hom
        (Iso.refl
          (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
              ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right)
⊢ Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
      ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) ≅
    Arrow.mk (X := S.opcycles) S.fromOpcycles

Tactic:
refine Arrow.isoMk (IsColimit.coconePointUniqueUpToIso hcc S.opcyclesIsCokernel)
      (Iso.refl _) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
apply :
  Cofork.π cc ≫
      Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
    Cofork.π cc ≫
      (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
            ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
        Iso.hom
          (Iso.refl
            (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
                ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right)
⊢ Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
    (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
          ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
      Iso.hom
        (Iso.refl
          (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
              ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right)

Tactic:
apply Cofork.IsColimit.hom_ext hcc

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Cofork.π cc ≫
      Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
    Cofork.π cc ≫
      (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
            ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
        Iso.hom
          (Iso.refl
            (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
                ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right)

Tactic:
simp [IsColimit.coconePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
⊢ S.Exact ↔ Epi (Y := S.cycles) S.toCycles

Tactic:
S.leftHomologyData.exact_iff_epi_f'

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f', CategoryTheory.ShortComplex.cycles, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
⊢ S.Exact ↔ Mono (X := S.opcycles) S.fromOpcycles

Tactic:
S.rightHomologyData.exact_iff_mono_g'

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.RightHomologyData.exact_iff_mono_g', CategoryTheory.ShortComplex.fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
rw : Epi (Y := S.cycles) S.toCycles ↔ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ S.Exact ↔ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
rw [exact_iff_epi_toCycles]

Premises used: CategoryTheory.ShortComplex.exact_iff_epi_toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
apply : Arrow.mk (Y := S.cycles) S.toCycles ≅ Arrow.mk (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ Epi (Y := S.cycles) S.toCycles ↔ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff

Premises used: CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
⊢ Arrow.mk (Y := S.cycles) S.toCycles ≅ Arrow.mk (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
exact Arrow.isoMk (Iso.refl _) S.cyclesIsoKernel (by cat_disch)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
rw : Mono (X := S.opcycles) S.fromOpcycles ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
⊢ S.Exact ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
rw [exact_iff_mono_fromOpcycles]

Premises used: CategoryTheory.ShortComplex.exact_iff_mono_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
⊢ Mono (X := S.opcycles) S.fromOpcycles ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
(MorphismProperty.monomorphisms C).arrow_mk_iso_iff (Iso.symm ?_)

Premises used: CategoryTheory.MorphismProperty.monomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
refine : Arrow.mk (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) ≅ Arrow.mk (X := S.opcycles) S.fromOpcycles
⊢ Mono (X := S.opcycles) S.fromOpcycles ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
refine (MorphismProperty.monomorphisms C).arrow_mk_iso_iff (Iso.symm ?_)

Premises used: CategoryTheory.MorphismProperty.monomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
⊢ Arrow.mk (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) ≅ Arrow.mk (X := S.opcycles) S.fromOpcycles

Tactic:
exact Arrow.isoMk S.opcyclesIsoCokernel.symm (Iso.refl _) (by cat_disch)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
hS : S.Exact
⊢ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
S.exact_iff_mono_cokernel_desc.1 hS

Premises used: CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc, Iff.mp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
hS : S.Exact
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
S.exact_iff_epi_kernel_lift.1 hS

Premises used: Iff.mp, CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : QuasiIso φ
simp : IsZero.{v_1, u_1} S₁.homology ↔ IsZero.{v_1, u_1} S₂.homology
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
simp only [exact_iff_isZero_homology]

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : QuasiIso φ
⊢ IsZero.{v_1, u_1} S₁.homology ↔ IsZero.{v_1, u_1} S₂.homology

Tactic:
Iso.isZero_iff (asIso (homologyMap φ))

Premises used: CategoryTheory.Iso.isZero_iff, CategoryTheory.ShortComplex.homologyMap, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : QuasiIso φ
⊢ IsZero.{v_1, u_1} S₁.homology ↔ IsZero.{v_1, u_1} S₂.homology

Tactic:
exact Iso.isZero_iff (asIso (homologyMap φ))

Premises used: CategoryTheory.Iso.isZero_iff, CategoryTheory.ShortComplex.homologyMap, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
rw : Epi (Y := S.cycles) S.toCycles
⊢ S.Exact

Tactic:
rw [exact_iff_epi_toCycles]

Premises used: CategoryTheory.ShortComplex.exact_iff_epi_toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
rw :
  Eq (α := S.cycles ⟶ S.X₂) (hS.lift (KernelFork.ofι (Z := S.cycles) S.iCycles ⋯) ≫ S.f : S.cycles ⟶ S.X₂)
    (S.iCycles : S.cycles ⟶ S.X₂)
⊢ Eq (α := S.cycles ⟶ S.cycles)
    (hS.lift (KernelFork.ofι (Z := S.cycles) S.iCycles ⋯) ≫ S.toCycles : S.cycles ⟶ S.cycles)
    (𝟙 S.cycles : S.cycles ⟶ S.cycles)

Tactic:
rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.toCycles_i, CategoryTheory.ShortComplex.iCycles, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.X₂) (hS.lift (KernelFork.ofι (Z := S.cycles) S.iCycles ⋯) ≫ S.f : S.cycles ⟶ S.X₂)
    (S.iCycles : S.cycles ⟶ S.X₂)

Tactic:
Fork.IsLimit.lift_ι hS

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.Limits.Fork.ι, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.X₂) (hS.lift (KernelFork.ofι (Z := S.cycles) S.iCycles ⋯) ≫ S.f : S.cycles ⟶ S.X₂)
    (S.iCycles : S.cycles ⟶ S.X₂)

Tactic:
exact Fork.IsLimit.lift_ι hS

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift_ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
⊢ IsSplitEpi (Y := S.cycles) S.toCycles

Tactic:
have : IsSplitEpi S.toCycles :=
    ⟨⟨{ section_ := hS.lift (KernelFork.ofι S.iCycles S.iCycles_g)
        id := by
          rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]
          exact Fork.IsLimit.lift_ι hS }⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
this : IsSplitEpi (Y := S.cycles) S.toCycles
⊢ Epi (Y := S.cycles) S.toCycles

Tactic:
infer_instance