awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
A : C
k : S.X₂ ⟶ A
inst_2 : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ Eq (α := S.rightHomology ⟶ A) (S.rightHomologyι ≫ S.descOpcycles k ⋯) 0

Tactic:
RightHomologyData.ι_descQ_eq_zero_of_boundary _ k x hx

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.descOpcycles, CategoryTheory.ShortComplex.rightHomologyι, CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
rw rw₁ : S.g = S.g
⊢ S.g = S.g ≫ 𝟙 S.X₃

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
φ : S₁ ⟶ S
inst_3 : S₁.HasRightHomology
rw : φ.τ₁ ≫ S.f ≫ k = 0
rw₁ : Eq (α := S₁.X₁ ⟶ A) (φ.τ₁ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ A) 0 0
⊢ S₁.f ≫ φ.τ₂ ≫ k = 0

Tactic:
rw [← φ.comm₁₂_assoc, hk, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
φ : S₁ ⟶ S
inst_3 : S₁.HasRightHomology
⊢ Eq (α := S₁.opcycles ⟶ A) (CategoryStruct.comp (Y := S.opcycles) (opcyclesMap φ) (S.descOpcycles k hk))
    (S₁.descOpcycles (φ.τ₂ ≫ k) ⋯)

Tactic:
simp only [← cancel_epi (S₁.pOpcycles), p_opcyclesMap_assoc, p_descOpcycles]

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.p_opcyclesMap_assoc, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
⊢ CategoryStruct.comp (Y := S.opcycles) (Iso.inv h.opcyclesIso) (S.descOpcycles k hk) = h.descQ k hk

Tactic:
simp only [← cancel_epi h.p, p_comp_opcyclesIso_inv_assoc, p_descOpcycles, p_descQ]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv_assoc, CategoryTheory.ShortComplex.RightHomologyData.p_descQ, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
rw :
  Eq (α := S.opcycles ⟶ A)
    (Iso.hom h.opcyclesIso ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.inv h.opcyclesIso) (S.descOpcycles k hk))
    (S.descOpcycles k hk)
rw₁ rw₂ : Eq (α := S.opcycles ⟶ A) (S.descOpcycles k hk) (S.descOpcycles k hk)
⊢ Eq (α := S.opcycles ⟶ A) (Iso.hom h.opcyclesIso ≫ h.descQ k hk) (S.descOpcycles k hk)

Tactic:
rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_inv_comp_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
⊢ HasCokernel S.f

Tactic:
⟨⟨⟨_, S.rightHomologyData.hp⟩⟩⟩

