awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
⊢ Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0

Tactic:
rw [S.rightHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h

Premises used: CategoryTheory.ShortComplex.RightHomologyData.exact_iff, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.rightHomologyData.H ⟶ S.rightHomologyData.H) (𝟙 S.rightHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.rightHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (𝟙 (F.obj S.rightHomologyData.H)) 0
rw₂ : F.map (𝟙 S.rightHomologyData.H) = 0
rw₃ : Eq (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) (F.map 0) 0
rw₄ rw₅ : Eq.{v_2 + 1} (α := F.obj S.rightHomologyData.H ⟶ F.obj S.rightHomologyData.H) 0 0
⊢ Exact (S.map F)

Tactic:
rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.Functor.map_id, CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : F.PreservesRightHomologyOf S
⊢ S.HasHomology

Tactic:
have := h.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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : F.PreservesRightHomologyOf S
this : S.HasHomology
⊢ Exact (S.map F)

Tactic:
h.map_of_preservesLeftHomologyOf F

Premises used: CategoryTheory.ShortComplex.Exact.map_of_preservesLeftHomologyOf
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : F.PreservesRightHomologyOf S
this : S.HasHomology
⊢ Exact (S.map F)

Tactic:
exact h.map_of_preservesLeftHomologyOf F

Premises used: CategoryTheory.ShortComplex.Exact.map_of_preservesLeftHomologyOf
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
mp : Exact (S.map F) → S.Exact
mpr : S.Exact → Exact (S.map F)
⊢ Exact (S.map F) ↔ S.Exact

Tactic:
constructor
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Exact (S.map F)
mp : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
⊢ S.Exact

Tactic:
rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Exact (S.map F)
⊢ Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0

Tactic:
rw [(S.leftHomologyData.map F).exact_iff, IsZero.iff_id_eq_zero,
      LeftHomologyData.map_H] at h

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.map, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.ShortComplex.LeftHomologyData.map_H
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
mp : F.map (𝟙 S.leftHomologyData.H) = F.map 0
⊢ Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
mp : 𝟙 (F.obj S.leftHomologyData.H) = F.map 0
mp₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
mp₂ mp₃ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) 0 0
⊢ F.map (𝟙 S.leftHomologyData.H) = F.map 0

Tactic:
rw [F.map_id, F.map_zero, h]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_id
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : S.Exact
⊢ Exact (S.map F)

Tactic:
h.map F

Premises used: CategoryTheory.ShortComplex.Exact.map
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : S.HasHomology
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
inst_8 : F.Faithful
h : S.Exact
⊢ Exact (S.map F)

Tactic:
exact h.map F

Premises used: CategoryTheory.ShortComplex.Exact.map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
⊢ S.HasHomology

Tactic:
have := h.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
⊢ S.Exact

Tactic:
have eq := h
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.Exact
⊢ Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0

Tactic:
rw [exact_iff_iCycles_pOpcycles_zero] at eq

Premises used: CategoryTheory.ShortComplex.exact_iff_iCycles_pOpcycles_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0
rw : CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫ b = 0
rw₁ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) S.iCycles ≫
      CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb) =
    0
rw₂ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (S.iCycles ≫ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles b hb)) =
    0
rw₃ :
  CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha)
      (CategoryStruct.comp (Y := S.opcycles) 0 (S.descOpcycles b hb)) =
    0
rw₄ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := S.cycles) (S.liftCycles a ha) 0) 0
rw₅ rw₆ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 0
⊢ a ≫ b = 0

Tactic:
rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
ex : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero.{v_1, u_1} S.X₂

Tactic:
(ShortComplex.HomologyData.ofZeros S hf hg).exact_iff.1 ex

Premises used: CategoryTheory.ShortComplex.HomologyData.exact_iff, CategoryTheory.ShortComplex.HomologyData.ofZeros, 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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
mp : S.Exact → Mono S.g
mpr : Mono S.g → S.Exact
⊢ S.Exact ↔ Mono S.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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : S.Exact
⊢ S.HasHomology

Tactic:
have := h.hasHomology
-- 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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : S.Exact
this : S.HasHomology
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
simp only [exact_iff_isZero_homology] at h

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 : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
⊢ IsIso (Y := S.opcycles) S.pOpcycles

Tactic:
have := S.isIso_pOpcycles hf
-- 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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this : IsIso (Y := S.opcycles) S.pOpcycles
⊢ Mono (X := S.opcycles) S.fromOpcycles

Tactic:
have := mono_of_isZero_kernel' _ S.homologyIsKernel h
-- 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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this_2 : IsIso (Y := S.opcycles) S.pOpcycles
this : Mono (X := S.opcycles) S.fromOpcycles
mp : Mono (CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles)
⊢ Mono S.g

Tactic:
rw [← S.p_fromOpcycles]

Premises used: CategoryTheory.ShortComplex.p_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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this_2 : IsIso (Y := S.opcycles) S.pOpcycles
this : Mono (X := S.opcycles) S.fromOpcycles
⊢ Mono (CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_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
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : Mono S.g
mpr :
  IsZero.{v_1, u_1}
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι (Z := 0) 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (Z := 0) 0 ⋯) ⋯ ⋯)).left.H
⊢ S.Exact

Tactic:
rw [(HomologyData.ofIsLimitKernelFork S hf _
      (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
        inferInstance (isZero_zero C))).exact_iff]

