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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.HomologyData
⊢ S.HasHomology

Tactic:
haveI := HasHomology.mk' 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.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.left.H

Tactic:
LeftHomologyData.exact_iff h.left

Premises used: CategoryTheory.ShortComplex.HomologyData.left, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.left.H

Tactic:
exact LeftHomologyData.exact_iff h.left

Premises used: CategoryTheory.ShortComplex.HomologyData.left, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.right.H

Tactic:
RightHomologyData.exact_iff h.right

Premises used: CategoryTheory.ShortComplex.RightHomologyData.exact_iff, CategoryTheory.ShortComplex.HomologyData.right
-- 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.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.right.H

Tactic:
exact RightHomologyData.exact_iff h.right

Premises used: CategoryTheory.ShortComplex.RightHomologyData.exact_iff, CategoryTheory.ShortComplex.HomologyData.right
-- 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
inst_2 : S.HasHomology
inst_3 : HasZeroObject.{v_1, u_1} C
rw : IsZero.{v_1, u_1} S.homology ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)
⊢ S.Exact ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)

Tactic:
rw [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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasZeroObject.{v_1, u_1} C
mp : IsZero.{v_1, u_1} S.homology → Nonempty.{v_1 + 1} (S.homology ≅ 0)
mpr : Nonempty.{v_1 + 1} (S.homology ≅ 0) → IsZero.{v_1, u_1} S.homology
⊢ IsZero.{v_1, u_1} S.homology ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)

Tactic:
constructor
-- 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
inst_2 : S.HasHomology
inst_3 : HasZeroObject.{v_1, u_1} C
h : IsZero.{v_1, u_1} S.homology
⊢ Nonempty.{v_1 + 1} (S.homology ≅ 0)

Tactic:
⟨h.isoZero⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.IsZero.isoZero
-- 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
inst_2 : S.HasHomology
inst_3 : HasZeroObject.{v_1, u_1} C
h : IsZero.{v_1, u_1} S.homology
⊢ Nonempty.{v_1 + 1} (S.homology ≅ 0)

Tactic:
exact ⟨h.isoZero⟩
-- 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
inst_2 : S.HasHomology
inst_3 : HasZeroObject.{v_1, u_1} C
e : S.homology ≅ 0
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
IsZero.of_iso (isZero_zero C) e

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso
-- 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
inst_2 : S.HasHomology
inst_3 : HasZeroObject.{v_1, u_1} C
e : S.homology ≅ 0
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
exact IsZero.of_iso (isZero_zero C) e

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.Exact
obtain : ∀ (h : S₁.HomologyData) (z : IsZero.{v_1, u_1} h.left.H), S₂.Exact
⊢ S₂.Exact

Tactic:
obtain ⟨⟨h, z⟩⟩ := 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.HomologyData
z : IsZero.{v_1, u_1} h.left.H
⊢ S₂.Exact

Tactic:
⟨⟨HomologyData.ofIso e h, z⟩⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, CategoryTheory.ShortComplex.HomologyData.ofIso, Exists.intro
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.HomologyData
z : IsZero.{v_1, u_1} h.left.H
⊢ S₂.Exact

Tactic:
exact ⟨⟨HomologyData.ofIso e h, z⟩⟩
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
⟨exact_of_iso e, exact_of_iso e.symm⟩

Premises used: CategoryTheory.ShortComplex.exact_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
⊢ Mono S₁.f ↔ Mono S₂.f

Tactic:
have : Mono S₁.f ↔ Mono S₂.f :=
    (MorphismProperty.monomorphisms C).arrow_mk_iso_iff
      (Arrow.isoMk (ShortComplex.π₁.mapIso e) (ShortComplex.π₂.mapIso e) e.hom.comm₁₂)
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
this : Mono S₁.f ↔ Mono S₂.f
rw : S₂.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
rw₁ rw₂ : S₂.Exact ∧ Mono S₂.f ↔ S₂.Exact ∧ Mono S₂.f
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

Tactic:
rw [exact_iff_of_iso e, this]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_iso
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
⊢ Epi S₁.g ↔ Epi S₂.g