Premises used: CategoryTheory.ShortComplex.RightHomologyData.hp, CategoryTheory.ShortComplex.rightHomologyData, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
inst_3 : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
⊢ HasLimit (parallelPair h.g' 0)

Tactic:
haveI : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
inst_3 : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ coequalizer.π S.f 0 ≫
      (parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0).map WalkingParallelPairHom.left ≫
        Iso.hom
          (Iso.refl ((parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) =
    CategoryStruct.comp (Y := coequalizer S.f 0) (coequalizer.π S.f 0)
      (Iso.hom (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp) ≫
        (parallelPair h.g' 0).map WalkingParallelPairHom.left)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
inst_3 : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ (parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) =
    Iso.hom (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp) ≫
      (parallelPair h.g' 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
inst_3 : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
e : parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp)
    (Iso.refl ((parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
hasLimit_of_iso e.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
inst_3 : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
e : parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp)
    (Iso.refl ((parallelPair (X := cokernel S.f) (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)

Tactic:
exact hasLimit_of_iso e.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₂
h₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ IsIso (opcyclesMap' φ h₁ h₂)

Tactic:
⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩

Premises used: CategoryTheory.ShortComplex.Hom.τ₂, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.IsIso.mk, CategoryTheory.ShortComplex.RightHomologyData.descQ, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₂
h₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
refine_1 : S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0
refine_2 : opcyclesMap' φ h₁ h₂ ≫ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ = 𝟙 h₁.Q
refine_3 : h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q
⊢ IsIso (opcyclesMap' φ h₁ h₂)

Tactic:
refine ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₂
h₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0

Tactic:
simp only [← cancel_epi φ.τ₁, comp_zero, φ.comm₁₂_assoc, IsIso.hom_inv_id_assoc, h₁.wp]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.wp, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₂
h₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' φ h₁ h₂ ≫ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ = 𝟙 h₁.Q

Tactic:
simp only [← cancel_epi h₁.p, p_opcyclesMap'_assoc, h₂.p_descQ,
      IsIso.hom_inv_id_assoc, comp_id]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_descQ, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.ShortComplex.p_opcyclesMap'_assoc, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₂
h₂_1 : IsIso φ.τ₂
h₁_1 : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₂.descQ (inv φ.τ₂ ≫ h₁.p) ⋯ ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q

Tactic:
simp only [← cancel_epi h₂.p, h₂.p_descQ_assoc, assoc, p_opcyclesMap',
      IsIso.inv_hom_id_assoc, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.p_opcyclesMap', CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₂
h₂ : IsIso φ.τ₂
h₁ : Epi φ.τ₁
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)

Tactic:
isIso_opcyclesMap'_of_isIso_of_epi φ h₂ h₁ _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : IsIso φ.τ₂
inst_3 : Epi φ.τ₁
inst_4 : S₁.HasRightHomology
inst_5 : S₂.HasRightHomology
⊢ IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)

Tactic:
isIso_opcyclesMap_of_isIso_of_epi' φ inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.isIso_opcyclesMap_of_isIso_of_epi'
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Mono (S₂.f ≫ e.inv.τ₂)
⊢ Mono S₂.f

Tactic:
mono_of_mono _ e.inv.τ₂

Premises used: CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.mono_of_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Mono (S₂.f ≫ e.inv.τ₂)
⊢ Mono S₂.f

Tactic:
exact mono_of_mono _ e.inv.τ₂

Premises used: CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.mono_of_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
suffices : Mono (S₂.f ≫ e.inv.τ₂)
⊢ Mono S₂.f

Tactic:
suffices Mono (S₂.f ≫ e.inv.τ₂) by
      exact mono_of_mono _ e.inv.τ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
⊢ Mono S₁.f

Tactic:
have := h.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Mono S₁.f
rw : Mono (e.inv.τ₁ ≫ S₁.f)
⊢ Mono (S₂.f ≫ e.inv.τ₂)

Tactic:
rw [← e.inv.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Mono S₁.f
⊢ Mono (e.inv.τ₁ ≫ S₁.f)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Epi (e.hom.τ₂ ≫ S₂.g)
⊢ Epi S₂.g

Tactic:
epi_of_epi e.hom.τ₂ _

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Epi (e.hom.τ₂ ≫ S₂.g)
⊢ Epi S₂.g

Tactic:
exact epi_of_epi e.hom.τ₂ _

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
suffices : Epi (e.hom.τ₂ ≫ S₂.g)
⊢ Epi S₂.g

Tactic:
suffices Epi (e.hom.τ₂ ≫ S₂.g) by
      exact epi_of_epi e.hom.τ₂ _
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
⊢ Epi S₁.g

Tactic:
have := h.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Epi S₁.g
rw : Epi (S₁.g ≫ e.hom.τ₃)
⊢ Epi (e.hom.τ₂ ≫ S₂.g)

Tactic:
rw [e.hom.comm₂₃]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
this : Epi S₁.g
⊢ Epi (S₁.g ≫ e.hom.τ₃)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₂
mp : S₁.ShortExact → S₂.ShortExact
mpr : S₂.ShortExact → S₁.ShortExact
⊢ S₁.ShortExact ↔ S₂.ShortExact

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact → S₂.ShortExact

Tactic:
shortExact_of_iso e

Premises used: CategoryTheory.ShortComplex.shortExact_of_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact → S₂.ShortExact

Tactic:
exact shortExact_of_iso e

Premises used: CategoryTheory.ShortComplex.shortExact_of_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₂.ShortExact → S₁.ShortExact

Tactic:
shortExact_of_iso e.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.shortExact_of_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₂.ShortExact → S₁.ShortExact

Tactic:
exact shortExact_of_iso e.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.shortExact_of_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
⊢ Epi S.g

Tactic:
have := h.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
this : Epi S.g
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S.X₃) (Y := Opposite.op S.X₂) S.g.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
⊢ Mono S.f

Tactic:
have := h.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
this : Mono S.f
⊢ Epi.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S.X₂) (Y := Opposite.op S.X₁) S.f.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
⊢ Epi S.g

Tactic:
have := h.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
this : Epi S.g
dsimp : Mono S.g.unop
⊢ Mono S.unop.f

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
this : Epi S.g
⊢ Mono S.g.unop

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
⊢ Mono S.f

Tactic:
have := h.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
this : Mono S.f
dsimp : Epi S.f.unop
⊢ Epi S.unop.g

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
this : Mono S.f
⊢ Epi S.f.unop

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact ↔ S.op.ShortExact

Tactic:
⟨ShortExact.op, ShortExact.unop⟩

Premises used: CategoryTheory.ShortComplex.ShortExact.op, CategoryTheory.ShortComplex.ShortExact.unop, Iff.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact ↔ S.unop.ShortExact

Tactic:
S.unop.shortExact_iff_op.symm

Premises used: CategoryTheory.ShortComplex.shortExact_iff_op, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.unop, Iff.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
this : Mono S.f
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
this_1 : Mono S.f
this : Epi S.g
⊢ ShortExact (S.map F)

Tactic:
hS.map F

Premises used: CategoryTheory.ShortComplex.ShortExact.map
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
this_1 : Mono S.f
this : Epi S.g
⊢ ShortExact (S.map F)

Tactic:
exact hS.map F

Premises used: CategoryTheory.ShortComplex.ShortExact.map
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
inst_2 : Balanced.{v_1, u_1} C
⊢ HasZeroObject.{v_1, u_1} C

Tactic:
have := hS.exact.hasZeroObject
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this : HasZeroObject.{v_1, u_1} C
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this : Mono S.f
⊢ Epi S.g

Tactic:
have := hS.epi_g