Premises used: CategoryTheory.ShortComplex.HomologyData.exact_iff, CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.isZero_zero, inferInstance, CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero, OfNat.ofNat
-- 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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : Mono S.g
⊢ IsZero.{v_1, u_1}
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι (Z := 0) 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (Z := 0) 0 ⋯) ⋯ ⋯)).left.H

Tactic:
isZero_zero C

Premises used: CategoryTheory.Limits.isZero_zero
-- 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 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : Mono S.g
⊢ IsZero.{v_1, u_1}
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι (Z := 0) 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (Z := 0) 0 ⋯) ⋯ ⋯)).left.H

Tactic:
exact isZero_zero C

Premises used: CategoryTheory.Limits.isZero_zero
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
mp : S.Exact → Epi S.f
mpr : Epi S.f → S.Exact
⊢ S.Exact ↔ Epi S.f

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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : S.Exact
⊢ S.HasHomology

Tactic:
have := h.hasHomology
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : S.Exact
this : S.HasHomology
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
simp only [exact_iff_isZero_homology] at h

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 : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
⊢ IsIso (X := S.cycles) S.iCycles

Tactic:
haveI := S.isIso_iCycles hg
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this : IsIso (X := S.cycles) S.iCycles
⊢ Epi (Y := S.cycles) S.toCycles

Tactic:
haveI : Epi S.toCycles := epi_of_isZero_cokernel' _ S.homologyIsCokernel h
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this_2 : IsIso (X := S.cycles) S.iCycles
this : Epi (Y := S.cycles) S.toCycles
mp : Epi (CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles)
⊢ Epi S.f

Tactic:
rw [← S.toCycles_i]

Premises used: CategoryTheory.ShortComplex.toCycles_i
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this_2 : IsIso (X := S.cycles) S.iCycles
this : Epi (Y := S.cycles) S.toCycles
⊢ Epi (CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_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
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : Epi S.f
mpr :
  IsZero.{v_1, u_1}
    (HomologyData.ofIsColimitCokernelCofork S hg (CokernelCofork.ofπ (Z := 0) 0 ⋯)
          (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⋯ ⋯)).left.H
⊢ S.Exact

Tactic:
rw [(HomologyData.ofIsColimitCokernelCofork S hg _
      (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (0 : S.X₂ ⟶ 0) comp_zero)
        inferInstance (isZero_zero C))).exact_iff]

Premises used: CategoryTheory.ShortComplex.HomologyData.exact_iff, CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.comp_zero, inferInstance, CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork, CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero, OfNat.ofNat, CategoryTheory.Limits.CokernelCofork.ofπ
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : Epi S.f
⊢ IsZero.{v_1, u_1}
    (HomologyData.ofIsColimitCokernelCofork S hg (CokernelCofork.ofπ (Z := 0) 0 ⋯)
          (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⋯ ⋯)).left.H

Tactic:
isZero_zero C

Premises used: CategoryTheory.Limits.isZero_zero
-- 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 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : Epi S.f
⊢ IsZero.{v_1, u_1}
    (HomologyData.ofIsColimitCokernelCofork S hg (CokernelCofork.ofπ (Z := 0) 0 ⋯)
          (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⋯ ⋯)).left.H

Tactic:
exact isZero_zero C

Premises used: CategoryTheory.Limits.isZero_zero
-- 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 : S.Exact
h : S.LeftHomologyData
⊢ S.HasHomology

Tactic:
haveI := hS.hasHomology
-- 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 : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
dsimp : IsZero.{v_1, u_1} h.H
⊢ IsZero.{v_1, u_1} (CokernelCofork.ofπ h.π ⋯).pt

Tactic:
dsimp
-- 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 : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
⊢ IsZero.{v_1, u_1} h.H

Tactic:
simpa only [← h.exact_iff] using hS

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.exact_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
hS : S.Exact
h : S.RightHomologyData
⊢ S.HasHomology

Tactic:
haveI := hS.hasHomology
-- 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 : S.Exact
h : S.RightHomologyData
this : S.HasHomology
dsimp : IsZero.{v_1, u_1} h.H
⊢ IsZero.{v_1, u_1} (KernelFork.ofι h.ι ⋯).pt

Tactic:
dsimp
-- 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 : S.Exact
h : S.RightHomologyData
this : S.HasHomology
⊢ IsZero.{v_1, u_1} h.H

Tactic:
simpa only [← h.exact_iff] using hS

Premises used: CategoryTheory.ShortComplex.RightHomologyData.exact_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
hS : S.Exact
inst_2 : S.HasLeftHomology
⊢ Epi (Y := S.cycles) S.toCycles

Tactic:
hS.epi_f' _

Premises used: CategoryTheory.ShortComplex.Exact.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
hS : S.Exact
inst_2 : S.HasRightHomology
⊢ Mono (X := S.opcycles) S.fromOpcycles

Tactic:
hS.mono_g' _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.Exact.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
h : S.LeftHomologyData
mp : S.Exact → Epi h.f'
mpr : Epi h.f' → S.Exact
⊢ S.Exact ↔ Epi h.f'

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.LeftHomologyData
hS : S.Exact
⊢ Epi h.f'

Tactic:
hS.epi_f' h

Premises used: CategoryTheory.ShortComplex.Exact.epi_f'