awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
⊢ Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0

Tactic:
simp only [← cancel_mono φ.τ₃, zero_comp, assoc, ← fromOpcycles_naturality,
      IsIso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]

Premises used: CategoryTheory.ShortComplex.fromOpcycles_naturality, CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles, CategoryTheory.Limits.zero_comp, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.ShortComplex.Hom.τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
⊢ Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0

Tactic:
have h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0 := by
    simp only [← cancel_mono φ.τ₃, zero_comp, assoc, ← fromOpcycles_naturality,
      IsIso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
have :
  ∀
    (z :
      S₂.homology ⟶
        Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
          (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles))
    (hz :
      Eq (α := S₂.homology ⟶ S₁.opcycles)
        (z ≫ Fork.ι (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯) : S₂.homology ⟶ S₁.opcycles)
        (S₂.homologyι ≫ inv (opcyclesMap φ) : S₂.homology ⟶ S₁.opcycles)),
    IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
have ⟨z, hz⟩ := KernelFork.IsLimit.lift' S₁.homologyIsKernel _ h
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
⟨⟨z, ?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : homologyMap φ ≫ z = 𝟙 S₁.homology
refine_2 : z ≫ homologyMap φ = 𝟙 S₂.homology
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
refine ⟨⟨z, ?_, ?_⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι
refine_1₁ : Eq (α := S₁.homology ⟶ S₁.opcycles) ((homologyMap φ ≫ z) ≫ S₁.homologyι) S₁.homologyι
refine_1₂ : Eq (α := S₁.homology ⟶ S₁.opcycles) (homologyMap φ ≫ z ≫ S₁.homologyι) S₁.homologyι
refine_1₃ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (S₂.homologyι ≫ inv (opcyclesMap φ))) S₁.homologyι
refine_1₄ :
  Eq (α := S₁.homology ⟶ S₁.opcycles)
    (S₁.homologyι ≫ CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ) (inv (opcyclesMap φ))) S₁.homologyι
refine_1₅ : Eq (α := S₁.homology ⟶ S₁.opcycles) (S₁.homologyι ≫ 𝟙 S₁.opcycles) S₁.homologyι
refine_1₆ refine_1₇ : Eq (α := S₁.homology ⟶ S₁.opcycles) S₁.homologyι S₁.homologyι
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology

Tactic:
rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc,
      IsIso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.homologyι_naturality_assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.ShortComplex.homologyι, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_2 : CategoryStruct.comp (Y := S₂.homology) (z ≫ homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₁ : z ≫ CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₂ : z ≫ S₁.homologyι ≫ opcyclesMap φ = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₃ :
  S₂.homologyι ≫ CategoryStruct.comp (Y := S₁.opcycles) (inv (opcyclesMap φ)) (opcyclesMap φ) =
    𝟙 S₂.homology ≫ S₂.homologyι
refine_2₄ : S₂.homologyι ≫ 𝟙 S₂.opcycles = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₅ : S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι
refine_2₆ refine_2₇ : Eq (α := S₂.homology ⟶ S₂.opcycles) S₂.homologyι S₂.homologyι
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology

Tactic:
rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz,
      IsIso.inv_hom_id, comp_id, id_comp]

Premises used: CategoryTheory.ShortComplex.homologyι_naturality, CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.homologyι, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : IsZero.{v, u} S.X₂
inst_2 : S.HasHomology
⊢ IsZero.{v, u} S.homology

Tactic:
IsZero.of_iso hS (HomologyData.ofZeros S (hS.eq_of_tgt _ _)
    (hS.eq_of_src _ _)).left.homologyIso

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.ShortComplex.HomologyData.ofZeros, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
⊢ IsIso (X := S.cycles) S.leftHomologyπ

Tactic:
have := S.isIso_leftHomologyπ hf
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
this : IsIso (X := S.cycles) S.leftHomologyπ
dsimp : IsIso (X := S.cycles) (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
⊢ IsIso (X := S.cycles) (Y := S.homology) S.homologyπ

Tactic:
dsimp only [homologyπ]

Premises used: CategoryTheory.ShortComplex.homologyπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
this : IsIso (X := S.cycles) S.leftHomologyπ
⊢ IsIso (X := S.cycles) (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
⊢ IsIso (X := S.rightHomology) S.rightHomologyι

Tactic:
have := S.isIso_rightHomologyι hg
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
this : IsIso (X := S.rightHomology) S.rightHomologyι
dsimp : IsIso (X := S.homology) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι)
⊢ IsIso (X := S.homology) S.homologyι

Tactic:
dsimp only [homologyι]

Premises used: CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
this : IsIso (X := S.rightHomology) S.rightHomologyι
⊢ IsIso (X := S.homology) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hf : S.f = 0
inst_2 : S.HasHomology
⊢ IsIso (X := S.cycles) (Y := S.homology) S.homologyπ

Tactic:
have := S.isIso_homologyπ hf
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hf : S.f = 0
inst_2 : S.HasHomology
this : IsIso (X := S.cycles) (Y := S.homology) S.homologyπ
⊢ S.cycles ≅ S.homology

Tactic:
exact asIso S.homologyπ

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
⊢ Iso.inv (S.asIsoHomologyπ hf) ≫ S.homologyπ = 𝟙 S.homology

Tactic:
Iso.inv_hom_id _

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hf : S.f = 0
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.homology) S.homologyπ (Iso.inv (S.asIsoHomologyπ hf)) : S.cycles ⟶ S.cycles)
    (𝟙 S.cycles : S.cycles ⟶ S.cycles)