Tactic:
have : Epi S₁.g ↔ Epi S₂.g :=
    (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
      (Arrow.isoMk (ShortComplex.π₂.mapIso e) (ShortComplex.π₃.mapIso e) e.hom.comm₂₃)
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
this : Epi S₁.g ↔ Epi S₂.g
rw : S₂.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
rw₁ rw₂ : S₂.Exact ∧ Epi S₂.g ↔ S₂.Exact ∧ Epi S₂.g
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g

Tactic:
rw [exact_iff_of_iso e, this]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_iso
-- 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 : IsZero.{v_1, u_1} S.X₂
rw : IsZero.{v_1, u_1} (HomologyData.ofZeros S ⋯ ⋯).left.H
⊢ S.Exact

Tactic:
rw [(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff]

Premises used: CategoryTheory.ShortComplex.HomologyData.exact_iff, CategoryTheory.ShortComplex.HomologyData.ofZeros, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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 : IsZero.{v_1, u_1} S.X₂
⊢ IsZero.{v_1, u_1} (HomologyData.ofZeros S ⋯ ⋯).left.H

Tactic:
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 : IsZero.{v_1, u_1} S.X₂
⊢ IsZero.{v_1, u_1} (HomologyData.ofZeros S ⋯ ⋯).left.H

Tactic:
exact 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
mp : S₁.Exact → S₂.Exact
mpr : S₂.Exact → S₁.Exact
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
constructor
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₁ : S₁.HomologyData
z₁ : IsZero.{v_1, u_1} h₁.left.H
⊢ S₂.Exact

Tactic:
⟨HomologyData.ofEpiOfIsIsoOfMono φ h₁, z₁⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono, Exists.intro
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₁ : S₁.HomologyData
z₁ : IsZero.{v_1, u_1} h₁.left.H
⊢ S₂.Exact

Tactic:
exact ⟨HomologyData.ofEpiOfIsIsoOfMono φ h₁, z₁⟩
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂ : S₂.HomologyData
z₂ : IsZero.{v_1, u_1} h₂.left.H
⊢ S₁.Exact

Tactic:
⟨HomologyData.ofEpiOfIsIsoOfMono' φ h₂, z₂⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono', Exists.intro
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂ : S₂.HomologyData
z₂ : IsZero.{v_1, u_1} h₂.left.H
⊢ S₁.Exact

Tactic:
exact ⟨HomologyData.ofEpiOfIsIsoOfMono' φ h₂, z₂⟩
-- 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.HomologyData
this : S.HasHomology
rw : IsZero.{v_1, u_1} h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0

Tactic:
rw [h.left.exact_iff, ← h.comm]

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff, CategoryTheory.ShortComplex.HomologyData.comm
-- 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.HomologyData
this : S.HasHomology
mp : IsZero.{v_1, u_1} h.left.H → h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
mpr : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero.{v_1, u_1} h.left.H
⊢ IsZero.{v_1, u_1} h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Tactic:
constructor
-- 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.HomologyData
this : S.HasHomology
z : IsZero.{v_1, u_1} h.left.H
mp : h.left.π ≫ 0 ≫ h.right.ι = 0
mp₁ : Eq (α := h.left.K ⟶ h.right.Q) (h.left.π ≫ 0) 0
mp₂ mp₃ : Eq.{v_1 + 1} (α := h.left.K ⟶ h.right.Q) 0 0
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Tactic:
rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]

Premises used: CategoryTheory.ShortComplex.HomologyData.iso, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.zero_comp, OfNat.ofNat, CategoryTheory.Iso.hom
-- 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.HomologyData
this : S.HasHomology
eq : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ IsZero.{v_1, u_1} h.left.H

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_mono h.iso.hom, id_comp, ← cancel_mono h.right.ι,
      ← cancel_epi h.left.π, eq, zero_comp, comp_zero]

Premises used: CategoryTheory.ShortComplex.HomologyData.iso, CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.ShortComplex.HomologyData.right, CategoryTheory.Category.id_comp
-- 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
inst_2 : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ S.Exact ↔ h₁.i ≫ h₂.p = 0

Tactic:
(HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).exact_iff_i_p_zero

Premises used: CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison', CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_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
inst_2 : S.HasHomology
⊢ S.Exact ↔ Eq (α := S.cycles ⟶ S.opcycles) (S.iCycles ≫ S.pOpcycles) 0

Tactic:
S.exact_iff_i_p_zero _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.exact_iff_i_p_zero, 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 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
inst_4 : HasCokernel S.f
⊢ HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
haveI := HasLeftHomology.hasCokernel S
-- 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
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
inst_4 : HasCokernel S.f
this : HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
haveI := HasRightHomology.hasKernel S
-- 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
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
inst_4 : HasCokernel S.f
this_1 : HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
this : HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
⊢ S.Exact ↔ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
S.exact_iff_i_p_zero (LeftHomologyData.ofHasKernelOfHasCokernel S)
    (RightHomologyData.ofHasCokernelOfHasKernel S)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel, CategoryTheory.Limits.colimit, CategoryTheory.ShortComplex.exact_iff_i_p_zero, CategoryTheory.Limits.limit, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel, CategoryTheory.Limits.colimit.ι
-- 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
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
inst_4 : HasCokernel S.f
this_1 : HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
this : HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
⊢ S.Exact ↔ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
exact S.exact_iff_i_p_zero (LeftHomologyData.ofHasKernelOfHasCokernel S)
    (RightHomologyData.ofHasCokernelOfHasKernel S)

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel, CategoryTheory.ShortComplex.exact_iff_i_p_zero, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel
-- 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
obtain : ∀ (h : S.HomologyData) (z : IsZero.{v_1, u_1} h.left.H), S.op.Exact
⊢ S.op.Exact

Tactic:
obtain ⟨h, z⟩ := 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.HomologyData
z : IsZero.{v_1, u_1} h.left.H
⊢ S.op.Exact

Tactic:
⟨⟨h.op, (IsZero.of_iso z h.iso.symm).op⟩⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, CategoryTheory.Limits.IsZero.op, CategoryTheory.ShortComplex.HomologyData.iso, CategoryTheory.ShortComplex.HomologyData.op, CategoryTheory.Limits.IsZero.of_iso, Exists.intro, CategoryTheory.Iso.symm
-- 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.HomologyData
z : IsZero.{v_1, u_1} h.left.H
⊢ S.op.Exact

Tactic:
exact ⟨⟨h.op, (IsZero.of_iso z h.iso.symm).op⟩⟩
-- 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
obtain : ∀ (h : S.HomologyData) (z : IsZero.{v_1, u_1} h.left.H), S.unop.Exact
⊢ S.unop.Exact

Tactic:
obtain ⟨h, z⟩ := 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.HomologyData
z : IsZero.{v_1, u_1} h.left.H
⊢ S.unop.Exact

Tactic:
⟨⟨h.unop, (IsZero.of_iso z h.iso.symm).unop⟩⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, CategoryTheory.ShortComplex.HomologyData.iso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.ShortComplex.HomologyData.unop, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsZero.unop
-- 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.HomologyData
z : IsZero.{v_1, u_1} h.left.H
⊢ S.unop.Exact

Tactic:
exact ⟨⟨h.unop, (IsZero.of_iso z h.iso.symm).unop⟩⟩
-- 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
⊢ S.op.Exact ↔ S.Exact

Tactic:
⟨Exact.unop, Exact.op⟩

Premises used: CategoryTheory.ShortComplex.Exact.unop, CategoryTheory.ShortComplex.Exact.op, Iff.intro
-- 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ᵒᵖ
⊢ S.unop.Exact ↔ S.Exact

Tactic:
S.unop.exact_op_iff.symm

Premises used: Quiver.Hom.op, CategoryTheory.ShortComplex.exact_op_iff, Quiver.Hom.unop, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.unop, Iff.symm
-- 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.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
inst_6 : HasHomology (S.map F)
⊢ Exact (S.map F) ↔ IsZero.{v_2, u_2} (F.obj h.H)

Tactic:
(h.map F).exact_iff

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.map, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
-- 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.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
inst_6 : HasHomology (S.map F)
⊢ Exact (S.map F) ↔ IsZero.{v_2, u_2} (F.obj h.H)

Tactic:
(h.map F).exact_iff

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map, CategoryTheory.ShortComplex.RightHomologyData.exact_iff
-- 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 : HasHomology (S.map F)
⊢ 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 : HasHomology (S.map F)
this : S.HasHomology
⊢ Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0

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

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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
inst_6 : HasHomology (S.map F)
this : S.HasHomology
h : Eq.{v_1 + 1} (α := S.leftHomologyData.H ⟶ S.leftHomologyData.H) (𝟙 S.leftHomologyData.H) 0
rw : IsZero.{v_2, u_2} (F.obj S.leftHomologyData.H)
rw₁ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (𝟙 (F.obj S.leftHomologyData.H)) 0
rw₂ : F.map (𝟙 S.leftHomologyData.H) = 0
rw₃ : Eq (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) (F.map 0) 0
rw₄ rw₅ : Eq.{v_2 + 1} (α := F.obj S.leftHomologyData.H ⟶ F.obj S.leftHomologyData.H) 0 0
⊢ Exact (S.map F)

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

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.Functor.map_zero, CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff, CategoryTheory.Functor.map_id, 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.PreservesRightHomologyOf S
inst_6 : HasHomology (S.map F)
⊢ S.HasHomology

Tactic:
have : S.HasHomology := h.hasHomology