Tactic:
(S.asIsoHomologyπ hf).hom_inv_id

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.asIsoHomologyπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hg : S.g = 0
inst_2 : S.HasHomology
⊢ IsIso (X := S.homology) S.homologyι

Tactic:
have := S.isIso_homologyι hg
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hg : S.g = 0
inst_2 : S.HasHomology
this : IsIso (X := S.homology) S.homologyι
⊢ S.homology ≅ S.opcycles

Tactic:
exact asIso S.homologyι

Premises used: CategoryTheory.ShortComplex.homologyι, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
⊢ Eq (α := S.opcycles ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.inv (S.asIsoHomologyι hg)) S.homologyι : S.opcycles ⟶ S.opcycles)
    (𝟙 S.opcycles : S.opcycles ⟶ S.opcycles)

Tactic:
Iso.inv_hom_id _

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hg : S.g = 0
inst_2 : S.HasHomology
⊢ S.homologyι ≫ Iso.inv (S.asIsoHomologyι hg) = 𝟙 S.homology

Tactic:
(S.asIsoHomologyι hg).hom_inv_id

Premises used: CategoryTheory.ShortComplex.asIsoHomologyι, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
rw : Mono (X := S₁.homology) (Y := S₂.opcycles) (S₁.homologyι ≫ opcyclesMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)

Tactic:
rw [homologyι_naturality φ]

Premises used: CategoryTheory.ShortComplex.homologyι_naturality
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.opcycles) (S₁.homologyι ≫ opcyclesMap φ)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)

Tactic:
have : Mono (homologyMap φ ≫ S₂.homologyι) := by
    rw [homologyι_naturality φ]
    apply mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
this :
  Mono (X := S₁.homology) (Y := S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
mono_of_mono (homologyMap φ) S₂.homologyι

Premises used: CategoryTheory.mono_of_mono, CategoryTheory.ShortComplex.homologyι, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
this :
  Mono (X := S₁.homology) (Y := S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
exact mono_of_mono (homologyMap φ) S₂.homologyι

Premises used: CategoryTheory.mono_of_mono, CategoryTheory.ShortComplex.homologyι, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : Mono (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
⊢ Mono (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
mono_homologyMap_of_mono_opcyclesMap' φ inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.mono_homologyMap_of_mono_opcyclesMap'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
rw : Epi (X := S₁.cycles) (Y := S₂.homology) (cyclesMap φ ≫ S₂.homologyπ)
⊢ Epi (X := S₁.cycles) (Y := S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)

Tactic:
rw [homologyπ_naturality φ]

Premises used: CategoryTheory.ShortComplex.homologyπ_naturality
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
⊢ Epi (X := S₁.cycles) (Y := S₂.homology) (cyclesMap φ ≫ S₂.homologyπ)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
⊢ Epi (X := S₁.cycles) (Y := S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)

Tactic:
have : Epi (S₁.homologyπ ≫ homologyMap φ) := by
    rw [homologyπ_naturality φ]
    apply epi_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
this :
  Epi (X := S₁.cycles) (Y := S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)
⊢ Epi (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
epi_of_epi S₁.homologyπ (homologyMap φ)

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.epi_of_epi, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
this :
  Epi (X := S₁.cycles) (Y := S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)
⊢ Epi (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
exact epi_of_epi S₁.homologyπ (homologyMap φ)

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.epi_of_epi, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : Epi (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
⊢ Epi (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
epi_homologyMap_of_epi_cyclesMap' φ inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.epi_homologyMap_of_epi_cyclesMap'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.X₃) (S.iCycles ≫ S.g) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ (canonical S).f' = S.toCycles

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.LeftHomologyData.canonical, CategoryTheory.ShortComplex.cycles, rfl, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
⊢ Eq (α := S.X₁ ⟶ S.opcycles) (S.f ≫ S.pOpcycles) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ (canonical S).g' = S.fromOpcycles

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.RightHomologyData.canonical, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ShortComplex.fromOpcycles, CategoryTheory.ShortComplex.RightHomologyData.descQ, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.LeftHomologyData
A : C
⊢ Mono h.i

Tactic:
⟨fun _ _ => Fork.IsLimit.hom_ext h.hi⟩

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.hi, CategoryTheory.Limits.Fork.IsLimit.hom_ext, CategoryTheory.Mono.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.LeftHomologyData
A : C
⊢ Epi h.π

Tactic:
⟨fun _ _ => Cofork.IsColimit.hom_ext h.hπ⟩

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.ShortComplex.LeftHomologyData.hπ, CategoryTheory.Epi.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
⊢ h.liftK k hk ≫ h.i = k

Tactic:
h.hi.fac _ WalkingParallelPair.zero

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.LeftHomologyData.hi, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac